Copyright (c) 1990 Association of Mizar Users
environ
vocabulary FINSEQ_1, ARYTM_1, REALSET1, GROUP_2, SETFAM_1, GROUP_1, BOOLE,
RELAT_1, INT_1, GROUP_3, QC_LANG1, ABSVALUE, VECTSP_1, FINSOP_1, BINOP_1,
SETWISEO, FUNCT_1, FINSEQ_2, FUNCT_2, RLSUB_1, TARSKI, LATTICES, NAT_1,
SUBSET_1, RLSUB_2, GROUP_4, CARD_3, FINSEQ_4, ORDINAL2, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, FINSOP_1,
ORDINAL1, ORDINAL2, INT_1, SETWISEO, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1,
GROUP_2, GROUP_3, LATTICES, GROUP_1, DOMAIN_1, NAT_1;
constructors FINSOP_1, SETWISEO, FUNCSDOM, FINSEQ_3, GROUP_3, LATTICES,
DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0, ORDINAL2, ORDINAL1;
clusters SUBSET_1, FINSEQ_1, GROUP_3, INT_1, LATTICES, GROUP_1, RELSET_1,
STRUCT_0, RLSUB_2, GROUP_2, XREAL_0, ZFMISC_1, XBOOLE_0, ORDINAL2,
NUMBERS, ARYTM_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSOP_1,
FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, INT_1, LATTICES, NAT_1,
ORDERS_1, REAL_1, RLSUB_2, RLVECT_1, SETFAM_1, SUBSET_1, TARSKI,
ZFMISC_1, VECTSP_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes BINOP_1, DOMAIN_1, FINSEQ_1, FINSEQ_2, NAT_1, ORDERS_2, XBOOLE_0;
begin
definition let D be non empty set; let F be FinSequence of D; let X be set;
redefine func F - X -> FinSequence of D;
coherence by FINSEQ_3:93;
end;
scheme MeetSbgEx{G() -> Group, P[set]}:
ex H being strict Subgroup of G() st
the carrier of H =
meet{A where A is Subset of G() :
ex K being strict Subgroup of G() st A = the carrier of K & P[K]}
provided
A1: ex H being strict Subgroup of G() st P[H]
proof set X = {A where A is Subset of G():
ex K being strict Subgroup of G()
st A = the carrier of K & P[K]};
consider T being strict Subgroup of G() such that A2: P[T] by A1;
carr T = the carrier of T by GROUP_2:def 9;
then A3: carr T in X by A2;
then reconsider Y = meet X as Subset of G() by SETFAM_1:8;
now let Z be set;
assume Z in X;
then consider A being Subset of G() such that
A4: Z = A and
A5: ex K being strict Subgroup of G() st A = the carrier of K & P[K];
consider H being Subgroup of G() such that
A6: A = the carrier of H & P[H] by A5;
1.G() in H by GROUP_2:55;
hence 1.G() in Z by A4,A6,RLVECT_1:def 1;
end;
then A7: Y <> {} by A3,SETFAM_1:def 1;
A8: now let a,b be Element of G();
assume A9: a in Y & b in Y;
now let Z be set;
assume A10: Z in X;
then consider A being Subset of G() such that
A11: A = Z and
A12: ex H being strict Subgroup of G()
st A = the carrier of H & P[H];
consider H being Subgroup of G() such that
A13: A = the carrier of H & P[H] by A12;
a in the carrier of H & b in the carrier of H
by A9,A10,A11,A13,SETFAM_1:def 1;
then a in H & b in H by RLVECT_1:def 1;
then a * b in H by GROUP_2:59;
hence a * b in Z by A11,A13,RLVECT_1:def 1;
end;
hence a * b in Y by A3,SETFAM_1:def 1;
end;
now let a be Element of G();
assume A14: a in Y;
now let Z be set;
assume A15: Z in X;
then consider A being Subset of G() such that
A16: A = Z and
A17: ex H being strict Subgroup of G()
st A = the carrier of H & P[H];
consider H being Subgroup of G() such that
A18: A = the carrier of H & P[H] by A17;
a in the carrier of H by A14,A15,A16,A18,SETFAM_1:def 1;
then a in H by RLVECT_1:def 1;
then a" in H by GROUP_2:60;
hence a" in Z by A16,A18,RLVECT_1:def 1;
end;
hence a" in Y by A3,SETFAM_1:def 1;
end;
hence thesis by A7,A8,GROUP_2:61;
end;
reserve x,y,y1,y2,X,Y for set,
k,l,m,n for Nat,
i,i1,i2,i3,j for Integer,
G for Group,
a,b,c,d for Element of G,
A,B,C for Subset of G,
H,H1,H2,H3 for Subgroup of G,
h for Element of H,
F,F1,F2 for FinSequence of the carrier of G,
I,I1,I2 for FinSequence of INT;
scheme SubgrSep{G() -> Group,P[set]}:
ex X st X c= Subgroups G() &
for H being strict Subgroup of G() holds H in X iff P[H]
proof
defpred R[set] means ex H being Subgroup of G() st $1 = H & P[H];
consider X such that A1: x in X iff x in Subgroups G() &
R[x] from Separation;
take X;
thus X c= Subgroups G()
proof let x;
assume x in X;
hence x in Subgroups G() by A1;
end;
let H be strict Subgroup of G();
thus H in X implies P[H]
proof assume H in X;
then ex H1 being Subgroup of G() st H = H1 & P[H1] by A1;
hence thesis;
end;
assume A2: P[H];
H in Subgroups G() by GROUP_3:def 1;
hence thesis by A1,A2;
end;
definition let i;
canceled;
func @i -> Element of INT equals
:Def2: i;
coherence by INT_1:12;
end;
canceled 2;
theorem Th3:
a = h implies a |^ n = h |^ n
proof assume A1: a = h;
defpred P[Nat] means a |^ $1 = h |^ $1;
a |^ 0 = 1.G by GROUP_1:43
.= 1.H by GROUP_2:53
.= h |^ 0 by GROUP_1:43; then
A2: P[0];
A3: now let n;
assume A4: P[n];
a |^ (n + 1) = a |^ n * a by GROUP_1:49
.= h |^ n * h by A1,A4,GROUP_2:52
.= h |^ (n + 1) by GROUP_1:49;
hence P[n+1];
end;
for n holds P[n] from Ind(A2,A3);
hence thesis;
end;
theorem
a = h implies a |^ i = h |^ i
proof assume A1: a = h;
now per cases;
suppose A2: i >= 0;
hence a |^ i = a |^ abs( i ) by GROUP_1:55
.= h |^ abs( i ) by A1,Th3
.= h |^ i by A2,GROUP_1:55;
suppose A3: i < 0;
A4: a |^ abs( i ) = h |^ abs( i ) by A1,Th3;
thus a |^ i = (a |^ abs( i ))" by A3,GROUP_1:56
.= (h |^ abs( i ))" by A4,GROUP_2:57
.= h |^ i by A3,GROUP_1:56;
end;
hence thesis;
end;
theorem Th5:
a in H implies a |^ n in H
proof assume A1: a in H;
defpred P[Nat] means a |^ $1 in H;
a |^ 0 = 1.G by GROUP_1:43;
then A2: P[0] by GROUP_2:55;
A3: now let n;
assume A4: P[n];
a |^ (n + 1) = a |^ n * a by GROUP_1:49;
hence P[n+1] by A1,A4,GROUP_2:59;
end;
for n holds P[n] from Ind(A2,A3);
hence thesis;
end;
theorem Th6:
a in H implies a |^ i in H
proof assume A1: a in H;
now per cases;
suppose i >= 0;
then a |^ i = a |^ abs( i ) by GROUP_1:55;
hence thesis by A1,Th5;
suppose i < 0;
then a |^ i = (a |^ abs( i ))" & a |^ abs( i ) in H by A1,Th5,GROUP_1:56;
hence thesis by GROUP_2:60;
end;
hence thesis;
end;
definition let G be non empty HGrStr;
let F be FinSequence of the carrier of G;
func Product F -> Element of G equals
:Def3: (the mult of G) "**" F;
correctness;
end;
canceled;
theorem Th8:
for G being associative unital (non empty HGrStr),
F1,F2 being FinSequence of the carrier of G
holds Product(F1 ^ F2) = Product(F1) * Product(F2)
proof let G be associative unital (non empty HGrStr),
F1,F2 be FinSequence of the carrier of G;
set g = the mult of G;
A1: g is associative & g has_a_unity by GROUP_1:31,34;
thus Product(F1 ^ F2) = g "**" (F1 ^ F2) by Def3
.= g.(g "**" F1,g "**" F2)by A1,FINSOP_1:6
.= g.(Product(F1),g "**" F2) by Def3
.= g.(Product F1,Product F2) by Def3
.= Product F1 * Product F2 by VECTSP_1:def 10;
end;
theorem Th9:
for G being unital (non empty HGrStr),
F being FinSequence of the carrier of G,
a being Element of G
holds Product(F ^ <* a *>) = Product(F) * a
proof let G be unital (non empty HGrStr),
F be FinSequence of the carrier of G,
a be Element of G;
set g = the mult of G;
A1: g has_a_unity by GROUP_1:34;
thus Product(F ^ <* a *>) = g "**" (F ^ <* a *>) by Def3
.= g.(g "**" F,a) by A1,FINSOP_1:5
.= (g "**" F) * a by VECTSP_1:def 10
.= Product F * a by Def3;
end;
theorem Th10:
for G being associative unital (non empty HGrStr),
F being FinSequence of the carrier of G,
a being Element of G
holds Product(<* a *> ^ F) = a * Product(F)
proof let G be associative unital (non empty HGrStr),
F be FinSequence of the carrier of G,
a be Element of G;
set g = the mult of G;
A1: g is associative & g has_a_unity by GROUP_1:31,34;
thus Product(<* a *> ^ F) = g "**" (<* a *> ^ F) by Def3
.= g.(a,g "**" F) by A1,FINSOP_1:7
.= a * (g "**" F) by VECTSP_1:def 10
.= a * Product F by Def3;
end;
theorem Th11:
for G being unital (non empty HGrStr)
holds Product <*> the carrier of G = 1.G
proof let G be unital (non empty HGrStr);
set g = the mult of G;
A1: len <*> the carrier of G = 0 & g has_a_unity by FINSEQ_1:32,GROUP_1:34;
thus Product <*> the carrier of G = g "**" (<*> the carrier of G) by Def3
.= the_unity_wrt g by A1,FINSOP_1:def 1
.= 1.G by GROUP_1:33;
end;
theorem Th12:
for G being non empty HGrStr, a being Element of G holds
Product<* a *> = a
proof let G be non empty HGrStr, a be Element of G;
thus Product<* a *> = (the mult of G) "**" <* a *> by Def3
.= a by FINSOP_1:12;
end;
theorem Th13:
for G being non empty HGrStr, a,b being Element of G holds
Product<* a,b *> = a * b
proof let G be non empty HGrStr, a,b be Element of G;
thus Product<* a,b *> = (the mult of G) "**" <* a,b *> by Def3
.= (the mult of G).(a,b) by FINSOP_1:13
.= a * b by VECTSP_1:def 10;
end;
theorem
Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c)
proof <* a,b,c *> = <* a *> ^ <* b,c *> & <* a,b,c *> = <* a,b *> ^ <* c *>
&
Product<* a *> = a & Product<* c *> = c & Product<* a,b *> = a * b &
Product<* b,c *> = b * c by Th12,Th13,FINSEQ_1:60;
hence thesis by Th8;
end;
Lm1: now let G,a;
thus Product(0 |-> a) = Product <*> the carrier of G by FINSEQ_2:72
.= 1.G by Th11
.= a |^ 0 by GROUP_1:43;
end;
Lm2: now let G,a; let n;
assume A1: Product(n |-> a) = a |^ n;
thus Product((n + 1) |-> a) = Product((n |-> a) ^ <* a *>) by FINSEQ_2:74
.= Product(n |-> a) * Product<* a *> by Th8
.= a |^ n * a by A1,Th12
.= a |^ (n + 1) by GROUP_1:49;
end;
theorem
Product(n |-> a) = a |^ n
proof
defpred P[Nat] means Product($1 |-> a) = a |^ $1;
A1: P[0] by Lm1;
A2: for n being Nat st P[n] holds P[n+1] by Lm2;
for n being Nat holds P[n] from Ind(A1,A2);
hence thesis;
end;
theorem
Product(F - {1.G}) = Product(F)
proof defpred P[FinSequence of the carrier of G] means
Product($1 - {1.G}) = Product$1;
A1: P[<*> the carrier of G] by FINSEQ_3:81;
A2: for F,a st P[F] holds P[F ^ <* a *>]
proof let F,a;
assume A3: P[F];
A4: Product((F ^ <* a *>) - {1.G}) =
Product(((F - {1.G}) ^ (<* a *> - {1.G}))) by FINSEQ_3:80
.= Product F * Product(<* a *> - {1.G}) by A3,Th8;
now per cases;
suppose A5: a = 1.G;
then a in {1.G} by TARSKI:def 1;
then <* a *> - {1.G} = <*> the carrier of G by FINSEQ_3:83;
then Product(<* a *> - {1.G}) = 1.G by Th11;
hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>)
by A4,A5,Th9;
suppose a <> 1.G;
then not a in {1.G} by TARSKI:def 1;
then <* a *> - {1.G} = <* a *> by FINSEQ_3:82;
hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>) by A4,Th8;
end;
hence thesis;
end;
for F holds P[F] from IndSeqD(A1,A2);
hence thesis;
end;
Lm3: for F1 being FinSequence, y being Nat st y in dom F1 holds
len F1 - y + 1 is Nat & len F1 - y + 1 >= 1 & len F1 - y + 1 <= len F1
proof let F1 be FinSequence, y be Nat;
assume A1: y in dom F1;
now assume len F1 - y + 1 < 0;
then 1 < 0 - (len F1 - y) by REAL_1:86;
then 1 < - (len F1 - y) by XCMPLX_1:150;
then 1 < y - len F1 by XCMPLX_1:143;
then len F1 + 1 < y & y <= len F1 by A1,FINSEQ_3:27,REAL_1:86;
hence contradiction by NAT_1:37;
end;
then reconsider n = len F1 - y + 1 as Nat by INT_1:16;
y + 0 <= len F1 by A1,FINSEQ_3:27;
then A2: 0 + 1 = 1 & 0 <= len F1 - y by REAL_1:84;
n - 1 <= len F1 - y & y >= 1 by A1,FINSEQ_3:27,REAL_1:86;
then n - 1 - y <= len F1 - y - 1 by REAL_1:92;
then n - (y + 1) <= len F1 - y - 1 by XCMPLX_1:36;
then n - (y + 1) <= len F1 - (y + 1) by XCMPLX_1:36;
hence thesis by A2,AXIOMS:24,REAL_1:54;
end;
theorem Th17:
len F1 = len F2 &
(for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") implies
Product(F1) = Product(F2)"
proof defpred P[Nat] means
for F1,F2 st len F1 = $1 & len F1 = len F2 &
(for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") holds
Product(F1) = Product(F2)";
A1: P[0]
proof let F1,F2;
assume len F1 = 0 & len F1 = len F2;
then F1 = <*> the carrier of G & F2 = <*> the carrier of G
by FINSEQ_1:32;
then Product F1 = 1.G & Product F2 = 1.G & 1.G = (1.G)"
by Th11,GROUP_1:16;
hence thesis;
end;
A2: for n st P[n] holds P[n + 1]
proof let n;
assume A3: P[n];
let F1,F2;
assume that A4: len F1 = n + 1 & len F1 = len F2 and
A5: for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)";
reconsider p = F1 | Seg n
as FinSequence of the carrier of G by FINSEQ_1:23;
1 <= n + 1 by NAT_1:37;
then n + 1 in dom F1 by A4,FINSEQ_3:27;
then F1.(n + 1) in rng F1 & rng F1 c= the carrier of G
by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider a = F1.(n + 1) as Element of G;
A6: len p = n by A4,FINSEQ_3:59;
deffunc F(Nat) = F2.($1 + 1);
consider q being FinSequence such that A7: len q = len p and
A8: for k st k in Seg len p holds q.k = F(k) from SeqLambda;
A9: dom q = dom p by A7,FINSEQ_3:31;
A10: Seg len p = dom p by FINSEQ_1:def 3;
rng q c= the carrier of G
proof let x;
assume x in rng q;
then consider y such that A11: y in dom q & x = q.y by FUNCT_1:def
5;
reconsider y as Nat by A11;
A12: x = F2.(y + 1) by A8,A9,A10,A11;
A13: 1 <= y + 1 by NAT_1:37;
y <= len p by A7,A11,FINSEQ_3:27;
then y + 1 <= len F2 by A4,A6,REAL_1:55;
then y + 1 in dom F2 by A13,FINSEQ_3:27;
then x in rng F2 & rng F2 c= the carrier of G
by A12,FINSEQ_1:def 4,FUNCT_1:def 5;
hence thesis;
end;
then reconsider q as FinSequence of the carrier of G by FINSEQ_1:def 4;
A14: len F2 = len<* a" *> + len q by A4,A6,A7,FINSEQ_1:56;
A15: now let k;
assume k in dom<* a" *>;
then A16: k in {1} by FINSEQ_1:4,def 8;
len F2 >= 1 by A4,NAT_1:37;
then A17: len F2 in dom F1 by A4,FINSEQ_3:27;
then F2.(len F1 - len F1 + 1) = (F1/.len F1)" by A4,A5;
then (F1/.len F1)" = F2.(0 + 1) by XCMPLX_1:14
.= F2.k by A16,TARSKI:def 1;
then F2.k = a" & k = 1 by A4,A16,A17,FINSEQ_4:def 4,TARSKI:def 1;
hence <* a" *>.k = F2.k by FINSEQ_1:def 8;
end;
now let k;
assume k in dom q;
then k in dom q & len<* a" *> = 1 & k + 1 = 1 + k
by FINSEQ_1:56;
hence F2.(len<* a" *> + k) = q.k by A8,A9,A10;
end;
then A18: F2 = <* a" *> ^ q by A14,A15,FINSEQ_3:43;
now let k;
assume A19: k in dom p;
then reconsider i = len p - k + 1 as Nat by Lm3;
1 <= i & i <= len p by A19,Lm3;
then i in dom p by FINSEQ_3:27;
then A20: q.i = F2.(i + 1) by A8,A10;
len p <= len F1 & k <= len p by A4,A6,A19,FINSEQ_3:27,NAT_1:37;
then 1 <= k & k <= len F1 by A19,AXIOMS:22,FINSEQ_3:27;
then A21: k in dom F1 by FINSEQ_3:27;
A22: i + 1 = (len p + - k + 1) + 1 by XCMPLX_0:def 8
.= len F1 + - k + 1 by A4,A6,XCMPLX_1:1
.= len F1 - k + 1 by XCMPLX_0:def 8;
F1/.k = F1.k by A21,FINSEQ_4:def 4
.= p.k by A19,FUNCT_1:70
.= p/.k by A19,FINSEQ_4:def 4;
hence q.(len p - k + 1) = (p/.k)" by A5,A20,A21,A22;
end;
then A23: Product p = Product q" by A3,A6,A7;
F1 = p ^ <* a *> by A4,FINSEQ_3:61;
then A24: Product F1 = Product p * a by Th9;
Product F2 = a" * Product q by A18,Th10
.= a" * Product p" by A23,GROUP_1:19
.= (Product p * a)" by GROUP_1:25;
hence thesis by A24,GROUP_1:19;
end;
for k holds P[k] from Ind(A1,A2);
hence thesis;
end;
theorem
G is commutative Group implies
for P being Permutation of dom F1 st F2 = F1 * P holds
Product(F1) = Product(F2)
proof set g = the mult of G;
assume G is commutative Group;
then A1: g is commutative & g has_a_unity & g is associative
by GROUP_1:31,34,GROUP_3:2;
let P be Permutation of dom F1;
assume A2: F2 = F1 * P;
thus Product(F1) = g "**" F1 by Def3
.= g "**" F2 by A1,A2,FINSOP_1:8
.= Product(F2) by Def3;
end;
theorem
G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng
F2
implies Product(F1) = Product(F2)
proof set g = the mult of G;
assume G is commutative Group;
then A1: g is commutative & g has_a_unity & g is associative
by GROUP_1:31,34,GROUP_3:2;
assume A2: F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2;
thus Product(F1) = g "**" F1 by Def3
.= g "**" F2 by A1,A2,FINSOP_1:9
.= Product(F2) by Def3;
end;
theorem
G is commutative Group & len F = len F1 & len F = len F2 &
(for k st k in dom F holds F.k = (F1/.k) * (F2/.k)) implies
Product(F) = Product(F1) * Product(F2)
proof set g = the mult of G;
assume G is commutative Group;
then A1: g is commutative & g has_a_unity & g is associative
by GROUP_1:31,34,GROUP_3:2;
assume A2: len F = len F1 & len F = len F2;
assume A3: for k st k in dom F holds F.k = (F1/.k) * (F2/.k);
A4: now let k;
assume A5: k in dom F;
A6: dom F = Seg len F & dom F1 = Seg len F1 & dom F2 = Seg len F2
by FINSEQ_1:def 3;
thus F.k = (F1/.k) * (F2/.k) by A3,A5
.= g.(F1/.k,F2/.k) by VECTSP_1:def 10
.= g.(F1.k,F2/.k) by A2,A5,A6,FINSEQ_4:def 4
.= g.(F1.k,F2.k) by A2,A5,A6,FINSEQ_4:def 4;
end;
thus Product(F) = g "**" F by Def3
.= g.(g "**" F1,g "**" F2) by A1,A2,A4,FINSOP_1:10
.= (g "**" F1) * (g "**" F2) by VECTSP_1:def 10
.= Product(F1) * (g "**" F2) by Def3
.= Product(F1) * Product(F2) by Def3;
end;
theorem Th21:
rng F c= carr H implies Product(F) in H
proof
defpred P[FinSequence of the carrier of G] means
rng $1 c= carr H implies Product $1 in H;
A1: P[<*> the carrier of G]
proof assume rng <*> the carrier of G c= carr H;
1.G in H by GROUP_2:55;
hence Product(<*> the carrier of G) in H by Th11;
end;
A2: now let F,d;
assume A3: P[F];
thus P[F^<*d*>]
proof
assume A4: rng(F ^ <* d *>) c= carr H;
rng F c= rng(F ^ <* d *>) & rng<* d *> c= rng(F ^ <* d *>)
by FINSEQ_1:42,43;
then rng F c= carr H & rng<* d *> c= carr H & rng<* d *> = {d} &
d in {d} by A4,FINSEQ_1:56,TARSKI:def 1,XBOOLE_1:1;
then d in H & Product(F) in
H & Product(F ^ <* d *>) = Product(F) * d by A3,Th9,GROUP_2:88;
hence Product(F ^ <* d *>) in H by GROUP_2:59;
end;
end;
for F holds P[F] from IndSeqD(A1,A2);
hence thesis;
end;
definition let G,I,F;
func F |^ I -> FinSequence of the carrier of G means
:Def4: len it = len F &
for k st k in dom F holds it.k = (F/.k) |^ @(I/.k);
existence
proof
deffunc F(Nat) = (F/.$1) |^ @(I/.$1);
consider p being FinSequence such that A1: len p = len F and
A2: for k st k in Seg len F holds p.k = F(k) from SeqLambda;
A3: dom p = dom F by A1,FINSEQ_3:31;
A4: dom F = Seg len F by FINSEQ_1:def 3;
rng p c= the carrier of G
proof let x;
assume x in rng p;
then consider y such that A5: y in dom p & p.y = x by FUNCT_1:def 5;
reconsider y as Nat by A5;
x = (F/.y) |^ @(I/.y) & (F/.y) |^ @(I/.y) in the carrier of G
by A2,A3,A4,A5;
hence thesis;
end;
then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4;
take p;
thus thesis by A1,A2,A4;
end;
uniqueness
proof let F1,F2;
assume that A6: len F1 = len F and
A7: for k st k in dom F holds F1.k = (F/.k) |^ @(I/.k);
assume that A8: len F2 = len F and
A9: for k st k in dom F holds F2.k = (F/.k) |^ @(I/.k);
now let k;
assume k in Seg len F;
then A10: k in dom F by FINSEQ_1:def 3;
hence F1.k = (F/.k) |^ @(I/.k) by A7
.= F2.k by A9,A10;
end;
hence thesis by A6,A8,FINSEQ_2:10;
end;
end;
canceled 3;
theorem Th25:
len F1 = len I1 & len F2 = len I2 implies
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
proof assume A1: len F1 = len I1 & len F2 = len I2;
set q = F1 |^ I1; set r = F2 |^ I2;
A2: len(q ^ r) = len q + len r by FINSEQ_1:35
.= len F1 + len r by Def4
.= len F1 + len F2 by Def4
.= len(F1 ^ F2) by FINSEQ_1:35;
len(F1 ^ F2) = len F1 + len F2 by FINSEQ_1:35
.= len(I1 ^ I2) by A1,FINSEQ_1:35;
then A3: dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:31;
now let k;
assume A4: k in dom(F1 ^ F2);
now per cases by A4,FINSEQ_1:38;
suppose A5: k in dom F1;
then A6: k in dom I1 by A1,FINSEQ_3:31;
then A7: I1/.k = I1.k by FINSEQ_4:def 4;
A8: (I1 ^ I2).k = (I1 ^ I2)/.k by A3,A4,FINSEQ_4:def 4;
len q = len F1 by Def4;
then k in dom q by A5,FINSEQ_3:31;
then A9: (q ^ r).k = q.k by FINSEQ_1:def 7
.= (F1/.k) |^ @(I1/.k) by A5,Def4;
F1/.k = F1.k by A5,FINSEQ_4:def 4
.= (F1 ^ F2).k by A5,FINSEQ_1:def 7
.= (F1 ^ F2)/.k by A4,FINSEQ_4:def 4;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k)
by A6,A7,A8,A9,FINSEQ_1:def 7;
suppose ex n st n in dom F2 & k = len F1 + n;
then consider n such that A10: n in dom F2 and A11: k = len F1 + n;
A12: len r = len F2 & len q = len F1 by Def4;
then A13: n in dom r & n in dom I2 by A1,A10,FINSEQ_3:31;
then A14: (q ^ r).k = r.n &
(I1 ^ I2).k = I2.n & (F1 ^ F2).k = F2.n &
n in dom F2 & (F1 ^ F2).k = (F1 ^ F2)/.k &
F2.n = F2/.n
by A1,A4,A10,A11,A12,FINSEQ_1:def 7,FINSEQ_4:def 4;
A15: (I1 ^ I2)/.k = (I1 ^ I2).k by A3,A4,FINSEQ_4:def 4;
I2/.n = I2.n by A13,FINSEQ_4:def 4;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A14,A15,Def4
;
end;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k);
end;
hence thesis by A2,Def4;
end;
theorem Th26:
rng F c= carr H implies Product(F |^ I) in H
proof assume that A1: rng F c= carr H;
rng(F |^ I) c= carr H
proof let x;
assume x in rng(F |^ I);
then consider y such that A2: y in dom(F |^ I) & x = (F |^ I).y
by FUNCT_1:def 5;
reconsider y as Nat by A2;
len(F |^ I) = len F by Def4;
then A3: y in dom F by A2,FINSEQ_3:31;
then A4: x = (F/.y) |^ @(I/.y) by A2,Def4;
F.y in rng F & F.y = F/.y by A3,FINSEQ_4:def 4,FUNCT_1:def 5;
then F/.y in H by A1,GROUP_2:88;
then x in H by A4,Th6;
hence thesis by GROUP_2:88;
end;
hence thesis by Th21;
end;
theorem Th27:
(<*> the carrier of G) |^ (<*> INT) = {}
proof len <*> the carrier of G = 0 & len <*> INT = 0 by FINSEQ_1:32;
then len((<*> the carrier of G) |^ (<*> INT)) = 0 by Def4;
hence thesis by FINSEQ_1:25;
end;
theorem Th28:
<* a *> |^ <* @i *> = <* a |^ i *>
proof
A1: len<* a *> = 1 & len<* @i *> = 1 & len<* a |^ i*> = 1 by FINSEQ_1:56;
now let k;
assume A2: k in dom <* a *>;
A3: i = @i & @i = <* @i *>/.1 by Def2,FINSEQ_4:25;
dom <* a *> = Seg len <* a *> by FINSEQ_1:def 3;
then A4: k = 1 by A1,A2,FINSEQ_1:4,TARSKI:def 1;
hence <* a |^ i *>.k = a |^ i by FINSEQ_1:57
.= (<* a *>/.k) |^ @(<* @i *>/.k) by A3,A4,FINSEQ_4:25;
end;
hence thesis by A1,Def4;
end;
theorem Th29:
<* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>
proof len<* a *> = 1 & len<* b *> = 1 & len <* @i *> = 1 & len<* @j *> = 1 &
<* a,b *> = <* a *> ^ <* b *> & <* @i,@j *> = <* @i *> ^ <* @j *>
by FINSEQ_1:56,def 9;
hence <* a,b *> |^ <* @i,@j *> =
(<* a *> |^ <* @i *>) ^ (<* b *> |^ <* @j *>) by Th25
.= <* a |^ i *> ^ (<* b *> |^ <* @j *>) by Th28
.= <* a |^ i *> ^ <* b |^ j *> by Th28
.= <* a |^ i,b |^ j *> by FINSEQ_1:def 9;
end;
theorem
<* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>
proof len<* a *> = 1 & len<* b,c *> = 2 &
len <* @i1 *> = 1 & len<* @i2,@i3 *> = 2 &
<* a,b,c *> = <* a *> ^ <* b,c *> &
<* @i1,@i2,@i3 *> = <* @i1 *> ^ <* @i2,@i3 *>
by FINSEQ_1:56,60,61;
hence <* a,b,c *> |^ <* @i1,@i2,@i3 *> =
(<* a *> |^ <* @i1 *>) ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th25
.= <* a |^ i1 *> ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th28
.= <* a |^ i1 *> ^ <* b |^ i2,c |^ i3 *> by Th29
.= <* a |^ i1,b |^ i2,c |^ i3 *> by FINSEQ_1:60;
end;
theorem
F |^ (len F |-> @(1)) = F
proof defpred P[FinSequence of the carrier of G] means
$1 |^ (len $1 |-> @(1)) = $1;
A1: P[<*> the carrier of G]
proof set A = <*> the carrier of G;
thus A |^ (len A |-> @(1)) = A |^ (0 |-> @(1)) by FINSEQ_1:32
.= A |^ (<*> INT) by FINSEQ_2:72
.= A by Th27;
end;
A2: for F,a st P[F] holds P[F ^ <* a *>]
proof let F,a; set A = F ^ <* a *>;
assume A3: P[F];
A4: len A = len F + len<* a *> by FINSEQ_1:35;
A5: len<* a *> = 1 by FINSEQ_1:57;
A6: len<* @(1) *> = 1 by FINSEQ_1:57;
A7: len(len F |-> @(1)) = len F by FINSEQ_2:69;
thus A |^ (len A |-> @(1)) = A |^ ((len F |-> @(1)) ^ <* @(1) *>)
by A4,A5,FINSEQ_2:74
.= (F |^ (len F |-> @(1))) ^ (<* a *> |^ <* @(1) *>)
by A5,A6,A7,Th25
.= F ^ <* a |^ 1 *> by A3,Th28
.= F ^ <* a *> by GROUP_1:44;
end;
for F holds P[F] from IndSeqD(A1,A2);
hence thesis;
end;
theorem
F |^ (len F |-> @(0)) = len F |-> 1.G
proof defpred P[FinSequence of the carrier of G] means
$1 |^ (len $1 |-> @(0)) = len $1 |-> 1.G;
A1: P[<*> the carrier of G]
proof set A = <*> the carrier of G;
A2: len A = 0 by FINSEQ_1:32;
thus A |^ (len A |-> @(0)) = A |^ (0 |-> @(0)) by FINSEQ_1:32
.= A |^ (<*> INT) by FINSEQ_2:72
.= {} by Th27
.= len A |-> 1.G by A2,FINSEQ_2:72;
end;
A3: for F,a st P[F] holds P[F ^ <* a *>]
proof let F,a; set A = F ^ <* a *>;
assume A4: P[F];
A5: len A = len F + len<* a *> by FINSEQ_1:35;
A6: len<* a *> = 1 by FINSEQ_1:57;
A7: len<* @(0) *> = 1 by FINSEQ_1:57;
A8: len(len F |-> @(0)) = len F by FINSEQ_2:69;
thus A |^ (len A |-> @(0)) = A |^ ((len F |-> @(0)) ^ <* @(0) *>)
by A5,A6,FINSEQ_2:74
.= (F |^ (len F |-> @(0))) ^ (<* a *> |^ <* @(0) *>)
by A6,A7,A8,Th25
.= (len F |-> 1.G) ^ <* a |^ 0 *> by A4,Th28
.= (len F |-> 1.G) ^ <* 1.G *> by GROUP_1:43
.= (len A |-> 1.G) by A5,A6,FINSEQ_2:74;
end;
for F holds P[F] from IndSeqD(A1,A3);
hence thesis;
end;
theorem
len I = n implies (n |-> 1.G) |^ I = n |-> 1.G
proof defpred P[Nat] means
for I st len I = $1 holds ($1 |-> 1.G) |^ I = $1 |-> 1.G;
A1: P[0]
proof let I;
assume len I = 0;
then I = <*> INT & (0 |-> 1.G) = {} & {} = <*> the carrier of G
by FINSEQ_1:32,FINSEQ_2:72;
hence (0 |-> 1.G) |^ I = 0 |-> 1.G by Th27;
end;
A2: for k st P[k] holds P[k + 1]
proof let k;
assume A3: P[k];
let I;
assume A4: len I = k + 1;
reconsider J = I | Seg k as FinSequence of INT by FINSEQ_1:23;
A5: len J = k by A4,FINSEQ_3:59;
then A6: (k |-> 1.G) |^ J = k |-> 1.G by A3;
1 <= k + 1 by NAT_1:37;
then k + 1 in dom I by A4,FINSEQ_3:27;
then I.(k + 1) in
rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider i = I.(k + 1) as Integer by INT_1:12;
A7: I = J ^ <* i *> by A4,FINSEQ_3:61
.= J ^ <* @i *> by Def2;
A8: (k + 1) |-> 1.G = (k |-> 1.G) ^ <* 1.G *> by FINSEQ_2:74;
len(k |-> 1.G) = k & len<* 1.G *> = 1 & len<* @i *> = 1
by FINSEQ_1:57,FINSEQ_2:69;
then ((k + 1) |-> 1.G) |^ I =
((k |-> 1.G) |^ J) ^ (<* 1.G *> |^ <* @i *>)
by A5,A7,A8,Th25
.= (k |-> 1.G) ^ <* (1.G) |^ i *> by A6,Th28
.= (k |-> 1.G) ^ <* 1.G *> by GROUP_1:61;
hence thesis by FINSEQ_2:74;
end;
for k holds P[k] from Ind(A1,A2);
hence thesis;
end;
definition let G,A;
func gr A -> strict Subgroup of G means
:Def5: A c= the carrier of it &
(for H being strict Subgroup of G
st A c= the carrier of H holds it is Subgroup of H);
existence
proof
defpred P[set] means ex H st $1 = carr H & A c= $1;
consider X such that A1: Y in X iff Y in bool the carrier of G &
P[Y] from Separation;
set M = meet X;
A2: the carrier of G in bool the carrier of G &
the carrier of the HGrStr of G = the carrier of (Omega).G &
A c= the carrier of G &
carr (Omega).G = the carrier of (Omega).
G by GROUP_2:def 8,def 9,ZFMISC_1:def 1;
then A3: the carrier of G in X by A1;
A4: X <> {} by A1,A2;
now let Y;
assume Y in X;
then consider H such that A5: Y = carr H and A c= Y by A1;
1.G in H by GROUP_2:55;
hence 1.G in Y by A5,GROUP_2:88;
end;
then A6: M <> {} by A4,SETFAM_1:def 1;
M c= the carrier of G
proof consider x such that A7: x in X by A3;
consider H such that A8: x = carr H and A c= x by A1,A7;
let y;
assume y in M;
then y in carr H & carr H c= the carrier of G by A7,A8,SETFAM_1:def 1;
hence thesis;
end;
then reconsider M as Subset of G;
A9: now let a,b;
assume A10: a in M & b in M;
now let Y;
assume A11: Y in X;
then consider H such that A12: Y = carr H and A c= Y by A1;
a in carr H & b in carr H by A10,A11,A12,SETFAM_1:def 1;
hence a * b in Y by A12,GROUP_2:89;
end;
hence a * b in M by A4,SETFAM_1:def 1;
end;
now let a;
assume A13: a in M;
now let Y;
assume A14: Y in X;
then consider H such that A15: Y = carr H and A c= Y by A1;
a in carr H by A13,A14,A15,SETFAM_1:def 1;
hence a" in Y by A15,GROUP_2:90;
end;
hence a" in M by A4,SETFAM_1:def 1;
end;
then consider H being strict Subgroup of G such that
A16: the carrier of H = M by A6,A9,GROUP_2:61;
take H;
now let Y;
assume Y in X;
then ex H st Y = carr H & A c= Y by A1;
hence A c= Y;
end;
hence A c= the carrier of H by A4,A16,SETFAM_1:6;
let H1 be strict Subgroup of G;
assume A17: A c= the carrier of H1;
the carrier of H1 = carr H1 by GROUP_2:def 9;
then the carrier of H1 in X by A1,A17;
then M c= the carrier of H1 by SETFAM_1:4;
hence H is Subgroup of H1 by A16,GROUP_2:66;
end;
uniqueness
proof let H1,H2 be strict Subgroup of G;
assume A c= the carrier of H1 &
(for H being strict Subgroup of G
st A c= the carrier of H holds H1 is Subgroup of H) &
A c= the carrier of H2 &
(for H being strict Subgroup of G
st A c= the carrier of H holds H2 is Subgroup of H);
then H1 is Subgroup of H2 & H2 is Subgroup of H1;
hence thesis by GROUP_2:64;
end;
end;
canceled 3;
theorem Th37:
a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a
proof
thus a in gr A implies ex F,I st len F = len I & rng F c= A &
Product(F |^ I) = a
proof assume A1: a in gr A;
defpred P[set] means
ex F,I st $1 = Product (F |^ I) & len F = len I & rng F c= A;
reconsider B = {b : P[b]}
as Subset of G from SubsetD;
1.G = Product <*> the carrier of G & <*> the carrier of G = {} &
(<*> the carrier of G) |^ (<*> INT) = {} &
rng <*> the carrier of G = {} & {} c= A & len {} = 0 & len<*>INT = 0
by Th11,Th27,FINSEQ_1:25,27,XBOOLE_1:2;
then A2: 1.G in B;
A3: now let c,d;
assume that A4: c in B and A5: d in B;
A6: ex d1 being Element of G st c = d1 &
ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A by A4;
A7: ex d2 being Element of G st d = d2 &
ex F,I st d2 = Product(F |^ I) & len F = len I & rng F c= A by A5;
consider F1,I1 such that A8: c = Product(F1 |^ I1) and
A9: len F1 = len I1 and A10: rng F1 c= A by A6;
consider F2,I2 such that A11: d = Product(F2 |^ I2) and
A12: len F2 = len I2 and
A13: rng F2 c= A by A7;
A14: c * d = Product((F1 |^ I1) ^ (F2 |^ I2)) by A8,A11,Th8
.= Product((F1 ^ F2) |^ (I1 ^ I2)) by A9,A12,Th25;
rng(F1 ^ F2) = rng F1 \/ rng F2 by FINSEQ_1:44;
then A15: rng(F1 ^ F2) c= A by A10,A13,XBOOLE_1:8;
len(F1 ^ F2) = len I1 + len I2 by A9,A12,FINSEQ_1:35
.= len(I1 ^ I2) by FINSEQ_1:35;
hence c * d in B by A14,A15;
end;
now let c;
assume c in B;
then ex d1 being Element of G st c = d1 &
ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A;
then consider F1,I1 such that A16: c = Product(F1 |^ I1) and
A17: len F1 = len I1 and A18: rng F1 c= A;
A19: dom F1 = dom I1 by A17,FINSEQ_3:31;
deffunc F(Nat) = F1.(len F1 - $1 + 1);
consider F2 being FinSequence such that A20: len F2 = len F1 and
A21: for k st k in Seg len F1 holds F2.k = F(k) from SeqLambda;
A22: dom F2 = dom F1 by A20,FINSEQ_3:31;
A23: Seg len F1 = dom F1 by FINSEQ_1:def 3;
defpred P[Nat,set] means ex i st i = I1.(len I1 - $1 + 1) & $2 = - i;
A24: for k,y1,y2 st k in Seg len I1 & P[k,y1] & P[k,y2] holds
y1 = y2;
A25: for k st k in Seg len I1 ex x st P[k,x]
proof let k;
assume k in Seg len I1;
then A26: k in dom I1 by FINSEQ_1:def 3;
then reconsider n = len I1 - k + 1 as Nat by Lm3;
1 <= n & n <= len I1 by A26,Lm3;
then n in dom I1 by FINSEQ_3:27;
then I1.n in
rng I1 & rng I1 c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider i = I1.n as Element of INT qua non empty set;
reconsider i as Integer;
reconsider x = - i as set;
take x,i;
thus thesis;
end;
consider I2 being FinSequence such that A27: dom I2 = Seg len I1 and
A28: for k st k in Seg len I1 holds P[k,I2.k] from SeqEx(A24,A25);
A29: Seg len I1 = dom I1 by FINSEQ_1:def 3;
A30: len F2 = len I2 by A17,A20,A27,FINSEQ_1:def 3;
A31: dom F2 = dom I2 by A17,A20,A27,FINSEQ_1:def 3;
A32: rng F2 c= rng F1
proof let x;
assume x in rng F2;
then consider y such that A33: y in dom F2 & F2.y = x
by FUNCT_1:def 5;
reconsider y as Nat by A33;
A34: x = F1.(len F1 - y + 1) by A21,A22,A23,A33;
reconsider n = len F1 - y + 1 as Nat by A20,A33,Lm3;
A35: 1 <= n by A20,A33,Lm3;
n <= len F1 by A20,A33,Lm3;
then n in dom F1 by A35,FINSEQ_3:27;
hence thesis by A34,FUNCT_1:def 5;
end;
then A36: rng F2 c= A by A18,XBOOLE_1:1;
rng F1 c= the carrier of G by FINSEQ_1:def 4;
then rng F2 c= the carrier of G by A32,XBOOLE_1:1;
then reconsider F2 as FinSequence of the carrier of G by FINSEQ_1:def
4;
rng I2 c= INT
proof let x;
assume x in rng I2;
then consider y such that A37: y in dom I2 and A38: x = I2.y
by FUNCT_1:def 5;
reconsider y as Nat by A37;
ex i st i = I1.(len I1 - y + 1) & x = - i by A27,A28,A37,A38;
hence thesis by INT_1:12;
end;
then reconsider I2 as FinSequence of INT by FINSEQ_1:def 4;
set p = F1 |^ I1; set q = F2 |^ I2;
A39: len p = len F1 & len q = len F2 by Def4;
then A40: dom p = dom F1 & dom q = dom F2 by FINSEQ_3:31;
now let k;
assume A41: k in dom q;
then reconsider n = len p - k + 1 as Nat by A20,A39,Lm3;
1 <= n & len p >= n by A20,A39,A41,Lm3;
then A42: n in dom I2 & n in Seg len I2
by A20,A30,A39,FINSEQ_1:3,FINSEQ_3:27;
dom q = dom I1 by A17,A20,A39,FINSEQ_3:31;
then consider i such that A43: i = I1.n & I2.k = - i by A17,A28,
A29,A39,A41;
I2.k = I2/.k & I2/.k = @(I2/.k)
by A31,A40,A41,Def2,FINSEQ_4:def 4;
then q.k = (F2/.k) |^ (- i) & F2/.k = F2.k & F2.k = F1.n &
F1/.n= F1.n by A17,A21,A22,A23,A27,A39,A40,A41,A42,A43,Def4,
FINSEQ_4:def 4;
then A44: q.k = ((F1/.n) |^ i)" by GROUP_1:70;
I1.n = I1/.n & I1/.n = @(I1/.n)
by A27,A29,A42,Def2,FINSEQ_4:def 4;
then p.n = (F1/.n) |^ i by A19,A27,A29,A42,A43,Def4;
then (p/.n)" = ((F1/.n) |^ i)" & q/.k = q.k
by A19,A27,A29,A40,A41,A42,FINSEQ_4:def 4;
then p/.n = (q/.k)" by A44,GROUP_1:19;
hence (q/.k)" = p.(len p - k + 1)
by A19,A27,A29,A40,A42,FINSEQ_4:def 4;
end;
then Product p" = Product q by A20,A39,Th17;
hence c" in B by A16,A30,A36;
end;
then consider H being strict Subgroup of G such that
A45: the carrier of H = B by A2,A3,GROUP_2:61;
A c= B
proof let x;
assume A46: x in A;
then reconsider a = x as Element of G;
reconsider p = 1 as Integer;
A47: len<* a *> = 1 & len<* @p *> = 1 by FINSEQ_1:56;
A48: Product(<* a *> |^ <* @p *>) = Product<* a |^ 1 *> by Th28
.= a |^ 1 by Th12
.= a by GROUP_1:44;
rng<* a *> = {a} & {a} c= A by A46,FINSEQ_1:56,ZFMISC_1:37;
hence thesis by A47,A48;
end;
then gr A is Subgroup of H by A45,Def5;
then a in H by A1,GROUP_2:49;
then a in B by A45,RLVECT_1:def 1;
then ex b st
b = a & ex F,I st b = Product(F |^ I) & len F = len I & rng F c= A;
hence thesis;
end;
given F,I such that len F = len I and A49: rng F c= A and
A50: Product(F |^ I) = a;
A c= the carrier of gr A by Def5;
then A c= carr gr A by GROUP_2:def 9;
then rng F c= carr gr A by A49,XBOOLE_1:1;
hence thesis by A50,Th26;
end;
theorem Th38:
a in A implies a in gr A
proof assume A1: a in A;
A c= the carrier of gr A by Def5;
hence thesis by A1,RLVECT_1:def 1;
end;
theorem
gr {} the carrier of G = (1).G
proof
A1: {} the carrier of G c= the carrier of (1).G by XBOOLE_1:2;
for H being strict Subgroup of G
st {} the carrier of G c= the carrier of H holds
(1).G is Subgroup of H by GROUP_2:77;
hence thesis by A1,Def5;
end;
theorem Th40:
for H being strict Subgroup of G holds gr carr H = H
proof let H be strict Subgroup of G;
A1: carr H = the carrier of H by GROUP_2:def 9;
now let H1 be strict Subgroup of G;
assume carr H c= the carrier of H1;
then the carrier of H c= the carrier of H1 by GROUP_2:def 9;
hence H is Subgroup of H1 by GROUP_2:66;
end;
hence thesis by A1,Def5;
end;
theorem Th41:
A c= B implies gr A is Subgroup of gr B
proof assume A1: A c= B;
now let a;
assume a in gr A;
then consider F,I such that
A2: len F = len I & rng F c= A & Product(F |^ I) = a by Th37;
rng F c= B by A1,A2,XBOOLE_1:1;
hence a in gr B by A2,Th37;
end;
hence thesis by GROUP_2:67;
end;
theorem
gr(A /\ B) is Subgroup of gr A /\ gr B
proof
now let a;
assume a in gr(A /\ B);
then consider F,I such that
A1: len F = len I & rng F c= A /\ B & Product(F |^ I) = a by Th37;
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then rng F c= A & rng F c= B by A1,XBOOLE_1:1;
then a in gr A & a in gr B by A1,Th37;
hence a in gr A /\ gr B by GROUP_2:99;
end;
hence thesis by GROUP_2:67;
end;
theorem Th43:
the carrier of gr A =
meet{B : ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H}
proof
defpred P[Subgroup of G] means A c= carr $1;
A1: A c= the carrier of G & the carrier of (Omega).G = carr (Omega).G &
(Omega).G = the HGrStr of G by GROUP_2:def 8,def 9;
then A2: ex H being strict Subgroup of G st P[H];
consider H being strict Subgroup of G such that A3: the carrier of H =
meet{B : ex H being strict Subgroup of G
st B = the carrier of H & P[H]} from MeetSbgEx(A2);
set X = {B :ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H};
A4: carr (Omega).G in X by A1;
now let Y;
assume Y in X;
then ex B st Y = B & ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H;
hence A c= Y by GROUP_2:def 9;
end;
then A5: A c= the carrier of H by A3,A4,SETFAM_1:6;
now let H1 be strict Subgroup of G;
assume A6: A c= the carrier of H1;
the carrier of H1 = carr H1 by GROUP_2:def 9;
then the carrier of H1 in X by A6;
then the carrier of H c= the carrier of H1 by A3,SETFAM_1:4;
hence H is Subgroup of H1 by GROUP_2:66;
end;
hence thesis by A3,A5,Def5;
end;
theorem Th44:
gr A = gr(A \ {1.G})
proof
set X = {B : ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H};
set Y = {C : ex H being strict Subgroup of G
st C = the carrier of H & A \ {1.G} c= carr H};
A1: X = Y
proof
thus X c= Y
proof let x;
assume x in X;
then consider B such that A2: x = B and
A3: ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H;
consider H being strict Subgroup of G such that
A4: B = the carrier of H and A5: A c= carr H
by A3
;
A \ {1.G} c= A by XBOOLE_1:36;
then A \ {1.G} c= carr H by A5,XBOOLE_1:1;
hence thesis by A2,A4;
end;
let x;
assume x in Y;
then consider B such that A6: x = B and
A7: ex H being strict Subgroup of G
st B = the carrier of H & A \ {1.G} c= carr H;
consider H being strict Subgroup of G such that
A8: B = the carrier of H and
A9: A \ {1.G} c= carr H by A7;
1.G in H by GROUP_2:55;
then 1.G in carr H by GROUP_2:88;
then {1.G} c= carr H by ZFMISC_1:37;
then A10: (A \ {1.G}) \/ {1.G} c= carr H by A9,XBOOLE_1:8;
now per cases;
suppose 1.G in A;
then {1.G} c= A by ZFMISC_1:37;
hence A c= carr H by A10,XBOOLE_1:45;
suppose not 1.G in A;
hence A c= carr H by A9,ZFMISC_1:65;
end;
hence thesis by A6,A8;
end;
the carrier of gr A = meet X by Th43
.= the carrier of gr(A \ {1.G}) by A1,Th43;
hence thesis by GROUP_2:68;
end;
definition let G,a;
attr a is generating means
:Def6:
not for A st gr A = the HGrStr of G holds gr(A \ {a}) = the HGrStr of G;
end;
canceled;
theorem
1.G is non generating
proof let A;
assume gr A = the HGrStr of G;
hence thesis by Th44;
end;
definition let G, H;
attr H is maximal means
:Def7: the HGrStr of H <> the HGrStr of G &
for K being strict Subgroup of G st
the HGrStr of H <> K & H is Subgroup of K
holds K = the HGrStr of G;
end;
canceled;
theorem Th48:
for G being strict Group, H being strict Subgroup of G,
a being Element of G holds
H is maximal & not a in H implies gr(carr H \/ {a}) = G
proof let G be strict Group, H be strict Subgroup of G,
a be Element of G;
assume that A1: H is maximal and A2: not a in H;
a in {a} by TARSKI:def 1;
then carr H c= carr H \/ {a} & a in carr H \/ {a}
by XBOOLE_0:def 2,XBOOLE_1:7;
then gr carr H is Subgroup of gr(carr H \/ {a}) &
a in gr(carr H \/ {a}) by Th38,Th41;
then H is Subgroup of gr(carr H \/ {a}) & H <> gr(carr H \/ {a})
by A2,Th40;
hence thesis by A1,Def7;
end;
::
:: Frattini subgroup.
::
definition let G be Group;
func Phi(G) -> strict Subgroup of G means
:Def8: the carrier of it =
meet{A where A is Subset of G :
ex H being strict Subgroup of G
st A = the carrier of H & H is maximal} if
ex H being strict Subgroup of G st H is maximal otherwise
it = the HGrStr of G;
existence
proof
defpred P[Subgroup of G] means $1 is maximal;
now per cases;
suppose A1: ex H being strict Subgroup of G st P[H];
ex H being strict Subgroup of G st the carrier of H =
meet{A where A is Subset of
G: ex K being strict Subgroup of G
st A = the carrier of K & P[K]} from MeetSbgEx(A1);
hence thesis by A1;
suppose A2: for H being strict Subgroup of G holds H is not maximal;
(Omega).G = the HGrStr of G &
(Omega).G is Subgroup of G by GROUP_2:def 8;
hence thesis by A2;
end;
hence thesis;
end;
uniqueness by GROUP_2:68;
correctness;
end;
canceled 3;
theorem Th52:
for G being Group holds
(ex H being strict Subgroup of G st H is maximal) implies
(a in Phi(G) iff
for H being strict Subgroup of G st H is maximal holds a in H)
proof let G be Group;
assume A1: ex H being strict Subgroup of G st H is maximal;
set X = {A where A is Subset of
G: ex K being strict Subgroup of G
st A = the carrier of K & K is maximal};
thus a in Phi(G) implies
for H being strict Subgroup of G st H is maximal holds a in H
proof assume a in Phi(G);
then a in the carrier of Phi(G) by RLVECT_1:def 1;
then A2: a in meet X by A1,Def8;
let H be strict Subgroup of G;
assume A3: H is maximal;
the carrier of H = carr H by GROUP_2:def 9;
then carr H in X by A3;
then a in carr H by A2,SETFAM_1:def 1;
hence thesis by GROUP_2:88;
end;
consider H being strict Subgroup of G such that A4: H is maximal by A1;
carr H = the carrier of H by GROUP_2:def 9;
then A5: carr H in X by A4;
assume A6: for H being strict Subgroup of G st H is maximal holds a in H;
now let Y;
assume Y in X;
then consider A being Subset of G such that A7: Y = A and
A8: ex H being strict Subgroup of G
st A = the carrier of H & H is maximal;
consider H being strict Subgroup of G such that
A9: A = the carrier of H & H is maximal by A8;
A = carr H & a in H by A6,A9,GROUP_2:def 9;
hence a in Y by A7,GROUP_2:88;
end;
then a in meet X by A5,SETFAM_1:def 1;
then a in the carrier of Phi(G) by A1,Def8;
hence thesis by RLVECT_1:def 1;
end;
theorem
for G being Group, a being Element of G holds
(for H being strict Subgroup of G holds H is not maximal) implies a in Phi(G)
proof let G be Group, a be Element of G;
assume for H being strict Subgroup of G holds H is not maximal;
then Phi(G) = the HGrStr of G by Def8;
hence thesis by RLVECT_1:def 1;
end;
theorem Th54:
for G being Group, H being strict Subgroup of G holds
H is maximal implies Phi(G) is Subgroup of H
proof let G be Group, H be strict Subgroup of G;
assume H is maximal;
then for a be Element of G
holds a in Phi(G) implies a in H by Th52;
hence thesis by GROUP_2:67;
end;
theorem Th55:
for G being strict Group holds
the carrier of Phi(G) = {a where a is Element of
G: a is non generating}
proof let G be strict Group;
set A = {a where a is Element of G: a is non generating};
thus the carrier of Phi(G) c= A
proof let x;
assume A1: x in the carrier of Phi(G);
assume A2: not x in A;
x in Phi(G) by A1,RLVECT_1:def 1;
then x in G by GROUP_2:49;
then reconsider a = x as Element of G by RLVECT_1:def 1;
a is generating by A2;
then consider B being Subset of G such that
A3: gr B = G and A4: gr(B \ {a}) <> G by Def6;
set M = B \ {a};
defpred P[Subgroup of G] means M c= carr $1 & not a in $1;
consider X such that A5: X c= Subgroups G and
A6: for H being strict Subgroup of G holds
H in X iff P[H] from SubgrSep;
M c= the carrier of gr M by Def5;
then A7: M c= carr gr M by GROUP_2:def 9;
now assume A8: a in gr M;
now let b be Element of G;
b in gr B by A3,RLVECT_1:def 1;
then consider F being FinSequence of the carrier of G,
I such that len I = len F and
A9: rng F c= B and A10: b = Product(F |^ I) by Th37;
rng(F |^ I) c= carr gr M
proof let x;
assume x in rng(F |^ I);
then consider y such that A11: y in dom(F |^ I) and
A12: (F |^ I).y = x by FUNCT_1:def 5;
reconsider y as Nat by A11;
len(F |^ I) = len F by Def4;
then A13: y in dom F by A11,FINSEQ_3:31;
then A14: x = (F/.y) |^ @(I/.y) by A12,Def4;
now per cases;
suppose F/.y = a;
then x in gr M by A8,A14,Th6;
hence thesis by GROUP_2:88;
suppose A15: F/.y <> a;
F/.y = F.y & F.y in rng F
by A13,FINSEQ_4:def 4,FUNCT_1:def 5;
then F/.y in B & not F/.y in {a}
by A9,A15,TARSKI:def 1;
then F/.y in M by XBOOLE_0:def 4;
then F/.y in gr M by Th38;
then x in gr M by A14,Th6;
hence thesis by GROUP_2:88;
end;
hence thesis;
end;
hence b in gr M by A10,Th21;
end;
hence contradiction by A4,GROUP_2:71;
end;
then reconsider X as non empty set by A6,A7;
defpred P[set,set] means
ex H1,H2 being strict Subgroup of G st
$1 = H1 & $2 = H2 & H1 is Subgroup of H2;
A16: now let x be Element of X;
x in Subgroups G by A5,TARSKI:def 3;
hence x is strict Subgroup of G by GROUP_3:def 1;
end;
A17: for x being Element of X holds P[x,x]
proof let x be Element of X;
reconsider H = x as strict Subgroup of G by A16;
H is Subgroup of H by GROUP_2:63;
hence thesis;
end;
A18: for x,y being Element of X st P[x,y] & P[y,x]
holds x = y by GROUP_2:64;
A19: for x,y,z being Element of X st P[x,y] & P[y,z]
holds P[x,z]
proof let x,y,z be Element of X;
given H1,H2 being strict Subgroup of G such that
A20: x = H1 & y = H2 & H1 is Subgroup of H2;
given H3,H4 being strict Subgroup of G such that
A21: y = H3 & z = H4 & H3 is Subgroup of H4;
H1 is Subgroup of H4 by A20,A21,GROUP_2:65;
hence thesis by A20,A21;
end;
A22: for Y st Y c= X &
(for x,y being Element of X st x in Y & y in Y holds
P[x,y] or P[y,x])
ex y being Element of X st
for x being Element of X st x in Y holds P[x,y]
proof let Y;
assume A23: Y c= X;
assume A24: for x,y being Element of X
st x in Y & y in Y holds
P[x,y] or P[y,x];
set C = {D where D is Subset of G :
ex H being strict Subgroup of G st H in Y & D = carr H};
now let Z be set;
assume Z in C;
then ex D being Subset of G st Z = D &
ex H being strict Subgroup of G st H in Y & D = carr H;
hence Z c= the carrier of G;
end;
then reconsider E = union C as Subset of G
by ZFMISC_1:94;
now per cases;
suppose A25: Y = {};
consider y being Element of X;
take y;
let x be Element of X;
assume x in Y;
hence P[x,y] by A25;
suppose A26: Y <> {};
consider s being Element of Y;
A27: s in X by A23,A26,TARSKI:def 3;
then reconsider s as strict Subgroup of G by A5,GROUP_3:def 1;
A28: carr s in C by A26;
then carr s c= E & M c= carr s by A6,A27,ZFMISC_1:92;
then A29: M c= E by XBOOLE_1:1;
carr s <> {} by GROUP_2:87;
then A30: E <> {} by A28,ORDERS_1:91;
A31: now let a,b be Element of G;
assume that A32: a in E and A33: b in E;
consider Z being set such that A34: a in Z and A35: Z in C
by A32,TARSKI:
def 4;
consider D being Subset of G such that
A36: Z = D and
A37: ex H being strict Subgroup of G
st H in Y & D = carr H by A35;
consider H1 being Subgroup of G such that
A38: H1 in Y & D = carr H1 by A37;
consider Z1 being set such that A39: b in Z1 and
A40: Z1 in C by A33,TARSKI:def 4;
consider B being Subset of G such that
A41: Z1 = B and
A42: ex H being strict Subgroup of G
st H in Y & B = carr H by A40;
consider H2 being Subgroup of G such that
A43: H2 in Y & B = carr H2 by A42;
now per cases by A23,A24,A38,A43;
suppose P[H1,H2];
then the carrier of H1 c= the carrier of H2
by GROUP_2:def 5;
then carr H1 c= the carrier of H2 by GROUP_2:def 9;
then carr H1 c= carr H2 by GROUP_2:def 9;
then a * b in carr H2 by A34,A36,A38,A39,A41,A43,
GROUP_2:89;
hence a * b in E by A40,A41,A43,TARSKI:def 4;
suppose P[H2,H1];
then the carrier of H2 c= the carrier of H1
by GROUP_2:def 5;
then carr H2 c= the carrier of H1 by GROUP_2:def 9;
then carr H2 c= carr H1 by GROUP_2:def 9;
then a * b in carr H1 by A34,A36,A38,A39,A41,A43,
GROUP_2:89;
hence a * b in E by A35,A36,A38,TARSKI:def 4;
end;
hence a * b in E;
end;
now let a be Element of G;
assume a in E;
then consider Z being set such that A44: a in Z and
A45: Z in C by TARSKI:def 4;
consider D being Subset of G such that
A46: Z = D and
A47: ex H being strict Subgroup of G
st H in Y & D = carr H by A45;
consider H1 being Subgroup of G such that
A48: H1 in Y & D = carr H1 by A47;
a" in carr H1 by A44,A46,A48,GROUP_2:90;
hence a" in E by A45,A46,A48,TARSKI:def 4;
end;
then consider H being strict Subgroup of G such that
A49: the carrier of H = E by A30,A31,GROUP_2:61;
A50: now assume a in H;
then a in E by A49,RLVECT_1:def 1;
then consider Z being set such that A51: a in Z and
A52: Z in C by TARSKI:def 4;
consider D being Subset of G such that
A53: Z = D and
A54: ex H being strict Subgroup of G
st H in Y & D = carr H by A52;
consider H1 being strict Subgroup of G such that
A55: H1 in Y & D = carr H1 by A54;
not a in H1 by A6,A23,A55;
hence contradiction by A51,A53,A55,GROUP_2:88;
end;
the carrier of H = carr H by GROUP_2:def 9;
then reconsider y = H as Element of X
by A6,A29,A49,A50;
take y;
let x be Element of X;
assume A56: x in Y;
x in Subgroups G by A5,TARSKI:def 3;
then reconsider K = x as strict Subgroup of G by GROUP_3:def 1;
take K,H;
thus x = K & y = H;
carr K = the carrier of K by GROUP_2:def 9;
then the carrier of K in C by A56;
then the carrier of K c= E by ZFMISC_1:92;
hence K is Subgroup of H by A49,GROUP_2:66;
end;
hence thesis;
end;
consider s being Element of X such that
A57: for y being Element of X st s <> y holds not P[s,y]
from Zorn_Max(A17,A18,A19,A22);
reconsider H = s as strict Subgroup of G by A16;
H is maximal
proof
not a in H by A6;
hence the HGrStr of H <> the HGrStr of G by RLVECT_1:def 1;
let K be strict Subgroup of G;
assume that A58: K <> the HGrStr of H and
A59: H is Subgroup of K and
A60: K <> the HGrStr of G;
the carrier of H = carr H & the carrier of K = carr K &
the carrier of H c= the carrier of K & M c= carr H
by A6,A59,GROUP_2:def 5,def 9;
then A61: M c= carr K by XBOOLE_1:1;
now assume a in K;
then a in carr K by GROUP_2:88;
then {a} c= carr K by ZFMISC_1:37;
then A62: M \/ {a} c= carr K by A61,XBOOLE_1:8;
B c= M \/ {a}
proof let x;
assume A63: x in B;
now per cases;
suppose x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
suppose x <> a;
then not x in {a} by TARSKI:def 1;
then x in M by A63,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 2;
end;
hence thesis;
end;
then B c= carr K by A62,XBOOLE_1:1;
then gr B is Subgroup of gr carr K by Th41;
then G is Subgroup of K by A3,Th40;
hence contradiction by A60,GROUP_2:64;
end;
then reconsider v = K as Element of X by A6,A61;
not P[s,v] by A57,A58;
hence thesis by A59;
end;
then Phi(G) is Subgroup of H by Th54;
then the carrier of Phi(G) c= the carrier of H by GROUP_2:def 5;
then x in H & not a in H by A1,A6,RLVECT_1:def 1;
hence thesis;
end;
let x;
assume x in A;
then consider a being Element of G such that
A64: x = a and A65: a is non generating;
now per cases;
suppose for H being strict Subgroup of G holds H is not maximal;
then Phi(G) = G by Def8;
hence thesis by A64;
suppose A66: ex H being strict Subgroup of G st H is maximal;
now let H be strict Subgroup of G;
assume A67: H is maximal;
now assume A68: not a in H;
then A69: gr(carr H \/ {a}) = G by A67,Th48;
A70: carr H misses {a}
proof
thus carr H /\ {a} c= {}
proof let x;
assume x in carr H /\ {a};
then x in carr H & x in {a} by XBOOLE_0:def 3;
then x in carr H & x = a by TARSKI:def 1;
hence thesis by A68,GROUP_2:88;
end;
thus {} c= carr H /\ {a} by XBOOLE_1:2;
end;
(carr H \/ {a}) \ {a} = carr H \ {a} by XBOOLE_1:40
.= carr H by A70,XBOOLE_1:83;
then gr((carr H \/ {a}) \ {a}) = H & H <> G by A67,Def7,Th40;
hence contradiction by A65,A69,Def6;
end;
hence a in H;
end;
then a in Phi(G) by A66,Th52;
hence thesis by A64,RLVECT_1:def 1;
end;
hence thesis;
end;
theorem
for G being strict Group, a being Element of G holds
a in Phi(G) iff a is non generating
proof let G be strict Group, a be Element of G;
thus a in Phi(G) implies a is non generating
proof assume a in Phi(G);
then a in the carrier of Phi(G) by RLVECT_1:def 1;
then a in {b where b is Element of
G: b is non generating} by Th55;
then ex b being Element of G
st a = b & b is non generating;
hence thesis;
end;
assume a is non generating;
then a in
{b where b is Element of G : b is non generating};
then a in the carrier of Phi(G) by Th55;
hence thesis by RLVECT_1:def 1;
end;
definition let G,H1,H2;
func H1 * H2 -> Subset of G equals
:Def9: carr H1 * carr H2;
correctness;
end;
theorem Th57:
H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 &
H1 * H2 = carr H1 * H2
proof
thus H1 * H2 = carr H1 * carr H2 by Def9;
hence thesis by GROUP_2:def 11,def 12;
end;
theorem
H * H = carr H
proof
thus H * H = carr H * carr H by Def9
.= carr H by GROUP_2:91;
end;
theorem
H1 * H2 * H3 = H1 * (H2 * H3)
proof
thus H1 * H2 * H3 = carr H1 * carr H2 * H3 by Def9
.= carr H1 * (carr H2 * H3) by GROUP_2:116
.= carr H1 * (H2 * H3) by Th57
.= H1 * (H2 * H3) by GROUP_2:def 12;
end;
theorem
a * H1 * H2 = a * (H1 * H2)
proof
thus a * H1 * H2 = a * carr H1 * H2 by GROUP_2:def 13
.= a * (carr H1 * H2) by GROUP_3:9
.= a * (H1 * H2) by Th57;
end;
theorem
H1 * H2 * a = H1 * (H2 * a)
proof
thus H1 * H2 * a = H1 * carr H2 * a by Th57
.= H1 * (carr H2 * a) by GROUP_3:14
.= H1 * (H2 * a) by GROUP_2:def 14;
end;
theorem
A * H1 * H2 = A * (H1 * H2)
proof
thus A * H1 * H2 = A * (H1 * carr H2) by GROUP_2:119
.= A * (H1 * H2) by Th57;
end;
theorem
H1 * H2 * A = H1 * (H2 * A)
proof
thus H1 * H2 * A = H1 * carr H2 * A by Th57
.= H1 * (carr H2 * A) by GROUP_2:118
.= H1 * (H2 * A) by GROUP_2:def 12;
end;
theorem Th64:
for N1,N2 being strict normal Subgroup of G
holds N1 * N2 = N2 * N1
proof let N1,N2 be strict normal Subgroup of G;
carr N1 * carr N2 = carr N2 * carr N1 by GROUP_3:148;
then N1 * N2 = carr N2 * carr N1 by Def9;
hence thesis by Def9;
end;
theorem Th65:
G is commutative Group implies H1 * H2 = H2 * H1
proof assume G is commutative Group;
then carr H1 * carr H2 = carr H2 * carr H1 by GROUP_2:29;
then H1 * H2 = carr H2 * carr H1 by Def9;
hence thesis by Def9;
end;
definition let G,H1,H2;
func H1 "\/" H2 -> strict Subgroup of G equals
:Def10: gr(carr H1 \/ carr H2);
correctness;
end;
canceled;
theorem Th67:
a in H1 "\/" H2 iff
ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I)
proof
thus a in H1 "\/" H2 implies
ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I)
proof assume a in H1 "\/" H2;
then a in gr(carr H1 \/ carr H2) by Def10;
hence thesis by Th37;
end;
assume
ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 &
a = Product(F |^ I);
then a in gr(carr H1 \/ carr H2) by Th37;
hence thesis by Def10;
end;
Lm4: for n being natural number holds n mod 2 = 0 or n mod 2 = 1
proof
let n be natural number;
assume A1: n mod 2 <> 0;
2 = 1 + 1 & n mod 2 < 2 by NAT_1:46;
then n mod 2 <= 1 & n mod 2 >= 1 by A1,NAT_1:38,RLVECT_1:98;
hence n mod 2 = 1 by AXIOMS:21;
end;
Lm5:
for k, n being Nat holds (k * n) mod k = 0
proof
let k, n be Nat;
now per cases;
suppose k = 0;
hence thesis by NAT_1:def 2;
suppose k <> 0;
then k * n = k * n + 0 & 0 < k by NAT_1:18;
hence thesis by NAT_1:def 2;
end;
hence thesis;
end;
Lm6:
for k, l being natural number holds k > 1 implies 1 mod k = 1
proof
let k, l be natural number;
assume A1: k > 1;
1 = k * 0 + 1;
hence thesis by A1,NAT_1:def 2;
end;
Lm7:
for k, l, n, m being natural number holds
k mod n = 0 & l = k - m * n implies l mod n = 0
proof
let k, l, n, m be natural number;
assume that A1: k mod n = 0 and A2: l = k - m * n;
now per cases;
suppose n = 0;
hence thesis by A1,A2;
suppose n <> 0;
then consider t being Nat such that
A3: k = n * t + 0 and A4: 0 < n by A1,NAT_1:def 2;
A5: l = n * (t - m) + 0 by A2,A3,XCMPLX_1:40;
now assume t - m < 0;
then l < n * 0 by A4,A5,REAL_1:70;
hence contradiction by NAT_1:18;
end;
then t - m is Nat by INT_1:16;
hence thesis by A4,A5,NAT_1:def 2;
end;
hence thesis;
end;
Lm8: n <> 0 & k mod n = 0 & l < n implies k + l mod n = l
proof assume that A1: n <> 0 and A2: k mod n = 0 and A3: l < n;
consider t being Nat such that A4: k = n * t + 0 and 0 < n
by A1,A2,NAT_1:def 2;
thus thesis by A3,A4,NAT_1:def 2;
end;
Lm9: k mod n = 0 implies k + l mod n = l mod n
proof assume that A1: k mod n = 0;
now per cases;
suppose
A2: n = 0;
hence k + l mod n = 0 by NAT_1:def 2
.= l mod n by A2,NAT_1:def 2;
suppose A3: n <> 0;
then consider m such that A4: k = n * m + 0 & 0 < n by A1,NAT_1:def 2;
consider t being Nat such that
A5: l = n * t + (l mod n) & l mod n < n by A3,NAT_1:def 2;
k + l = n * m + n * t + (l mod n) by A4,A5,XCMPLX_1:1
.= n * (m + t) + (l mod n) by XCMPLX_1:8;
hence thesis by A5,NAT_1:def 2;
end;
hence thesis;
end;
Lm10: k <> 0 implies (k * n) div k = n
proof assume k <> 0;
then k * n = k * n + 0 & 0 < k by NAT_1:18;
hence thesis by NAT_1:def 1;
end;
Lm11: n <> 0 & k mod n = 0 implies
(k + l) div n = (k div n) + (l div n)
proof assume that A1:n <> 0 and A2: k mod n = 0;
A3: 0 <= n by NAT_1:18;
then A4: k = n * (k div n) + 0 by A1,A2,NAT_1:47;
A5: ex t being Nat st l = n * t + (l mod n) & l mod n < n by A1,NAT_1:def 2;
l = n * (l div n) + (l mod n) by A1,A3,NAT_1:47;
then k + l = n * (k div n) + n * (l div n) + (l mod n) by A4,XCMPLX_1:1
.= n * ((k div n) + (l div n)) + (l mod n) by XCMPLX_1:8;
hence thesis by A5,NAT_1:def 1;
end;
theorem
H1 "\/" H2 = gr(H1 * H2)
proof set H = gr(carr H1 * carr H2);
A1: carr H1 * carr H2 = H1 * H2 by Def9;
A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10;
carr H1 \/ carr H2 c= carr H1 * carr H2
proof let x;
assume A3: x in carr H1 \/ carr H2;
then reconsider a = x as Element of G;
now per cases by A3,XBOOLE_0:def 2;
suppose A4: x in carr H1;
1.G in H2 by GROUP_2:55;
then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88;
hence thesis by A4,GROUP_2:12;
suppose A5: x in carr H2;
1.G in H1 by GROUP_2:55;
then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88;
hence thesis by A5,GROUP_2:12;
end;
hence thesis;
end;
then A6: H1 "\/" H2 is Subgroup of H by A2,Th41;
now let a;
assume a in H;
then consider F,I such that A7: len F = len I and
A8: rng F c= carr H1 * carr H2 and A9: a = Product(F |^ I) by Th37;
rng(F |^ I) c= carr(H1 "\/" H2)
proof let x; set f = F |^ I;
assume x in rng f;
then consider y such that A10: y in dom f and
A11: f.y = x by FUNCT_1:def 5;
reconsider y as Nat by A10;
A12: len f = len F by Def4;
then A13: y in dom I by A7,A10,FINSEQ_3:31;
then I.y in rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider i = I.y as Integer by INT_1:12;
A14: y in dom F by A10,A12,FINSEQ_3:31;
I/.y = I.y & @(I/.y) = I/.y by A13,Def2,FINSEQ_4:def 4;
then A15: x = (F/.y) |^ i by A11,A14,Def4;
y in dom F by A10,A12,FINSEQ_3:31;
then F/.y = F.y & F.y in rng F by FINSEQ_4:def 4,FUNCT_1:def 5;
then consider b,c such that A16: F/.y = b * c and
A17: b in carr H1 and A18: c in carr H2 by A8,GROUP_2:12;
now per cases;
suppose i >= 0;
then reconsider n = i as Nat by INT_1:16;
defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = b) &
($1 mod 2 = 0 implies $2 = c);
A19: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds
y1 = y2 by Lm4;
A20: for k st k in Seg(2 * n) ex x st P[k,x]
proof let k;
assume k in Seg(2 * n);
now per cases by Lm4;
suppose A21: k mod 2 = 1;
reconsider x = b as set;
take x;
thus (k mod 2 = 1 implies x = b) &
(k mod 2 = 0 implies x = c) by A21;
suppose A22: k mod 2 = 0;
reconsider x = c as set;
take x;
thus (k mod 2 = 1 implies x = b) &
(k mod 2 = 0 implies x = c) by A22;
end;
hence thesis;
end;
consider p being FinSequence such that
A23: dom p = Seg(2 * n) and
A24: for k st k in
Seg(2 * n) holds P[k,p.k] from SeqEx(A19,A20
);
A25: len p = 2 * n by A23,FINSEQ_1:def 3;
A26: rng p c= {b,c}
proof let x;
assume x in rng p;
then consider y such that A27: y in dom p and A28: p.y = x
by FUNCT_1:def
5;
reconsider y as Nat by A27;
now per cases by Lm4;
suppose y mod 2 = 0;
then x = c by A23,A24,A27,A28;
hence thesis by TARSKI:def 2;
suppose y mod 2 = 1;
then x = b by A23,A24,A27,A28;
hence thesis by TARSKI:def 2;
end;
hence thesis;
end;
then rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p as FinSequence of the carrier of G
by FINSEQ_1:def 4;
defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies
for F1 st F1 = p | Seg $1 holds Product(F1) =
(F/.y) |^ ($1 div 2);
A29: for k st for l st l < k holds Q[l] holds Q[k]
proof let k;
assume A30: for l st l < k holds Q[l];
assume that A31: k <= 2 * n and A32: k mod 2 = 0;
let F1;
assume A33: F1 = p | Seg k;
now per cases;
suppose A34: k = 0;
then F1 = <*> the carrier of G by A33,FINSEQ_1:4,
RELAT_1:110;
then A35: Product F1 = 1.G by Th11;
2 * 0 = 0;
then 0 div 2 = 0 by Lm10;
hence thesis by A34,A35,GROUP_1:43;
suppose k <> 0;
then A36: k >= 1 by RLVECT_1:98;
k <> 1 by A32,Lm6;
then k > 1 by A36,REAL_1:def 5;
then k >= 1 + 1 by NAT_1:38;
then k - 2 >= 2 - 2 by REAL_1:49;
then reconsider m = k - 2 as Nat by INT_1:16;
A37: m + 2 = k by XCMPLX_1:27;
then A38: m < k by RLVECT_1:102;
then A39: m <= 2 * n by A31,AXIOMS:22;
1 * 2 = 2;
then A40: m mod 2 = 0 by A32,Lm7;
reconsider q = p | Seg m
as FinSequence of the carrier of G by FINSEQ_1:23;
A41: Product q = (F/.y) |^ (m div 2)
by A30,A38,A39,A40;
A42: ex j being Nat st 2 * n = k + j by A31,NAT_1:28;
ex o being Nat st 2 * n = m + o by A39,NAT_1:28;
then A43: len F1 = k & len q = m
by A25,A33,A42,FINSEQ_3:59;
then A44: len F1 = m + 2 by XCMPLX_1:27
.= len q + len<* b,c *> by A43,FINSEQ_1:61;
A45: now let l;
assume A46: l in dom q;
then 1 <= l & l <= len q & len q <= len F1
by A37,A43,FINSEQ_3:27,RLVECT_1:102
;
then 1 <= l & l <= len F1 by AXIOMS:22;
then l in dom F1 by FINSEQ_3:27;
then F1.l = p.l & q.l = p.l by A33,A46,FUNCT_1:70;
hence F1.l = q.l;
end;
now let l;
assume l in dom<* b,c *>;
then A47: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now per cases by A47,TARSKI:def 2;
suppose A48: l = 1;
then A49: <* b,c *>.l = b by FINSEQ_1:61;
m + 1 <= k & 1 <= m + 1
by A38,NAT_1:37,38;
then A50: m + 1 in dom F1 by A43,FINSEQ_3:27;
then A51: F1.(len q + l) = p.(m + 1) by A33,A43,
A48,FUNCT_1:70;
A52: m + 1 mod 2 = 1 by A40,Lm8;
dom F1 c= dom p by A33,FUNCT_1:76;
hence F1.(len q + l) = <* b,c *>.l by A23,A24,
A49,A50,A51,A52;
suppose A53: l = 2;
then A54: <* b,c *>.l = c by FINSEQ_1:61;
1 <= m + (1 + 1) by NAT_1:37;
then A55: m + 2 in
dom F1 by A37,A43,FINSEQ_3:27;
then A56: F1.(len q + l) = p.(m + 2) by A33,A43,
A53,FUNCT_1:70;
2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5;
then A57: m + 2 mod 2 = 0 by A40,Lm9;
dom F1 c= dom p by A33,FUNCT_1:76;
hence F1.(len q + l) = <* b,c *>.l by A23,A24,
A54,A55,A56,A57;
end;
hence F1.(len q + l) = <* b,c *>.l;
end;
then F1 = q ^ <* b,c *> by A44,A45,FINSEQ_3:43;
then A58: Product F1 = Product q * Product<* b,c *>
by Th8
.= Product q * (F/.y) by A16,Th13
.= (F/.y) |^ ((m div 2) + 1)
by A41,GROUP_1:49;
m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10
.= k div 2 by A37,A40,Lm11;
hence thesis by A58;
end;
hence thesis;
end;
A59: for k holds Q[k] from Comp_Ind(A29);
A60: 2 * n mod 2 = 0 by Lm5;
A61: 2 * n div 2 = n by Lm10;
len p = 2 * n by A23,FINSEQ_1:def 3;
then p = p | Seg(2 * n) by FINSEQ_3:55;
then A62: x = Product(p) by A15,A59,A60,A61;
b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2
by A17,A18,
XBOOLE_0:def 2;
then {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38;
then A63: rng p c= carr H1 \/ carr H2 by A26,XBOOLE_1:1;
carr H1 \/ carr H2 c=
the carrier of gr(carr H1 \/ carr H2) &
carr gr(carr H1 \/ carr H2) =
the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9;
then rng p c= carr gr(carr H1 \/ carr H2)
by A63,XBOOLE_1:1;
then x in gr(carr H1 \/ carr H2) by A62,Th21;
then x in H1 "\/" H2 by Def10;
hence thesis by GROUP_2:88;
suppose A64: i < 0;
set n = abs( i );
defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = c") &
($1 mod 2 = 0 implies $2 = b");
A65: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds
y1 = y2 by Lm4;
A66: for k st k in Seg(2 * n) ex x st P[k,x]
proof let k;
assume k in Seg(2 * n);
now per cases by Lm4;
suppose A67: k mod 2 = 1;
reconsider x = c" as set;
take x;
thus (k mod 2 = 1 implies x = c") &
(k mod 2 = 0 implies x = b") by A67;
suppose A68: k mod 2 = 0;
reconsider x = b" as set;
take x;
thus (k mod 2 = 1 implies x = c") &
(k mod 2 = 0 implies x = b") by A68;
end;
hence thesis;
end;
consider p being FinSequence such that
A69: dom p = Seg(2 * n) and
A70: for k st k in
Seg(2 * n) holds P[k,p.k] from SeqEx(A65,A66);
A71: len p = 2 * n by A69,FINSEQ_1:def 3;
A72: rng p c= {b",c"}
proof let x;
assume x in rng p;
then consider y such that A73: y in dom p and A74: p.y = x
by FUNCT_1:def 5;
reconsider y as Nat by A73;
now per cases by Lm4;
suppose y mod 2 = 0;
then x = b" by A69,A70,A73,A74;
hence thesis by TARSKI:def 2;
suppose y mod 2 = 1;
then x = c" by A69,A70,A73,A74;
hence thesis by TARSKI:def 2;
end;
hence thesis;
end;
then rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p as FinSequence of the carrier of G
by FINSEQ_1:def 4;
defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies
for F1 st F1 = p | Seg $1 holds
Product(F1) = ((F/.y) |^ ($1 div 2))";
A75: for k st for l st l < k holds Q[l] holds Q[k]
proof let k;
assume A76: for l st l < k holds Q[l];
assume that A77: k <= 2 * n and A78: k mod 2 = 0;
let F1;
assume A79: F1 = p | Seg k;
now per cases;
suppose A80: k = 0;
then F1 = <*> the carrier of G by A79,FINSEQ_1:4,
RELAT_1:110;
then A81: Product F1 = 1.G by Th11;
2 * 0 = 0;
then 0 div 2 = 0 by Lm10;
then (F/.y) |^ (k div 2) = 1.G by A80,GROUP_1:43;
hence thesis by A81,GROUP_1:16;
suppose k <> 0;
then A82: k >= 1 by RLVECT_1:98;
k <> 1 by A78,Lm6;
then k > 1 by A82,REAL_1:def 5;
then k >= 1 + 1 by NAT_1:38;
then k - 2 >= 2 - 2 by REAL_1:49;
then reconsider m = k - 2 as Nat by INT_1:16;
A83: m + 2 = k by XCMPLX_1:27;
then A84: m < k by RLVECT_1:102;
then A85: m <= 2 * n by A77,AXIOMS:22;
1 * 2 = 2;
then A86: m mod 2 = 0 by A78,Lm7;
reconsider q = p | Seg m
as FinSequence of the carrier of G by FINSEQ_1:23;
A87: Product q = ((F/.y) |^ (m div 2))" by A76,A84,A85,A86;
A88: ex j being Nat st 2 * n = k + j by A77,NAT_1:28;
ex o being Nat st 2 * n = m + o by A85,NAT_1:28;
then A89: len F1 = k & len q = m
by A71,A79,A88,FINSEQ_3:59;
then A90: len F1 = m + 2 by XCMPLX_1:27
.= len q + len<* c",b" *> by A89,FINSEQ_1:61;
A91: now let l;
assume A92: l in dom q;
then 1 <= l & l <= len q & len q <= len F1
by A83,A89,FINSEQ_3:27,RLVECT_1:102
;
then 1 <= l & l <= len F1 by AXIOMS:22;
then l in dom F1 by FINSEQ_3:27;
then F1.l = p.l & q.l = p.l by A79,A92,FUNCT_1:70;
hence F1.l = q.l;
end;
now let l;
assume l in dom<* c",b" *>;
then A93: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now per cases by A93,TARSKI:def 2;
suppose A94: l = 1;
then A95: <* c",b" *>.l = c" by FINSEQ_1:61;
m + 1 <= k & 1 <= m + 1
by A84,NAT_1:37,38;
then A96: m + 1 in dom F1 by A89,FINSEQ_3:27;
then A97: F1.(len q + l) = p.(m + 1) by A79,A89,
A94,FUNCT_1:70;
A98: m + 1 mod 2 = 1 by A86,Lm8;
dom F1 c= dom p by A79,FUNCT_1:76;
hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A95,A96,A97,A98;
suppose A99: l = 2;
then A100: <* c",b" *>.l = b" by FINSEQ_1:61;
1 <= m + (1 + 1) by NAT_1:37;
then A101: m + 2 in
dom F1 by A83,A89,FINSEQ_3:27
;
then A102: F1.(len q + l) = p.(m + 2) by A79,A89
,A99,FUNCT_1:70;
2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5;
then A103: m + 2 mod 2 = 0 by A86,Lm9;
dom F1 c= dom p by A79,FUNCT_1:76;
hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A100,A101,A102,A103;
end;
hence F1.(len q + l) = <* c",b" *>.l;
end;
then F1 = q ^ <* c",b" *> by A90,A91,FINSEQ_3:43;
then A104: Product F1 = Product q *
Product<* c",b" *> by Th8
.= Product q * (c" * b") by Th13
.= Product q * (F/.y)"
by A16,GROUP_1:25
.= ((F/.y) * ((F/.y) |^ (m div 2)))"
by A87,GROUP_1:25
.= ((F/.y) |^ ((m div 2) + 1))"
by GROUP_1:49;
m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10
.= k div 2 by A83,A86,Lm11;
hence thesis by A104;
end;
hence thesis;
end;
A105: for k holds Q[k] from Comp_Ind(A75);
A106: 2 * n mod 2 = 0 by Lm5;
A107: 2 * n div 2 = n by Lm10;
len p = 2 * n by A69,FINSEQ_1:def 3;
then A108: p = p | Seg(2 * n) by FINSEQ_3:55;
x = ((F/.y) |^ n)" by A15,A64,GROUP_1:56;
then A109: x = Product(p) by A105,A106,A107,A108;
b" in carr H1 & c" in carr H2 by A17,A18,GROUP_2:90;
then b" in carr H1 \/ carr H2 &
c" in carr H1 \/ carr H2 by XBOOLE_0:def 2;
then {b",c"} c= carr H1 \/ carr H2 by ZFMISC_1:38;
then A110: rng p c= carr H1 \/ carr H2 by A72,XBOOLE_1:1;
carr H1 \/ carr H2 c=
the carrier of gr(carr H1 \/ carr H2) &
carr gr(carr H1 \/ carr H2) =
the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9;
then rng p c= carr gr(carr H1 \/ carr H2)
by A110,XBOOLE_1:1;
then x in gr(carr H1 \/ carr H2) by A109,Th21;
then x in H1 "\/" H2 by Def10;
hence thesis by GROUP_2:88;
end;
hence thesis;
end;
hence a in H1 "\/" H2 by A9,Th21;
end;
then H is Subgroup of H1 "\/" H2 by GROUP_2:67;
hence gr(H1 * H2) = H1 "\/" H2 by A1,A6,GROUP_2:64;
end;
theorem Th69:
H1 * H2 = H2 * H1 implies
the carrier of H1 "\/" H2 = H1 * H2
proof assume H1 * H2 = H2 * H1;
then carr H1 * carr H2 = H2 * H1 by Def9;
then carr H1 * carr H2 = carr H2 * carr H1 by Def9;
then consider H being strict Subgroup of G such that
A1: the carrier of H = carr H1 * carr H2 by GROUP_2:93;
A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10;
carr H1 \/ carr H2 c= carr H1 * carr H2
proof let x;
assume A3: x in carr H1 \/ carr H2;
then reconsider a = x as Element of G;
now per cases by A3,XBOOLE_0:def 2;
suppose A4: x in carr H1;
1.G in H2 by GROUP_2:55;
then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88;
hence thesis by A4,GROUP_2:12;
suppose A5: x in carr H2;
1.G in H1 by GROUP_2:55;
then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88;
hence thesis by A5,GROUP_2:12;
end;
hence thesis;
end;
then A6: H1 "\/" H2 is Subgroup of H by A1,A2,Def5;
now let a;
assume a in H;
then a in carr H1 * carr H2 by A1,RLVECT_1:def 1;
then consider b,c such that A7: a = b * c and
A8: b in carr H1 & c in carr H2 by GROUP_2:12;
reconsider p = 1 as Integer;
A9: len<* b,c *> = 2 & len<* @p,@p *> = 2 by FINSEQ_1:61;
A10: rng<* b,c *> = {b,c} by FINSEQ_2:147;
b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A8,XBOOLE_0:def
2
;
then A11: {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38;
a = Product<* b *> * c by A7,Th12
.= Product<* b *> * Product<* c *> by Th12
.= Product(<* b *> ^ <* c *>) by Th8
.= Product<* b,c *> by FINSEQ_1:def 9
.= Product<* b |^ p, c *> by GROUP_1:44
.= Product<* b |^ p, c |^ p *> by GROUP_1:44
.= Product(<* b,c *> |^ <* @p,@p *>) by Th29;
then a in gr(carr H1 \/ carr H2) by A9,A10,A11,Th37;
hence a in H1 "\/" H2 by Def10;
end;
then H is Subgroup of H1 "\/" H2 by GROUP_2:67;
then H = H1 "\/" H2 & carr H1 * carr H2 = H1 * H2 by A6,Def9,GROUP_2:64;
hence thesis by A1;
end;
theorem
G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2
proof assume G is commutative Group;
then H1 * H2 = H2 * H1 by Th65;
hence thesis by Th69;
end;
theorem Th71:
for N1,N2 being strict normal Subgroup of G
holds the carrier of N1 "\/" N2 = N1 * N2
proof let N1,N2 be strict normal Subgroup of G;
N1 * N2 = N2 * N1 by Th64;
hence thesis by Th69;
end;
theorem
for N1,N2 being strict normal Subgroup of G
holds N1 "\/" N2 is normal Subgroup of G
proof let N1,N2 be strict normal Subgroup of G;
consider N being strict normal Subgroup of G such that
A1: the carrier of N = carr N1 * carr N2 by GROUP_3:149;
the carrier of N1 "\/" N2 = N1 * N2 & N1 * N2 = carr N1 * carr N2
by Th57,Th71;
hence thesis by A1,GROUP_2:68;
end;
theorem Th73:
for H being strict Subgroup of G holds H "\/" H = H
proof let H be strict Subgroup of G;
thus H "\/" H = gr(carr H \/ carr H) by Def10
.= H by Th40;
end;
theorem Th74:
H1 "\/" H2 = H2 "\/" H1
proof
thus H1 "\/" H2 = gr(carr H2 \/ carr H1) by Def10
.= H2 "\/" H1 by Def10;
end;
Lm12: H1 is Subgroup of H1 "\/" H2
proof carr H1 c= carr H1 \/ carr H2 &
carr H1 \/ carr H2 c= the carrier of gr(carr H1 \/ carr H2) &
H1 "\/" H2 = gr(carr H1 \/ carr H2) &
the carrier of H1 = carr H1 by Def5,Def10,GROUP_2:def 9,XBOOLE_1:7;
then the carrier of H1 c= the carrier of H1 "\/" H2 by XBOOLE_1:1;
hence thesis by GROUP_2:66;
end;
Lm13: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
proof
now let a;
assume a in H1 "\/" H2 "\/" H3;
then consider F,I such that A1: len F = len I and
A2: rng F c= carr(H1 "\/" H2) \/ carr H3 and
A3: a = Product(F |^ I) by Th67;
rng F c= carr gr(carr H1 \/ carr(H2 "\/" H3))
proof let x;
assume
A4: x in rng F;
now per cases by A2,A4,XBOOLE_0:def 2;
suppose A5: x in carr(H1 "\/" H2);
then A6: x in H1 "\/" H2 by GROUP_2:88;
reconsider b = x as Element of G by A5;
consider F1,I1 such that A7: len F1 = len I1 and
A8: rng F1 c= carr H1 \/ carr H2 and
A9: b = Product(F1 |^ I1) by A6,Th67;
H2 is Subgroup of H2 "\/" H3 by Lm12;
then the carrier of H2 c= the carrier of H2 "\/" H3 &
the carrier of H2 = carr H2 &
the carrier of H3 = carr H3 &
H2 "\/" H3 = gr(carr H2 \/ carr H3)
by Def10,GROUP_2:def 5,def 9;
then carr H2 c= carr(H2 "\/" H3) by GROUP_2:def 9;
then carr H1 \/ carr H2 c= carr H1 \/ carr(H2 "\/" H3)
by XBOOLE_1:9;
then rng F1 c= carr H1 \/ carr(H2 "\/" H3) by A8,XBOOLE_1:1;
then b in H1 "\/" (H2 "\/" H3) by A7,A9,Th67;
then x in gr(carr H1 \/ carr(H2 "\/" H3)) by Def10;
hence thesis by GROUP_2:88;
suppose x in carr H3;
then x in H3 & H3 is Subgroup of H3 "\/" H2 by Lm12,GROUP_2:88;
then x in H3 "\/" H2 by GROUP_2:49;
then x in H2 "\/" H3 by Th74;
then x in carr(H2 "\/" H3) by GROUP_2:88;
then x in carr H1 \/ carr(H2 "\/" H3) &
carr H1 \/ carr(H2 "\/" H3)
c= the carrier of gr(carr H1 \/ carr(H2 "\/" H3))
by Def5,XBOOLE_0:def 2
;
then x in the carrier of gr(carr H1 \/ carr(H2 "\/" H3));
hence thesis by GROUP_2:def 9;
end;
hence thesis;
end;
then a in gr carr gr(carr H1 \/ carr(H2 "\/" H3)) by A1,A3,Th37;
then a in gr(carr H1 \/ carr(H2 "\/" H3)) by Th40;
hence a in H1 "\/" (H2 "\/" H3) by Def10;
end;
hence thesis by GROUP_2:67;
end;
theorem Th75:
H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3)
proof A1: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm13;
H2 "\/" H3 "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) by Lm13;
then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" H1 "\/" H2 &
H3 "\/" H1 "\/" H2 is Subgroup of H3 "\/" (H1 "\/" H2) by Lm13,Th74;
then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:65;
then H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by Th74;
then H1 "\/" (H2 "\/" H3) is Subgroup of H1 "\/" H2 "\/" H3 by Th74;
hence thesis by A1,GROUP_2:64;
end;
theorem
for H being strict Subgroup of G holds
(1).G "\/" H = H & H "\/" (1).G = H
proof let H be strict Subgroup of G;
A1: carr(1).G = the carrier of (1).G by GROUP_2:def 9
.= {1.G} by GROUP_2:def 7;
1.G in H by GROUP_2:55;
then 1.G in carr H by GROUP_2:88;
then {1.G} c= carr H by ZFMISC_1:37;
then A2: {1.G} \/ carr H = carr H by XBOOLE_1:12;
thus (1).G "\/" H = gr(carr(1).G \/ carr H) by Def10
.= H by A1,A2,Th40;
hence thesis by Th74;
end;
theorem Th77:
(Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G
proof
A1: [#] the carrier of G = the carrier of the HGrStr of G by SUBSET_1:def 4
.= the carrier of (Omega).G by GROUP_2:def 8;
A2: carr (Omega).G = the carrier of (Omega).G by GROUP_2:def 9;
(the carrier of (Omega).
G) \/ carr H = [#] the carrier of G by A1,SUBSET_1:28;
hence (Omega).G "\/" H = gr carr (Omega).G by A1,A2,Def10
.= (Omega).G by Th40;
hence thesis by Th74;
end;
theorem Th78:
H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2
proof H1 "\/" H2 = H2 "\/" H1 by Th74;
hence thesis by Lm12;
end;
theorem Th79:
for H2 being strict Subgroup of G holds
H1 is Subgroup of H2 iff H1 "\/" H2 = H2
proof let H2 be strict Subgroup of G;
thus H1 is Subgroup of H2 implies H1 "\/" H2 = H2
proof assume H1 is Subgroup of H2;
then A1: the carrier of H1 c= the carrier of H2 &
the carrier of H1 = carr H1 & carr H2 = the carrier of H2
by GROUP_2:def 5,def 9;
thus H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10
.= gr carr H2 by A1,XBOOLE_1:12
.= H2 by Th40;
end;
thus thesis by Th78;
end;
theorem
H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3
proof H2 is Subgroup of H2 "\/" H3 by Th78;
hence thesis by GROUP_2:65;
end;
theorem
for H3 being strict Subgroup of G holds
H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/"
H2 is Subgroup of H3
proof let H3 be strict Subgroup of G;
assume that A1: H1 is Subgroup of H3 and A2: H2 is Subgroup of H3;
now let a;
assume a in H1 "\/" H2;
then consider F,I such that A3: len F = len I &
rng F c= carr H1 \/ carr H2 & a = Product(F |^ I) by Th67;
the carrier of H1 c= the carrier of H3 &
the carrier of H2 c= the carrier of H3 &
the carrier of H1 = carr H1 & the carrier of H2 = carr H2 &
the carrier of H3 = carr H3 by A1,A2,GROUP_2:def 5,def 9;
then carr H1 \/ carr H2 c= carr H3 by XBOOLE_1:8;
then rng F c= carr H3 by A3,XBOOLE_1:1;
then a in gr carr H3 by A3,Th37;
hence a in H3 by Th40;
end;
hence thesis by GROUP_2:67;
end;
theorem
for H3,H2 being strict Subgroup of G holds
H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3
proof let H3,H2 be strict Subgroup of G;
assume A1: H1 is Subgroup of H2;
(H1 "\/" H3) "\/" (H2 "\/" H3) = H1 "\/" H3 "\/" H2 "\/" H3 by Th75
.= H1 "\/" (H3 "\/" H2) "\/" H3 by Th75
.= H1 "\/" (H2 "\/" H3) "\/" H3 by Th74
.= H1 "\/" H2 "\/" H3 "\/" H3 by Th75
.= H2 "\/" H3 "\/" H3 by A1,Th79
.= H2 "\/" (H3 "\/" H3) by Th75
.= H2 "\/" H3 by Th73;
hence thesis by Th79;
end;
theorem
H1 /\ H2 is Subgroup of H1 "\/" H2
proof H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2
by Th78,GROUP_2:106;
hence thesis by GROUP_2:65;
end;
theorem Th84:
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
proof let H2 be strict Subgroup of G;
H1 /\ H2 is Subgroup of H2 by GROUP_2:106;
hence thesis by Th79;
end;
theorem Th85:
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
proof let H1 be strict Subgroup of G;
H1 is Subgroup of H1 "\/" H2 by Th78;
hence thesis by GROUP_2:107;
end;
theorem
for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1
proof let H1,H2 be strict Subgroup of G;
(H1 "\/" H2 = H2 iff H1 is Subgroup of H2) &
(H1 /\ H2 = H1 iff H1 is Subgroup of H2) by Th79,GROUP_2:107;
hence thesis;
end;
reserve S1,S2 for Element of Subgroups G;
definition let G;
func SubJoin G -> BinOp of Subgroups G means
:Def11: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 "\/" H2;
existence
proof
defpred P[set,set,set] means
for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 "\/" H2;
A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B]
proof let S1,S2;
reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1;
reconsider C = H1 "\/" H2 as Element of Subgroups(G)
by GROUP_3:def 1;
take C;
thus thesis;
end;
ex o being BinOp of Subgroups G st
for a,b being Element of Subgroups G holds P[a,b,o.(a,b)]
from BinOpEx(A1);
hence thesis;
end;
uniqueness
proof let o1,o2 be BinOp of Subgroups(G);
assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 "\/"
H2;
assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 "\/"
H2;
now let x,y be set;
assume A4: x in Subgroups(G) & y in Subgroups(G);
then reconsider A = x, B = y as Element of Subgroups(G);
reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1;
o1.(A,B) = H1 "\/" H2 & o2.(A,B) = H1 "\/" H2 by A2,A3;
then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
by BINOP_1:def 1;
hence o1.[x,y] = o2.[x,y];
end;
hence thesis by FUNCT_2:118;
end;
end;
definition let G;
func SubMeet G -> BinOp of Subgroups G means
:Def12: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 /\ H2;
existence
proof
defpred P[set,set,set] means
for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 /\ H2;
A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B]
proof let S1,S2;
reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1;
reconsider C = H1 /\ H2 as Element of Subgroups(G)
by GROUP_3:def 1;
take C;
thus thesis;
end;
ex o being BinOp of Subgroups G st
for a,b being Element of Subgroups G holds P[a,b,o.(a,b)]
from BinOpEx(A1);
hence thesis;
end;
uniqueness
proof let o1,o2 be BinOp of Subgroups(G);
assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 /\
H2;
assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 /\
H2;
now let x,y be set;
assume A4: x in Subgroups(G) & y in Subgroups(G);
then reconsider A = x, B = y as Element of Subgroups(G);
reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1;
o1.(A,B) = H1 /\ H2 & o2.(A,B) = H1 /\ H2 by A2,A3;
then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
by BINOP_1:def 1;
hence o1.[x,y] = o2.[x,y];
end;
hence thesis by FUNCT_2:118;
end;
end;
Lm14: for G being Group holds
LattStr (# Subgroups G, SubJoin G, SubMeet G #) is Lattice &
LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 0_Lattice &
LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 1_Lattice
proof let G be Group;
set L = LattStr (# Subgroups G, SubJoin G, SubMeet G #);
A1: now let A,B be Element of L;
let H1,H2 be Subgroup of G;
assume A2: A = H1 & B = H2;
reconsider A'= A, B'= B as Element of Subgroups G;
thus A "/\" B = SubMeet(G).(A',B') by LATTICES:def 2
.= H1 /\ H2 by A2,Def12;
end;
A3: now let A,B be Element of L;
let H1,H2 be Subgroup of G;
assume A4: A = H1 & B = H2;
reconsider A'= A, B'= B as Element of Subgroups G;
thus A "\/" B = SubJoin(G).(A',B') by LATTICES:def 1
.= H1 "\/" H2 by A4,Def11;
end;
now let A,B,C be Element of L;
reconsider H1 = A, H2 = B, H3 = C as strict Subgroup of G
by GROUP_3:def 1;
thus A "\/" B = H1 "\/" H2 by A3
.= H2 "\/" H1 by Th74
.= B "\/" A by A3;
A5: H1 "\/" H2 = A "\/" B & H2 "\/" H3 = B "\/" C by A3;
hence A "\/" B "\/" C = H1 "\/" H2 "\/" H3 by A3
.= H1 "\/" (H2 "\/" H3) by Th75
.= A "\/" (B "\/" C) by A3,A5;
A6: H1 /\ H2 = A "/\" B by A1;
hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A3
.= B by Th84;
thus A "/\" B = H2 /\ H1 by A1
.= B "/\" A by A1;
A7: H2 /\ H3 = B "/\" C by A1;
thus A "/\" B "/\" C = H1 /\ H2 /\ H3 by A1,A6
.= H1 /\ (H2 /\ H3) by GROUP_2:102
.= A "/\" (B "/\" C) by A1,A7;
thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A1,A5
.= A by Th85;
end;
then A8: L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence L is Lattice by LATTICES:def 10;
reconsider L as Lattice by A8,LATTICES:def 10;
reconsider E = (1).G as Element of L by GROUP_3:def 1;
now let A be Element of L;
reconsider H = A as Subgroup of G by GROUP_3:def 1;
thus E "/\" A = (1).G /\ H by A1
.= E by GROUP_2:103;
hence A "/\" E = E;
end;
hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 0_Lattice
by LATTICES:def 13;
reconsider F = (Omega).G as Element of L by GROUP_3:def 1;
now let A be Element of L;
reconsider H = A as Subgroup of G by GROUP_3:def 1;
thus F "\/" A = (Omega).G "\/" H by A3
.= F by Th77;
hence A "\/" F = F;
end;
hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 1_Lattice
by LATTICES:def 14;
end;
definition let G be Group;
func lattice G -> strict Lattice equals
:Def13: LattStr (# Subgroups G, SubJoin G, SubMeet G #);
coherence by Lm14;
end;
canceled 5;
theorem Th92:
for G being Group holds
the carrier of lattice G = Subgroups G
proof let G be Group;
lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
hence thesis;
end;
theorem Th93:
for G being Group holds
the L_join of lattice G = SubJoin G
proof let G be Group;
lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
hence thesis;
end;
theorem Th94:
for G being Group holds
the L_meet of lattice G = SubMeet G
proof let G be Group;
lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
hence thesis;
end;
definition let G be Group;
cluster lattice G -> lower-bounded upper-bounded;
coherence
proof
A1: lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
hence lattice G is lower-bounded by Lm14;
thus lattice G is upper-bounded by A1,Lm14;
end;
end;
canceled 3;
theorem
for G being Group holds Bottom lattice G = (1).G
proof let G be Group;
A1: the carrier of lattice G = Subgroups G by Th92;
set L = lattice G;
reconsider E = (1).G as Element of L by A1,GROUP_3:def 1;
now let A be Element of L;
reconsider H = A as Subgroup of G by A1,GROUP_3:def 1;
thus A "/\" E = (the L_meet of lattice G).(A,E) by LATTICES:def 2
.= SubMeet(G).(A,E) by Th94
.= H /\ (1).G by A1,Def12
.= E by GROUP_2:103;
end;
hence thesis by RLSUB_2:84;
end;
theorem
for G being Group holds Top lattice G = (Omega).G
proof let G be Group;
A1: the carrier of lattice G = Subgroups G by Th92;
set L = lattice G;
reconsider E = (Omega).
G as Element of L by A1,GROUP_3:def 1;
now let A be Element of L;
reconsider H = A as Subgroup of G by A1,GROUP_3:def 1;
thus A "\/" E = (the L_join of lattice G).(A,E) by LATTICES:def 1
.= SubJoin(G).(A,E) by Th93
.= H "\/" (Omega).G by A1,Def11
.= E by Th77;
end;
hence thesis by RLSUB_2:85;
end;
::
:: Auxiliary theorems.
::
reserve k, l, m, n for natural number;
theorem
n mod 2 = 0 or n mod 2 = 1 by Lm4;
theorem
for k, n being Nat holds (k * n) mod k = 0 by Lm5;
theorem
k > 1 implies 1 mod k = 1 by Lm6;
theorem
k mod n = 0 & l = k - m * n implies l mod n = 0 by Lm7;
reserve k, n, l, m for Nat;
theorem
n <> 0 & k mod n = 0 & l < n implies k + l mod n = l by Lm8;
theorem
k mod n = 0 implies k + l mod n = l mod n by Lm9;
theorem
n <> 0 & k mod n = 0 implies
(k + l) div n = (k div n) + (l div n) by Lm11;
theorem
k <> 0 implies (k * n) div k = n by Lm10;