:: ALG_1 semantic presentation
theorem E1: :: ALG_1:1
theorem E2: :: ALG_1:2
theorem :: ALG_1:3
theorem E3: :: ALG_1:4
theorem E4: :: ALG_1:5
proof
let c
1, c
2, c
3 be
Universal_Algebra;
let c
4 be
Function of c
1,c
2;
let c
5 be
Function of c
2,c
3;
let c
6 be
FinSequence of c
1;
E5:
len (c5 * (c4 * c6)) = len (c4 * c6)
by E1;
E6:
dom (c5 * (c4 * c6)) = dom (c4 * c6)
by E1;
E7:
len (c4 * c6) = len c
6
by E1;
E8:
dom (c4 * c6) = dom c
6
by E1;
E9:
len c
6 = len ((c5 * c4) * c6)
by E1;
E10:
dom c
6 = dom ((c5 * c4) * c6)
by E1;
E11:
(
dom c
6 = Seg (len c6) &
dom (c5 * (c4 * c6)) = Seg (len c6) &
dom (c4 * c6) = Seg (len c6) &
dom ((c5 * c4) * c6) = Seg (len c6) )
by E6, E8, E9, FINSEQ_1:def 3;
now
let c
7 be
Nat;
assume E12:
c
7 in dom c
6
;
then E13:
c
6 . c
7 in the
carrier of c
1
by FINSEQ_2:13;
thus (c5 * (c4 * c6)) . c
7 =
c
5 . ((c4 * c6) . c7)
by E6, E8, E12, E1
.=
c
5 . (c4 . (c6 . c7))
by E8, E12, E1
.=
(c5 * c4) . (c6 . c7)
by E13, FUNCT_2:21
.=
((c5 * c4) * c6) . c
7
by E10, E12, E1
;
end;
hence
c
5 * (c4 * c6) = (c5 * c4) * c
6
by E5, E7, E9, E11, FINSEQ_2:10;
end;
:: deftheorem E5 defines is_homomorphism ALG_1:def 1 :
:: deftheorem E6 defines is_monomorphism ALG_1:def 2 :
:: deftheorem E7 defines is_epimorphism ALG_1:def 3 :
:: deftheorem E8 defines is_isomorphism ALG_1:def 4 :
:: deftheorem E9 defines are_isomorphic ALG_1:def 5 :
theorem E10: :: ALG_1:6
theorem E11: :: ALG_1:7
proof
let c
1, c
2, c
3 be
Universal_Algebra;
let c
4 be
Function of c
1,c
2;
let c
5 be
Function of c
2,c
3;
set c
6 =
signature c
1;
set c
7 =
signature c
2;
set c
8 =
signature c
3;
assume E12:
( c
4 is_homomorphism c
1,c
2 & c
5 is_homomorphism c
2,c
3 )
;
then
( c
1,c
2 are_similar & c
2,c
3 are_similar )
by E5;
then E13:
(
signature c
1 = signature c
2 &
signature c
2 = signature c
3 )
by UNIALG_2:def 2;
hence
signature c
1 = signature c
3
;
:: according to UNIALG_2:def 2,
ALG_1:def 1
E14:
(
len (signature c1) = len the
charact of c
1 &
len (signature c2) = len the
charact of c
2 )
by UNIALG_1:def 11;
E15:
(
dom the
charact of c
1 = Seg (len the charact of c1) &
dom the
charact of c
2 = Seg (len the charact of c2) &
dom (signature c1) = Seg (len (signature c1)) &
dom (signature c2) = Seg (len (signature c2)) )
by FINSEQ_1:def 3;
let c
9 be
Nat;
assume E16:
c
9 in dom the
charact of c
1
;
then reconsider c
10 = the
charact of c
2 . c
9 as
operation of c
2 by E13, E14, E15, UNIALG_2:6;
let c
11 be
operation of c
1;
let c
12 be
operation of c
3;
assume E17:
( c
11 = the
charact of c
1 . c
9 & c
12 = the
charact of c
3 . c
9 )
;
let c
13 be
FinSequence of c
1;
assume E18:
c
13 in dom c
11
;
then E19:
( c
11 . c
13 in rng c
11 &
rng c
11 c= the
carrier of c
1 )
by FUNCT_1:def 5, RELSET_1:12;
E20:
(
(signature c1) . c
9 = arity c
11 &
(signature c2) . c
9 = arity c
10 )
by E13, E14, E15, E16, E17, UNIALG_1:def 11;
E21:
(
dom c
10 = (arity c10) -tuples_on the
carrier of c
2 &
dom c
11 = (arity c11) -tuples_on the
carrier of c
1 )
by UNIALG_2:2;
then
c
13 in { b1 where B is Element of the carrier of c1 * : len b1 = arity c11 }
by E18, FINSEQ_2:def 4;
then consider c
14 being
Element of the
carrier of c
1 * such that E22:
( c
14 = c
13 &
len c
14 = arity c
11 )
;
reconsider c
15 = c
4 * c
13 as
Element of the
carrier of c
2 * by FINSEQ_1:def 11;
len (c4 * c13) = arity c
10
by E13, E20, E22, E1;
then
c
15 in { b1 where B is Element of the carrier of c2 * : len b1 = arity c10 }
;
then
c
4 * c
13 in dom c
10
by E21, FINSEQ_2:def 4;
then
( c
4 . (c11 . c13) = c
10 . (c4 * c13) & c
5 . (c10 . (c4 * c13)) = c
12 . (c5 * (c4 * c13)) )
by E12, E13, E14, E15, E16, E17, E18, E5;
hence (c5 * c4) . (c11 . c13) =
c
12 . (c5 * (c4 * c13))
by E19, FUNCT_2:21
.=
c
12 . ((c5 * c4) * c13)
by E4
;
end;
theorem E12: :: ALG_1:8
theorem E13: :: ALG_1:9
theorem E14: :: ALG_1:10
proof
let c
1, c
2 be
Universal_Algebra;
let c
3 be
Function of c
1,c
2;
let c
4 be
Function of c
2,c
1;
assume E15:
( c
3 is_isomorphism c
1,c
2 & c
4 = c
3 " )
;
then E16:
( c
3 is_homomorphism c
1,c
2 &
rng c
3 = the
carrier of c
2 & c
3 is
one-to-one )
by E12;
then E17:
c
1,c
2 are_similar
by E5;
then E18:
signature c
1 = signature c
2
by UNIALG_2:def 2;
E19:
(
len (signature c1) = len the
charact of c
1 &
len (signature c2) = len the
charact of c
2 )
by UNIALG_1:def 11;
E20:
(
dom (signature c1) = dom (signature c1) &
dom (signature c2) = Seg (len (signature c2)) &
dom the
charact of c
1 = Seg (len the charact of c1) &
dom the
charact of c
2 = Seg (len the charact of c2) )
by FINSEQ_1:def 3;
now
let c
5 be
Nat;
assume E21:
c
5 in dom the
charact of c
2
;
let c
6 be
operation of c
2;
let c
7 be
operation of c
1;
assume E22:
( c
6 = the
charact of c
2 . c
5 & c
7 = the
charact of c
1 . c
5 )
;
let c
8 be
FinSequence of c
2;
assume
c
8 in dom c
6
;
then
c
8 in (arity c6) -tuples_on the
carrier of c
2
by UNIALG_2:2;
then
c
8 in { b1 where B is Element of the carrier of c2 * : len b1 = arity c6 }
by FINSEQ_2:def 4;
then consider c
9 being
Element of the
carrier of c
2 * such that E23:
( c
8 = c
9 &
len c
9 = arity c
6 )
;
defpred S
1[
set ,
set ] means c
3 . a
2 = c
8 . a
1;
E24:
for b
1 being
Nat holds
not ( b
1 in Seg (len c8) & ( for b
2 being
Element of c
1 holds
not S
1[b
1,b
2] ) )
consider c
10 being
FinSequence of c
1 such that E25:
(
dom c
10 = Seg (len c8) & ( for b
1 being
Nat holds
( b
1 in Seg (len c8) implies S
1[b
1,c
10 . b
1] ) ) )
from FINSEQ_1:sch 5(E24);
E26: c
4 * c
3 =
id (dom c3)
by E15, E16, FUNCT_1:61
.=
id the
carrier of c
1
by FUNCT_2:def 1
;
E27:
(
len c
10 = len c
8 &
dom c
8 = Seg (len c8) &
dom (c3 * c10) = dom c
10 )
by E25, E1, FINSEQ_1:def 3;
now
let c
11 be
Nat;
assume E28:
c
11 in dom c
8
;
hence c
8 . c
11 =
c
3 . (c10 . c11)
by E25, E27
.=
(c3 * c10) . c
11
by E25, E27, E28, E1
;
end;
then E28:
c
8 = c
3 * c
10
by E25, E27, FINSEQ_1:17;
then E29: c
4 * c
8 =
(id the carrier of c1) * c
10
by E26, E4
.=
c
10
by E3
;
reconsider c
11 = c
10 as
Element of the
carrier of c
1 * by FINSEQ_1:def 11;
(
(signature c1) . c
5 = arity c
7 &
(signature c2) . c
5 = arity c
6 )
by E18, E19, E20, E21, E22, UNIALG_1:def 11;
then
c
11 in { b1 where B is Element of the carrier of c1 * : len b1 = arity c7 }
by E18, E23, E27;
then
c
11 in (arity c7) -tuples_on the
carrier of c
1
by FINSEQ_2:def 4;
then E30:
c
11 in dom c
7
by UNIALG_2:2;
then E31:
c
4 . (c6 . c8) = c
4 . (c3 . (c7 . c11))
by E16, E18, E19, E20, E21, E22, E28, E5;
E32:
c
7 . c
11 in the
carrier of c
1
by E30, PARTFUN1:27;
then
c
7 . c
11 in dom c
3
by FUNCT_2:def 1;
hence c
4 . (c6 . c8) =
(id the carrier of c1) . (c7 . c11)
by E26, E31, FUNCT_1:23
.=
c
7 . (c4 * c8)
by E29, E32, FUNCT_1:34
;
end;
hence
c
4 is_homomorphism c
2,c
1
by E17, E5;
end;
theorem E15: :: ALG_1:11
proof
let c
1, c
2 be
Universal_Algebra;
let c
3 be
Function of c
1,c
2;
let c
4 be
Function of c
2,c
1;
assume E16:
( c
3 is_isomorphism c
1,c
2 & c
4 = c
3 " )
;
then E17:
c
3 is
one-to-one
by E12;
then E18:
c
4 is
one-to-one
by E16, FUNCT_1:62;
E19:
rng c
4 =
dom c
3
by E16, E17, FUNCT_1:55
.=
the
carrier of c
1
by FUNCT_2:def 1
;
c
4 is_homomorphism c
2,c
1
by E16, E14;
hence
c
4 is_isomorphism c
2,c
1
by E18, E19, E12;
end;
theorem E16: :: ALG_1:12
proof
let c
1, c
2, c
3 be
Universal_Algebra;
let c
4 be
Function of c
1,c
2;
let c
5 be
Function of c
2,c
3;
assume E17:
( c
4 is_isomorphism c
1,c
2 & c
5 is_isomorphism c
2,c
3 )
;
then E18:
( c
4 is
one-to-one & c
5 is
one-to-one )
by E12;
E19:
rng (c5 * c4) = the
carrier of c
3
E20:
c
5 * c
4 is
one-to-one
by E18, FUNCT_1:46;
( c
4 is_homomorphism c
1,c
2 & c
5 is_homomorphism c
2,c
3 )
by E17, E12;
then
c
5 * c
4 is_homomorphism c
1,c
3
by E11;
hence
c
5 * c
4 is_isomorphism c
1,c
3
by E19, E20, E12;
end;
theorem :: ALG_1:13
theorem :: ALG_1:14
proof
let c
1, c
2 be
Universal_Algebra;
assume
c
1,c
2 are_isomorphic
;
then consider c
3 being
Function of c
1,c
2 such that E17:
c
3 is_isomorphism c
1,c
2
by E9;
E18:
c
3 is_epimorphism c
1,c
2
by E17, E8;
c
3 is_monomorphism c
1,c
2
by E17, E8;
then E19:
c
3 is
one-to-one
by E6;
then E20:
dom (c3 " ) =
rng c
3
by FUNCT_1:55
.=
the
carrier of c
2
by E18, E7
;
rng (c3 " ) =
dom c
3
by E19, FUNCT_1:55
.=
the
carrier of c
1
by FUNCT_2:def 1
;
then reconsider c
4 = c
3 " as
Function of c
2,c
1 by E20, FUNCT_2:def 1, RELSET_1:11;
take
c
4
;
:: according to ALG_1:def 5
thus
c
4 is_isomorphism c
2,c
1
by E17, E15;
end;
theorem :: ALG_1:15
proof
let c
1, c
2, c
3 be
Universal_Algebra;
assume E17:
c
1,c
2 are_isomorphic
;
assume E18:
c
2,c
3 are_isomorphic
;
consider c
4 being
Function of c
1,c
2 such that E19:
c
4 is_isomorphism c
1,c
2
by E17, E9;
consider c
5 being
Function of c
2,c
3 such that E20:
c
5 is_isomorphism c
2,c
3
by E18, E9;
c
5 * c
4 is_isomorphism c
1,c
3
by E19, E20, E16;
hence
c
1,c
3 are_isomorphic
by E9;
end;
definition
let c
1, c
2 be
Universal_Algebra;
let c
3 be
Function of c
1,c
2;
assume E17:
c
3 is_homomorphism c
1,c
2
;
func Image c
3 -> strict SubAlgebra of a
2 means :
E17:
:: ALG_1:def 6
the
carrier of a
4 = a
3 .: the
carrier of a
1;
existence
ex b1 being strict SubAlgebra of c2 st the carrier of b1 = c3 .: the carrier of c1
proof
E18:
dom c
3 = the
carrier of c
1
by FUNCT_2:def 1;
then reconsider c
4 = c
3 .: the
carrier of c
1 as non
empty Subset of c
2 by RELAT_1:152;
take c
5 =
UniAlgSetClosed c
4;
c
4 is
opers_closed
proof
let c
6 be
operation of c
2;
:: according to UNIALG_2:def 5
consider c
7 being
Nat such that E19:
( c
7 in dom the
charact of c
2 & the
charact of c
2 . c
7 = c
6 )
by FINSEQ_2:11;
E20:
c
1,c
2 are_similar
by E17, E5;
then E21:
signature c
1 = signature c
2
by UNIALG_2:def 2;
E22:
(
len (signature c1) = len the
charact of c
1 &
len (signature c2) = len the
charact of c
2 )
by UNIALG_1:def 11;
E23:
(
dom the
charact of c
1 = Seg (len the charact of c1) &
dom the
charact of c
2 = Seg (len the charact of c2) &
dom (signature c1) = Seg (len (signature c1)) &
dom (signature c1) = dom (signature c2) &
dom (signature c2) = Seg (len (signature c2)) )
by E20, FINSEQ_1:def 3, UNIALG_2:def 2;
then reconsider c
8 = the
charact of c
1 . c
7 as
operation of c
1 by E19, E22, UNIALG_2:6;
let c
9 be
FinSequence of c
4;
:: according to UNIALG_2:def 4
assume E24:
len c
9 = arity c
6
;
E25:
(
(signature c1) . c
7 = arity c
8 &
(signature c2) . c
7 = arity c
6 )
by E19, E22, E23, UNIALG_1:def 11;
defpred S
1[
set ,
set ] means c
3 . a
2 = c
9 . a
1;
E26:
for b
1 being
set holds
not ( b
1 in dom c
9 & ( for b
2 being
set holds
not ( b
2 in the
carrier of c
1 & S
1[b
1,b
2] ) ) )
consider c
10 being
Function such that E27:
(
dom c
10 = dom c
9 &
rng c
10 c= the
carrier of c
1 & ( for b
1 being
set holds
( b
1 in dom c
9 implies S
1[b
1,c
10 . b
1] ) ) )
from WELLORD2:sch 1(E26);
dom c
10 = Seg (len c9)
by E27, FINSEQ_1:def 3;
then reconsider c
11 = c
10 as
FinSequence by FINSEQ_1:def 2;
reconsider c
12 = c
11 as
FinSequence of c
1 by E27, FINSEQ_1:def 4;
reconsider c
13 = c
12 as
Element of the
carrier of c
1 * by FINSEQ_1:def 11;
E28:
len c
13 = len c
9
by E27, FINSEQ_3:31;
then
c
13 in { b1 where B is Element of the carrier of c1 * : len b1 = arity c8 }
by E21, E24, E25;
then
c
13 in (arity c8) -tuples_on the
carrier of c
1
by FINSEQ_2:def 4;
then E29:
c
13 in dom c
8
by UNIALG_2:2;
then E30:
c
3 . (c8 . c13) = c
6 . (c3 * c13)
by E17, E19, E22, E23, E5;
E31:
len (c3 * c13) = len c
13
by E1;
E32:
dom (c3 * c13) = Seg (len (c3 * c13))
by FINSEQ_1:def 3;
then E33:
c
9 = c
3 * c
13
by E28, E31, FINSEQ_2:10;
(
rng c
8 c= the
carrier of c
1 & c
8 . c
13 in rng c
8 )
by E29, FUNCT_1:def 5, RELSET_1:12;
hence
c
6 . c
9 in c
4
by E18, E30, E33, FUNCT_1:def 12;
end;
then
c
5 = UAStr(# c
4,
(Opers c2,c4) #)
by UNIALG_2:def 9;
hence
the
carrier of c
5 = c
3 .: the
carrier of c
1
;
end;
uniqueness
for b1, b2 being strict SubAlgebra of c2 holds
( ( the carrier of b1 = c3 .: the carrier of c1 & the carrier of b2 = c3 .: the carrier of c1 ) implies ( b1 = b2 ) )
end;
:: deftheorem E17 defines Image ALG_1:def 6 :
theorem :: ALG_1:16
theorem :: ALG_1:17
definition
let c
1 be non
empty set ;
let c
2 be
Relation of c
1;
canceled;canceled;func ExtendRel c
2 -> Relation of a
1 * means :
E18:
:: ALG_1:def 9
for b
1, b
2 being
FinSequence of a
1 holds
(
[b1,b2] in a
3 iff (
len b
1 = len b
2 & ( for b
3 being
Nat holds
( b
3 in dom b
1 implies
[(b1 . b3),(b2 . b3)] in a
2 ) ) ) );
existence
ex b1 being Relation of c1 * st
for b2, b3 being FinSequence of c1 holds
( [b2,b3] in b1 iff ( len b2 = len b3 & ( for b4 being Nat holds
( b4 in dom b2 implies [(b2 . b4),(b3 . b4)] in c2 ) ) ) )
proof
defpred S
1[
set ,
set ] means for b
1, b
2 being
FinSequence of c
1 holds
( ( b
1 = a
1 & b
2 = a
2 ) implies ( (
len b
1 = len b
2 & ( for b
3 being
Nat holds
( b
3 in dom b
1 implies
[(b1 . b3),(b2 . b3)] in c
2 ) ) ) ) );
consider c
3 being
Relation of c
1 * ,c
1 * such that E18:
for b
1, b
2 being
set holds
(
[b1,b2] in c
3 iff ( b
1 in c
1 * & b
2 in c
1 * & S
1[b
1,b
2] ) )
from RELSET_1:sch 1();
take
c
3
;
let c
4, c
5 be
FinSequence of c
1;
thus
(
[c4,c5] in c
3 implies (
len c
4 = len c
5 & ( for b
1 being
Nat holds
( b
1 in dom c
4 implies
[(c4 . b1),(c5 . b1)] in c
2 ) ) ) )
by E18;
assume E19:
(
len c
4 = len c
5 & ( for b
1 being
Nat holds
( b
1 in dom c
4 implies
[(c4 . b1),(c5 . b1)] in c
2 ) ) )
;
E20:
( c
4 in c
1 * & c
5 in c
1 * )
by FINSEQ_1:def 11;
S
1[c
4,c
5]
by E19;
hence
[c4,c5] in c
3
by E18, E20;
end;
uniqueness
for b1, b2 being Relation of c1 * holds
( ( ( for b3, b4 being FinSequence of c1 holds
( [b3,b4] in b1 iff ( len b3 = len b4 & ( for b5 being Nat holds
( b5 in dom b3 implies [(b3 . b5),(b4 . b5)] in c2 ) ) ) ) ) & ( for b3, b4 being FinSequence of c1 holds
( [b3,b4] in b2 iff ( len b3 = len b4 & ( for b5 being Nat holds
( b5 in dom b3 implies [(b3 . b5),(b4 . b5)] in c2 ) ) ) ) ) ) implies ( b1 = b2 ) )
proof
let c
3, c
4 be
Relation of c
1 * ;
assume that E18:
for b
1, b
2 being
FinSequence of c
1 holds
(
[b1,b2] in c
3 iff (
len b
1 = len b
2 & ( for b
3 being
Nat holds
( b
3 in dom b
1 implies
[(b1 . b3),(b2 . b3)] in c
2 ) ) ) )
and E19:
for b
1, b
2 being
FinSequence of c
1 holds
(
[b1,b2] in c
4 iff (
len b
1 = len b
2 & ( for b
3 being
Nat holds
( b
3 in dom b
1 implies
[(b1 . b3),(b2 . b3)] in c
2 ) ) ) )
;
for b
1, b
2 being
set holds
(
[b1,b2] in c
3 iff
[b1,b2] in c
4 )
hence
c
3 = c
4
by RELAT_1:def 2;
end;
end;
:: deftheorem ALG_1:def 7 :
canceled;
:: deftheorem ALG_1:def 8 :
canceled;
:: deftheorem E18 defines ExtendRel ALG_1:def 9 :
theorem E19: :: ALG_1:18