:: Lattice of Subgroups of a Group. Frattini Subgroup
:: by Wojciech A. Trybulec
::
:: Received August 22, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_1, GROUP_1, STRUCT_0, GROUP_2,
SETFAM_1, SUBSET_1, RELAT_1, INT_1, TARSKI, GROUP_3, QC_LANG1, NEWTON,
ARYTM_3, CARD_1, XXREAL_0, COMPLEX1, ALGSTR_0, CARD_3, FINSOP_1, BINOP_1,
ORDINAL4, SETWISEO, FINSEQ_2, NAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
ZFMISC_1, RLSUB_1, BVFUNC_2, EQREL_1, PRE_TOPC, RLSUB_2, LATTICES,
GROUP_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, FINSOP_1, ORDINAL1,
NUMBERS, INT_1, SETWISEO, SETFAM_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_2,
GROUP_3, LATTICES, GROUP_1, DOMAIN_1, XXREAL_0, NAT_1, INT_2;
constructors PARTFUN1, SETFAM_1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, NAT_D,
FINSEQ_3, FINSEQ_4, FINSOP_1, REALSET1, REAL_1, LATTICES, GROUP_3,
RELSET_1, FINSEQ_2, BINOP_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, INT_1,
FINSEQ_1, STRUCT_0, LATTICES, GROUP_1, GROUP_2, GROUP_3, ORDINAL1,
CARD_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities GROUP_2, SUBSET_1, ALGSTR_0;
expansions TARSKI, XBOOLE_0;
theorems BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSOP_1, FUNCT_1,
GROUP_1, GROUP_2, GROUP_3, INT_1, LATTICES, NAT_1, RLSUB_2, SETFAM_1,
SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1,
XREAL_1, XXREAL_0, NAT_D, STRUCT_0, PARTFUN1, ABSVALUE, CARD_1;
schemes BINOP_1, DOMAIN_1, FINSEQ_1, FINSEQ_2, NAT_1, ORDERS_1, XBOOLE_0,
XFAMILY;
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; :: redefines - (FINSEQ_3, definition)
coherence by FINSEQ_3:86;
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;
A3: carr T in X by A2;
then reconsider Y = meet X as Subset of G() by SETFAM_1:7;
A4: now
let a be Element of G();
assume
A5: a in Y;
now
let Z be set;
assume
A6: Z in X;
then consider A being Subset of G() such that
A7: A = Z and
A8: ex H being strict Subgroup of G() st A = the carrier of H & P[H ];
consider H being Subgroup of G() such that
A9: A = the carrier of H and
P[H] by A8;
a in the carrier of H by A5,A6,A7,A9,SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a" in H by GROUP_2:51;
hence a" in Z by A7,A9,STRUCT_0:def 5;
end;
hence a" in Y by A3,SETFAM_1:def 1;
end;
A10: now
let a,b be Element of G();
assume that
A11: a in Y and
A12: b in Y;
now
let Z be set;
assume
A13: Z in X;
then consider A being Subset of G() such that
A14: A = Z and
A15: ex H being strict Subgroup of G() st A = the carrier of H & P[H ];
consider H being Subgroup of G() such that
A16: A = the carrier of H and
P[H] by A15;
b in the carrier of H by A12,A13,A14,A16,SETFAM_1:def 1;
then
A17: b in H by STRUCT_0:def 5;
a in the carrier of H by A11,A13,A14,A16,SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a * b in H by A17,GROUP_2:50;
hence a * b in Z by A14,A16,STRUCT_0:def 5;
end;
hence a * b in Y by A3,SETFAM_1:def 1;
end;
now
let Z be set;
assume Z in X;
then consider A being Subset of G() such that
A18: Z = A and
A19: ex K being strict Subgroup of G() st A = the carrier of K & P[K];
consider H being Subgroup of G() such that
A20: A = the carrier of H and
P[H] by A19;
1_G() in H by GROUP_2:46;
hence 1_G() in Z by A18,A20,STRUCT_0:def 5;
end;
then Y <> {} by A3,SETFAM_1:def 1;
hence thesis by A10,A4,GROUP_2:52;
end;
reserve x,y,X,Y for set,
k,l,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[object] means ex H being Subgroup of G() st $1 = H & P[H];
consider X such that
A1: for x being object holds x in X iff x in Subgroups G() & R[x]
from XBOOLE_0:sch 1;
take X;
thus X c= Subgroups G()
by A1;
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;
A2: H in Subgroups G() by GROUP_3:def 1;
assume P[H];
hence thesis by A1,A2;
end;
definition
let i;
func @i -> Element of INT equals
i;
coherence by INT_1:def 2;
end;
theorem Th1:
a = h implies a |^ n = h |^ n
proof
defpred P[Nat] means a |^ $1 = h |^ $1;
assume
A1: a = h;
A2: now
let n;
assume
A3: P[n];
a |^ (n + 1) = a |^ n * a by GROUP_1:34
.= h |^ n * h by A1,A3,GROUP_2:43
.= h |^ (n + 1) by GROUP_1:34;
hence P[n+1];
end;
a |^ 0 = 1_G by GROUP_1:25
.= 1_H by GROUP_2:44
.= h |^ 0 by GROUP_1:25;
then
A4: P[0];
for n holds P[n] from NAT_1:sch 2(A4,A2);
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 |^ |.i.| by ABSVALUE:def 1
.= h |^ |.i.| by A1,Th1
.= h |^ i by A2,ABSVALUE:def 1;
end;
suppose
A3: i < 0;
A4: a |^ |.i.| = h |^ |.i.| by A1,Th1;
thus a |^ i = (a |^ |.i.|)" by A3,GROUP_1:30
.= (h |^ |.i.|)" by A4,GROUP_2:48
.= h |^ i by A3,GROUP_1:30;
end;
end;
hence thesis;
end;
theorem Th3:
a in H implies a |^ n in H
proof
defpred P[Nat] means a |^ $1 in H;
assume
A1: a in H;
A2: now
let n;
A3: a |^ (n + 1) = a |^ n * a by GROUP_1:34;
assume P[n];
hence P[n+1] by A1,A3,GROUP_2:50;
end;
a |^ 0 = 1_G by GROUP_1:25;
then
A4: P[0] by GROUP_2:46;
for n holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th4:
a in H implies a |^ i in H
proof
assume
A1: a in H;
now
per cases;
suppose
i >= 0;
then a |^ i = a |^ |.i.| by ABSVALUE:def 1;
hence thesis by A1,Th3;
end;
suppose
i < 0;
then
A2: a |^ i = (a |^ |.i.|)" by GROUP_1:30;
a |^ |.i.| in H by A1,Th3;
hence thesis by A2,GROUP_2:51;
end;
end;
hence thesis;
end;
definition
let G be non empty multMagma;
let F be FinSequence of the carrier of G;
func Product F -> Element of G equals
(the multF of G) "**" F;
correctness;
end;
theorem
for G being associative unital non empty multMagma,
F1,F2 being FinSequence of the carrier of G holds
Product(F1 ^ F2) = Product(F1) * Product(F2) by FINSOP_1:5;
theorem
for G being unital non empty multMagma, F being FinSequence of the
carrier of G, a being Element of G holds Product(F ^ <* a *>) = Product(F) * a
by FINSOP_1:4;
theorem
for G being associative unital non empty multMagma, F being
FinSequence of the carrier of G, a being Element of G holds Product(<* a *> ^ F
) = a * Product(F) by FINSOP_1:6;
theorem Th8:
for G being unital non empty multMagma holds Product <*> the
carrier of G = 1_G
proof
let G be unital non empty multMagma;
set g = the multF of G;
len <*> the carrier of G = 0 & g is having_a_unity;
hence Product <*> the carrier of G = the_unity_wrt g by FINSOP_1:def 1
.= 1_G by GROUP_1:22;
end;
theorem
for G being non empty multMagma, a being Element of G holds Product<*
a *> = a by FINSOP_1:11;
theorem
for G being non empty multMagma, a,b being Element of G holds Product
<* a,b *> = a * b by FINSOP_1:12;
theorem
Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c)
proof
A1: Product<* a *> = a & Product<* c *> = c by FINSOP_1:11;
A2: Product<* a,b *> = a * b & Product<* b,c *> = b * c by FINSOP_1:12;
<* a,b,c *> = <* a *> ^ <* b,c *> & <* a,b,c *> = <* a,b *> ^ <* c *> by
FINSEQ_1:43;
hence thesis by A1,A2,FINSOP_1:5;
end;
Lm1: now
let G,a;
thus Product(0 |-> a) = Product <*> the carrier of G .= 1_G by Th8
.= a |^ 0 by GROUP_1:25;
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:60
.= Product(n |-> a) * Product<* a *> by FINSOP_1:5
.= a |^ n * a by A1,FINSOP_1:11
.= a |^ (n + 1) by GROUP_1:34;
end;
theorem
Product(n |-> a) = a |^ n
proof
defpred P[Nat] means Product($1 |-> a) = a |^ $1;
A1: for n being Nat st P[n] holds P[n+1] by Lm2;
A2: P[0] by Lm1;
for n being Nat holds P[n] from NAT_1:sch 2(A2,A1);
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: for F,a st P[F] holds P[F ^ <* a *>]
proof
let F,a;
assume
A2: P[F];
A3: Product((F ^ <* a *>) - {1_G}) = Product(((F - {1_G}) ^ (<* a *> - {
1_G}))) by FINSEQ_3:73
.= Product F * Product(<* a *> - {1_G}) by A2,FINSOP_1:5;
now
per cases;
suppose
A4: a = 1_G;
then a in {1_G} by TARSKI:def 1;
then <* a *> - {1_G} = <*> the carrier of G by FINSEQ_3:76;
then Product(<* a *> - {1_G}) = 1_G by Th8;
hence thesis by A3,A4,FINSOP_1:4;
end;
suppose
a <> 1_G;
then not a in {1_G} by TARSKI:def 1;
then <* a *> - {1_G} = <* a *> by FINSEQ_3:75;
hence thesis by A3,FINSOP_1:5;
end;
end;
hence thesis;
end;
A5: P[<*> the carrier of G] by FINSEQ_3:74;
for F holds P[F] from FINSEQ_2:sch 2(A5,A1);
hence thesis;
end;
Lm3: for F1 being FinSequence, y being Element of NAT st y in dom F1 holds len
F1 - y + 1 is Element of NAT & len F1 - y + 1 >= 1 & len F1 - y + 1 <= len F1
proof
let F1 be FinSequence, y be Element of NAT;
assume
A1: y in dom F1;
now
assume len F1 - y + 1 < 0;
then 1 < 0 qua Nat - (len F1 - y) by XREAL_1:20;
then 1 < y - len F1;
then
A2: len F1 + 1 < y by XREAL_1:20;
y <= len F1 by A1,FINSEQ_3:25;
hence contradiction by A2,NAT_1:12;
end;
then reconsider n = len F1 - y + 1 as Element of NAT by INT_1:3;
y >= 1 by A1,FINSEQ_3:25;
then n - 1 - y <= len F1 - y - 1 by XREAL_1:13;
then
A3: n - (y + 1) <= len F1 - (y + 1);
y + 0 <= len F1 by A1,FINSEQ_3:25;
then 0 + 1 = 1 & 0 <= len F1 - y by XREAL_1:19;
hence thesis by A3,XREAL_1:6,9;
end;
theorem Th14:
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: for n st P[n] holds P[n + 1]
proof
let n;
assume
A2: P[n];
let F1,F2;
assume that
A3: len F1 = n + 1 and
A4: 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:18
;
deffunc F(Nat) = F2.($1 + 1);
consider q being FinSequence such that
A6: len q = len p and
A7: for k be Nat st k in dom q holds q.k = F(k) from FINSEQ_1:sch 2;
A8: dom q = dom p by A6,FINSEQ_3:29;
A9: len p = n by A3,FINSEQ_3:53;
A10: rng q c= the carrier of G
proof
let x be object;
assume x in rng q;
then consider y being object such that
A11: y in dom q and
A12: x = q.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A11;
y <= len p by A6,A11,FINSEQ_3:25;
then 1 <= y + 1 & y + 1 <= len F2 by A3,A4,A9,NAT_1:12,XREAL_1:7;
then
A13: y + 1 in dom F2 by FINSEQ_3:25;
x = F2.(y + 1) by A7,A11,A12;
then
A14: x in rng F2 by A13,FUNCT_1:def 3;
rng F2 c= the carrier of G by FINSEQ_1:def 4;
hence thesis by A14;
end;
A15: rng F1 c= the carrier of G by FINSEQ_1:def 4;
1 <= n + 1 by NAT_1:12;
then n + 1 in dom F1 by A3,FINSEQ_3:25;
then F1.(n + 1) in rng F1 by FUNCT_1:def 3;
then reconsider a = F1.(n + 1) as Element of G by A15;
A16: F1 = p ^ <* a *> by A3,FINSEQ_3:55;
A17: now
let k;
assume k in dom<* a" *>;
then
A18: k in {1} by FINSEQ_1:2,def 8;
len F2 >= 1 by A3,A4,NAT_1:12;
then
A19: len F2 in dom F1 by A4,FINSEQ_3:25;
then F2.(len F1 - len F1 + 1) = (F1/.len F1)" by A4,A5;
then (F1/.len F1)" = F2.k by A18,TARSKI:def 1;
then
A20: F2.k = a" by A3,A4,A19,PARTFUN1:def 6;
k = 1 by A18,TARSKI:def 1;
hence <* a" *>.k = F2.k by A20;
end;
reconsider q as FinSequence of the carrier of G by A10,FINSEQ_1:def 4;
now
let k;
assume
A21: k in dom p;
then reconsider i = len p - k + 1 as Element of NAT by Lm3;
A22: i + 1 = len F1 - k + 1 by A3,A9;
1 <= i & i <= len p by A21,Lm3;
then i in dom p by FINSEQ_3:25;
then
A23: q.i = F2.(i + 1) by A7,A8;
k <= len p by A21,FINSEQ_3:25;
then
A24: k <= len F1 by A3,A9,NAT_1:12;
1 <= k by A21,FINSEQ_3:25;
then
A25: k in dom F1 by A24,FINSEQ_3:25;
then F1/.k = F1.k by PARTFUN1:def 6
.= p.k by A21,FUNCT_1:47
.= p/.k by A21,PARTFUN1:def 6;
hence q.(len p - k + 1) = (p/.k)" by A5,A23,A25,A22;
end;
then
A26: Product p = Product q" by A2,A9,A6;
A27: now
let k;
A28: len<* a" *> = 1 by FINSEQ_1:39;
assume k in dom q;
hence F2.(len<* a" *> + k) = q.k by A7,A28;
end;
len F2 = len<* a" *> + len q by A3,A4,A9,A6,FINSEQ_1:39;
then F2 = <* a" *> ^ q by A17,A27,FINSEQ_3:38;
then Product F2 = a" * Product q by FINSOP_1:6
.= a" * Product p" by A26
.= (Product p * a)" by GROUP_1:17;
hence thesis by A16,FINSOP_1:4;
end;
A29: P[0]
proof
let F1,F2;
assume that
A30: len F1 = 0 and
A31: len F1 = len F2;
F1 = <*> the carrier of G by A30;
then
A32: Product F1 = 1_G by Th8;
F2 = <*> the carrier of G by A30,A31;
then Product F2 = 1_G by Th8;
hence thesis by A32,GROUP_1:8;
end;
for k holds P[k] from NAT_1:sch 2(A29,A1);
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 multF of G;
assume G is commutative Group;
then g is commutative by GROUP_3:2;
hence thesis by FINSOP_1:7;
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 multF of G;
assume G is commutative Group;
then g is commutative by GROUP_3:2;
hence thesis by FINSOP_1:8;
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 multF of G;
assume G is commutative Group;
then
A1: g is commutative by GROUP_3:2;
assume that
A2: len F = len F1 and
A3: len F = len F2;
assume
A4: for k st k in dom F holds F.k = (F1/.k) * (F2/.k);
now
A5: dom F2 = Seg len F2 by FINSEQ_1:def 3;
A6: dom F1 = Seg len F1 by FINSEQ_1:def 3;
let k;
A7: dom F = Seg len F by FINSEQ_1:def 3;
assume
A8: k in dom F;
hence F.k = (F1/.k) * (F2/.k) by A4
.= g.(F1.k,F2/.k) by A2,A8,A7,A6,PARTFUN1:def 6
.= g.(F1.k,F2.k) by A3,A8,A7,A5,PARTFUN1:def 6;
end;
hence thesis by A1,A2,A3,FINSOP_1:9;
end;
theorem Th18:
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: now
let F,d;
assume
A2: P[F];
thus P[F^<*d*>]
proof
A3: rng F c= rng(F ^ <* d *>) & Product(F ^ <* d *>) = Product(F) * d
by FINSEQ_1:29,FINSOP_1:4;
A4: rng<* d *> = {d} & d in {d} by FINSEQ_1:39,TARSKI:def 1;
assume
A5: rng(F ^ <* d *>) c= carr H;
rng<* d *> c= rng(F ^ <* d *>) by FINSEQ_1:30;
then rng<* d *> c= carr H by A5;
then d in H by A4,STRUCT_0:def 5;
hence thesis by A2,A5,A3,GROUP_2:50,XBOOLE_1:1;
end;
end;
A6: P[<*> the carrier of G]
proof
assume rng <*> the carrier of G c= carr H;
1_G in H by GROUP_2:46;
hence thesis by Th8;
end;
for F holds P[F] from FINSEQ_2:sch 2(A6,A1);
hence thesis;
end;
definition
let G,I,F;
func F |^ I -> FinSequence of the carrier of G means
:Def3:
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 be Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2;
A3: dom p = dom F by A1,FINSEQ_3:29;
rng p c= the carrier of G
proof
let x be object;
assume x in rng p;
then consider y being object such that
A4: y in dom p and
A5: p.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A4;
x = (F/.y) |^ @(I/.y) by A2,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,A3;
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);
A10: dom F1 = Seg len F by A6,FINSEQ_1:def 3;
now
let k be Nat;
assume k in dom F1;
then
A11: k in dom F by A10,FINSEQ_1:def 3;
hence F1.k = (F/.k) |^ @(I/.k) by A7
.= F2.k by A9,A11;
end;
hence thesis by A6,A8,FINSEQ_2:9;
end;
end;
theorem Th19:
len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2)
= (F1 |^ I1) ^ (F2 |^ I2)
proof
assume that
A1: len F1 = len I1 and
A2: len F2 = len I2;
set r = F2 |^ I2;
set q = F1 |^ I1;
len(F1 ^ F2) = len F1 + len F2 by FINSEQ_1:22
.= len(I1 ^ I2) by A1,A2,FINSEQ_1:22;
then
A3: dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:29;
A4: now
let k;
assume
A5: k in dom(F1 ^ F2);
now
per cases by A5,FINSEQ_1:25;
suppose
A6: k in dom F1;
len q = len F1 by Def3;
then k in dom q by A6,FINSEQ_3:29;
then
A7: (q ^ r).k = q.k by FINSEQ_1:def 7
.= (F1/.k) |^ @(I1/.k) by A6,Def3;
A8: (I1 ^ I2).k = (I1 ^ I2)/.k by A3,A5,PARTFUN1:def 6;
A9: F1/.k = F1.k by A6,PARTFUN1:def 6
.= (F1 ^ F2).k by A6,FINSEQ_1:def 7
.= (F1 ^ F2)/.k by A5,PARTFUN1:def 6;
A10: k in dom I1 by A1,A6,FINSEQ_3:29;
then I1/.k = I1.k by PARTFUN1:def 6;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A10,A8,A7,A9,
FINSEQ_1:def 7;
end;
suppose
ex n be Nat st n in dom F2 & k = len F1 + n;
then consider n such that
A11: n in dom F2 and
A12: k = len F1 + n;
A13: (F1 ^ F2).k = F2.n & F2.n = F2/.n by A11,A12,FINSEQ_1:def 7
,PARTFUN1:def 6;
A14: len q = len F1 by Def3;
len r = len F2 by Def3;
then n in dom r by A11,FINSEQ_3:29;
then
A15: (q ^ r).k = r.n by A12,A14,FINSEQ_1:def 7;
A16: (F1 ^ F2).k = (F1 ^ F2)/.k & (I1 ^ I2)/.k = (I1 ^ I2).k by A3,A5,
PARTFUN1:def 6;
A17: n in dom I2 by A2,A11,FINSEQ_3:29;
then
A18: I2/.n = I2.n by PARTFUN1:def 6;
(I1 ^ I2).k = I2.n by A1,A12,A17,FINSEQ_1:def 7;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A11,A15,A13,A16
,A18,Def3;
end;
end;
hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k);
end;
len(q ^ r) = len q + len r by FINSEQ_1:22
.= len F1 + len r by Def3
.= len F1 + len F2 by Def3
.= len(F1 ^ F2) by FINSEQ_1:22;
hence thesis by A4,Def3;
end;
theorem Th20:
rng F c= carr H implies Product(F |^ I) in H
proof
assume
A1: rng F c= carr H;
rng(F |^ I) c= carr H
proof
let x be object;
assume x in rng(F |^ I);
then consider y being object such that
A2: y in dom(F |^ I) and
A3: x = (F |^ I).y by FUNCT_1:def 3;
reconsider y as Element of NAT by A2;
len(F |^ I) = len F by Def3;
then
A4: y in dom F by A2,FINSEQ_3:29;
then F.y in rng F & F.y = F/.y by FUNCT_1:def 3,PARTFUN1:def 6;
then
A5: F/.y in H by A1,STRUCT_0:def 5;
x = (F/.y) |^ @(I/.y) by A3,A4,Def3;
then x in H by A5,Th4;
hence thesis by STRUCT_0:def 5;
end;
hence thesis by Th18;
end;
theorem Th21:
(<*> the carrier of G) |^ (<*> INT) = {}
proof
len <*> the carrier of G = 0;
then len((<*> the carrier of G) |^ (<*> INT)) = 0 by Def3;
hence thesis;
end;
theorem Th22:
<* a *> |^ <* @i *> = <* a |^ i *>
proof
A1: len<* a *> = 1 by FINSEQ_1:39;
A2: now
let k;
A3: @i = <* @i *>/.1 by FINSEQ_4:16;
A4: dom <* a *> = Seg len <* a *> by FINSEQ_1:def 3;
assume k in dom <* a *>;
then
A5: k = 1 by A1,A4,FINSEQ_1:2,TARSKI:def 1;
hence <* a |^ i *>.k = a |^ i
.= (<* a *>/.k) |^ @(<* @i *>/.k) by A3,A5,FINSEQ_4:16;
end;
len<* a |^ i*> = 1 by FINSEQ_1:39;
hence thesis by A1,A2,Def3;
end;
theorem Th23:
<* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>
proof
A1: len <* @i *> = 1 & len<* @j *> = 1 by FINSEQ_1:39;
A2: <* a,b *> = <* a *> ^ <* b *> & <* @i,@j *> = <* @i *> ^ <* @j *> by
FINSEQ_1:def 9;
len<* a *> = 1 & len<* b *> = 1 by FINSEQ_1:39;
hence
<* a,b *> |^ <* @i,@j *> = (<* a *> |^ <* @i *>) ^ (<* b *> |^ <* @j *>
) by A1,A2,Th19
.= <* a |^ i *> ^ (<* b *> |^ <* @j *>) by Th22
.= <* a |^ i *> ^ <* b |^ j *> by Th22
.= <* a |^ i,b |^ j *> by FINSEQ_1:def 9;
end;
theorem
<* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>
proof
A1: len <* @i1 *> = 1 & len<* @i2,@i3 *> = 2 by FINSEQ_1:39,44;
A2: <* a,b,c *> = <* a *> ^ <* b,c *> & <* @i1,@i2,@i3 *> = <* @i1 *> ^ <* @
i2,@ i3 *> by FINSEQ_1:43;
len<* a *> = 1 & len<* b,c *> = 2 by FINSEQ_1:39,44;
hence <* a,b,c *> |^ <* @i1,@i2,@i3 *> = (<* a *> |^ <* @i1 *>) ^ (<* b,c *>
|^ <* @i2,@i3 *>) by A1,A2,Th19
.= <* a |^ i1 *> ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th22
.= <* a |^ i1 *> ^ <* b |^ i2,c |^ i3 *> by Th23
.= <* a |^ i1,b |^ i2,c |^ i3 *> by FINSEQ_1:43;
end;
theorem
F |^ (len F |-> @(1)) = F
proof
defpred P[FinSequence of the carrier of G] means $1 |^ (len $1 |-> @(1)) =
$1;
A1: for F,a st P[F] holds P[F ^ <* a *>]
proof
let F,a;
set A = F ^ <* a *>;
assume
A2: P[F];
A3: len<* a *> = 1 by FINSEQ_1:40;
A4: len<* @(1) *> = 1 & len(len F |-> @(1)) = len F by CARD_1:def 7;
len A = len F + len<* a *> by FINSEQ_1:22;
hence A |^ (len A |-> @(1)) = A |^ ((len F |-> @(1)) ^ <* @(1) *>) by A3,
FINSEQ_2:60
.= (F |^ (len F |-> @(1))) ^ (<* a *> |^ <* @(1) *>) by A3,A4,Th19
.= F ^ <* a |^ 1 *> by A2,Th22
.= F ^ <* a *> by GROUP_1:26;
end;
A5: P[<*> the carrier of G]
proof
set A = <*> the carrier of G;
thus A |^ (len A |-> @(1)) = A |^ (0 |-> @(1)) .= A |^ (<*> INT)
.= A by Th21;
end;
for F holds P[F] from FINSEQ_2:sch 2(A5,A1);
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: for F,a st P[F] holds P[F ^ <* a *>]
proof
let F,a;
set A = F ^ <* a *>;
assume
A2: P[F];
A3: len<* a *> = 1 by FINSEQ_1:40;
A4: len<* @(0) *> = 1 & len(len F |-> @(0)) = len F by CARD_1:def 7;
A5: len A = len F + len<* a *> by FINSEQ_1:22;
hence A |^ (len A |-> @(0)) = A |^ ((len F |-> @(0)) ^ <* @(0) *>) by A3,
FINSEQ_2:60
.= (F |^ (len F |-> @(0))) ^ (<* a *> |^ <* @(0) *>) by A3,A4,Th19
.= (len F |-> 1_G) ^ <* a |^ 0 *> by A2,Th22
.= (len F |-> 1_G) ^ <* 1_G *> by GROUP_1:25
.= (len A |-> 1_G) by A5,A3,FINSEQ_2:60;
end;
A6: P[<*> the carrier of G]
proof
set A = <*> the carrier of G;
thus A |^ (len A |-> @(0)) = A |^ (0 |-> @(0)) .= A |^ (<*> INT)
.= {} by Th21
.= len A |-> 1_G;
end;
for F holds P[F] from FINSEQ_2:sch 2(A6,A1);
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: for k st P[k] holds P[k + 1]
proof
let k;
assume
A2: P[k];
let I;
reconsider J = I | Seg k as FinSequence of INT by FINSEQ_1:18;
assume
A3: len I = k + 1;
then
A4: len J = k by FINSEQ_3:53;
then
A5: (k |-> 1_G) |^ J = k |-> 1_G by A2;
A6: rng I c= INT by FINSEQ_1:def 4;
1 <= k + 1 by NAT_1:12;
then k + 1 in dom I by A3,FINSEQ_3:25;
then I.(k + 1) in rng I by FUNCT_1:def 3;
then reconsider i = I.(k + 1) as Integer by A6;
A7: len<* 1_G *> = 1 & len<* @i *> = 1 by FINSEQ_1:40;
A8: (k + 1) |-> 1_G = (k |-> 1_G) ^ <* 1_G *> & len(k |-> 1_G) = k by
CARD_1:def 7,FINSEQ_2:60;
I = J ^ <* @i *> by A3,FINSEQ_3:55;
then
((k + 1) |-> 1_G) |^ I = ((k |-> 1_G) |^ J) ^ (<* 1_G *> |^ <* @i *>)
by A4,A8,A7,Th19
.= (k |-> 1_G) ^ <* (1_G) |^ i *> by A5,Th22
.= (k |-> 1_G) ^ <* 1_G *> by GROUP_1:31;
hence thesis by FINSEQ_2:60;
end;
A9: P[0]
proof
let I;
assume len I = 0;
then
A10: I = <*> INT;
{} = <*> the carrier of G;
hence thesis by A10,Th21;
end;
for k holds P[k] from NAT_1:sch 2(A9,A1);
hence thesis;
end;
definition
let G,A;
func gr A -> strict Subgroup of G means
:Def4:
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 XFAMILY:sch 1;
set M = meet X;
A2: carr (Omega).G = the carrier of (Omega). G;
then
A3: X <> {} by A1;
A4: the carrier of G in X by A1,A2;
A5: M c= the carrier of G
by A4,SETFAM_1:def 1;
now
let Y;
assume Y in X;
then consider H such that
A6: Y = carr H and
A c= Y by A1;
1_G in H by GROUP_2:46;
hence 1_G in Y by A6,STRUCT_0:def 5;
end;
then
A7: M <> {} by A3,SETFAM_1:def 1;
reconsider M as Subset of G by A5;
A8: now
let a,b;
assume
A9: a in M & b in M;
now
let Y;
assume
A10: Y in X;
then consider H such that
A11: Y = carr H and
A c= Y by A1;
a in carr H & b in carr H by A9,A10,A11,SETFAM_1:def 1;
hence a * b in Y by A11,GROUP_2:74;
end;
hence a * b in M by A3,SETFAM_1:def 1;
end;
now
let a;
assume
A12: a in M;
now
let Y;
assume
A13: Y in X;
then consider H such that
A14: Y = carr H and
A c= Y by A1;
a in carr H by A12,A13,A14,SETFAM_1:def 1;
hence a" in Y by A14,GROUP_2:75;
end;
hence a" in M by A3,SETFAM_1:def 1;
end;
then consider H being strict Subgroup of G such that
A15: the carrier of H = M by A7,A8,GROUP_2:52;
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 A3,A15,SETFAM_1:5;
let H1 be strict Subgroup of G;
A16: the carrier of H1 = carr H1;
assume A c= the carrier of H1;
then the carrier of H1 in X by A1,A16;
hence thesis by A15,GROUP_2:57,SETFAM_1:3;
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:55;
end;
end;
theorem Th28:
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
defpred P[set] means ex F,I st $1 = Product (F |^ I) & len F = len I & rng
F c= A;
assume
A1: a in gr A;
reconsider B = {b : P[b]} as Subset of G from DOMAIN_1:sch 7;
A2: now
let c,d;
assume that
A3: c in B and
A4: d in B;
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 A3;
then consider F1,I1 such that
A5: c = Product(F1 |^ I1) and
A6: len F1 = len I1 and
A7: rng F1 c= A;
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 A4;
then consider F2,I2 such that
A8: d = Product(F2 |^ I2) and
A9: len F2 = len I2 and
A10: rng F2 c= A;
A11: len(F1 ^ F2) = len I1 + len I2 by A6,A9,FINSEQ_1:22
.= len(I1 ^ I2) by FINSEQ_1:22;
rng(F1 ^ F2) = rng F1 \/ rng F2 by FINSEQ_1:31;
then
A12: rng(F1 ^ F2) c= A by A7,A10,XBOOLE_1:8;
c * d = Product((F1 |^ I1) ^ (F2 |^ I2)) by A5,A8,FINSOP_1:5
.= Product((F1 ^ F2) |^ (I1 ^ I2)) by A6,A9,Th19;
hence c * d in B by A12,A11;
end;
A13: 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
A14: c = Product(F1 |^ I1) and
A15: len F1 = len I1 and
A16: rng F1 c= A;
deffunc F(Nat) = F1.(len F1 - $1 + 1);
consider F2 being FinSequence such that
A17: len F2 = len F1 and
A18: for k be Nat st k in dom F2 holds F2.k = F(k) from FINSEQ_1:sch
2;
A19: Seg len I1 = dom I1 by FINSEQ_1:def 3;
A20: rng F2 c= rng F1
proof
let x be object;
assume x in rng F2;
then consider y being object such that
A21: y in dom F2 and
A22: F2.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A21;
reconsider n = len F1 - y + 1 as Element of NAT by A17,A21,Lm3;
1 <= n & n <= len F1 by A17,A21,Lm3;
then
A23: n in dom F1 by FINSEQ_3:25;
x = F1.(len F1 - y + 1) by A18,A21,A22;
hence thesis by A23,FUNCT_1:def 3;
end;
then
A24: rng F2 c= A by A16;
defpred P[Nat,object] means ex i st i = I1.(len I1 - $1 + 1) & $2 = - i;
A25: for k be Nat st k in Seg len I1 ex x being object st P[k,x]
proof
let k be Nat;
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 Element of NAT by Lm3;
1 <= n & n <= len I1 by A26,Lm3;
then n in dom I1 by FINSEQ_3:25;
then
A27: I1.n in rng I1 by FUNCT_1:def 3;
rng I1 c= INT by FINSEQ_1:def 4;
then reconsider i = I1.n as Element of INT qua non empty set by A27;
take -i,i;
thus thesis;
end;
consider I2 being FinSequence such that
A28: dom I2 = Seg len I1 and
A29: for k be Nat st k in Seg len I1 holds P[k,I2.k] from FINSEQ_1:
sch 1(A25);
A30: len F2 = len I2 by A15,A17,A28,FINSEQ_1:def 3;
A31: rng I2 c= INT
proof
let x be object;
assume x in rng I2;
then consider y being object such that
A32: y in dom I2 and
A33: x = I2.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A32;
ex i st i = I1.(len I1 - y + 1) & x = - i by A28,A29,A32,A33;
hence thesis by INT_1:def 2;
end;
rng F1 c= the carrier of G by FINSEQ_1:def 4;
then
A34: rng F2 c= the carrier of G by A20;
set p = F1 |^ I1;
A35: Seg len F1 = dom F1 by FINSEQ_1:def 3;
A36: len p = len F1 by Def3;
A37: dom F2 = dom I2 by A15,A17,A28,FINSEQ_1:def 3;
reconsider I2 as FinSequence of INT by A31,FINSEQ_1:def 4;
reconsider F2 as FinSequence of the carrier of G by A34,FINSEQ_1:def 4;
set q = F2 |^ I2;
A38: len q = len F2 by Def3;
then
A39: dom q = dom F2 by FINSEQ_3:29;
A40: dom F1 = dom I1 by A15,FINSEQ_3:29;
now
let k;
A41: I2/.k = @(I2/.k);
assume
A42: k in dom q;
then reconsider n = len p - k + 1 as Element of NAT by A17,A36,A38,Lm3;
A43: I1/.n = @(I1/.n) & q/.k = q.k by A42,PARTFUN1:def 6;
dom q = dom I1 by A15,A17,A38,FINSEQ_3:29;
then consider i such that
A44: i = I1.n and
A45: I2.k = - i by A15,A29,A19,A36,A42;
I2.k = I2/.k by A37,A39,A42,PARTFUN1:def 6;
then
A46: q.k = (F2/.k) |^ (- i) by A39,A42,A45,A41,Def3;
A47: F2/.k = F2.k & F2.k = F1.n by A18,A36,A39,A42,PARTFUN1:def 6;
1 <= n & len p >= n by A17,A36,A38,A42,Lm3;
then
A48: n in dom I2 by A17,A30,A36,FINSEQ_3:25;
then
A49: I1.n = I1/.n by A28,A19,PARTFUN1:def 6;
F1/.n= F1.n by A15,A35,A28,A48,PARTFUN1:def 6;
then q.k = ((F1/.n) |^ i)" by A46,A47,GROUP_1:36;
hence (q/.k)" = p.(len p - k + 1) by A40,A28,A19,A48,A44,A49,A43,Def3;
end;
then Product p" = Product q by A17,A36,A38,Th14;
hence c" in B by A14,A30,A24;
end;
A50: len {} = 0;
A51: rng <*> the carrier of G = {} & {} c= A;
1_G = Product <*> the carrier of G & (<*> the carrier of G) |^ (<*>
INT) = {} by Th8,Th21;
then 1_G in B by A51,A50;
then consider H being strict Subgroup of G such that
A52: the carrier of H = B by A2,A13,GROUP_2:52;
A c= B
proof
reconsider p = 1 as Integer;
let x be object;
assume
A53: x in A;
then reconsider a = x as Element of G;
A54: rng<* a *> = {a} & {a} c= A by A53,FINSEQ_1:39,ZFMISC_1:31;
A55: len<* a *> = 1 & len<* @p *> = 1 by FINSEQ_1:39;
Product(<* a *> |^ <* @p *>) = Product<* a |^ 1 *> by Th22
.= a |^ 1 by FINSOP_1:11
.= a by GROUP_1:26;
hence thesis by A55,A54;
end;
then gr A is Subgroup of H by A52,Def4;
then a in H by A1,GROUP_2:40;
then a in B by A52,STRUCT_0:def 5;
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
A56: rng F c= A and
A57: Product(F |^ I) = a;
A c= the carrier of gr A by Def4;
then rng F c= carr gr A by A56;
hence thesis by A57,Th20;
end;
theorem Th29:
a in A implies a in gr A
proof
assume
A1: a in A;
A c= the carrier of gr A by Def4;
hence thesis by A1,STRUCT_0:def 5;
end;
theorem
gr {} the carrier of G = (1).G
proof
{} the carrier of G c= the carrier of (1).G & 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:65;
hence thesis by Def4;
end;
theorem Th31:
for H being strict Subgroup of G holds gr carr H = H
proof
let H be strict Subgroup of G;
for H1 be strict Subgroup of G st carr H c= the carrier of H1 holds H is
Subgroup of H1 by GROUP_2:57;
hence thesis by Def4;
end;
theorem Th32:
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 and
A3: rng F c= A and
A4: Product(F |^ I) = a by Th28;
rng F c= B by A1,A3;
hence a in gr B by A2,A4,Th28;
end;
hence thesis by GROUP_2:58;
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 and
A2: rng F c= A /\ B and
A3: Product(F |^ I) = a by Th28;
A /\ B c= B by XBOOLE_1:17;
then rng F c= B by A2;
then
A4: a in gr B by A1,A3,Th28;
A /\ B c= A by XBOOLE_1:17;
then rng F c= A by A2;
then a in gr A by A1,A3,Th28;
hence a in gr A /\ gr B by A4,GROUP_2:82;
end;
hence thesis by GROUP_2:58;
end;
theorem Th34:
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;
set X = {B :ex H being strict Subgroup of G st B = the carrier of H & A c=
carr H};
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;
end;
the carrier of (Omega).G = carr (Omega).G;
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);
A4: now
let H1 be strict Subgroup of G;
A5: the carrier of H1 = carr H1;
assume A c= the carrier of H1;
then the carrier of H1 in X by A5;
hence H is Subgroup of H1 by A3,GROUP_2:57,SETFAM_1:3;
end;
carr (Omega).G in X;
then A c= the carrier of H by A3,A1,SETFAM_1:5;
hence thesis by A3,A4,Def4;
end;
theorem Th35:
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 be object;
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;
hence thesis by A2,A4;
end;
let x be object;
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:46;
then 1_G in carr H by STRUCT_0:def 5;
then {1_G} c= carr H by ZFMISC_1:31;
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:31;
hence A c= carr H by A10,XBOOLE_1:45;
end;
suppose
not 1_G in A;
hence A c= carr H by A9,ZFMISC_1:57;
end;
end;
hence thesis by A6,A8;
end;
the carrier of gr A = meet X by Th34
.= the carrier of gr(A \ {1_G}) by A1,Th34;
hence thesis by GROUP_2:59;
end;
definition
let G,a;
attr a is generating means
not for A st gr A = the multMagma of G
holds gr(A \ {a}) = the multMagma of G;
end;
theorem
1_G is non generating
by Th35;
definition
let G, H;
attr H is maximal means
the multMagma of H <> the multMagma of G &
for K being strict Subgroup of G st the multMagma of H <> K & H is Subgroup of
K holds K = the multMagma of G;
end;
theorem Th37:
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;
gr carr H is Subgroup of gr(carr H \/ {a}) by Th32,XBOOLE_1:7;
then
A3: H is Subgroup of gr(carr H \/ {a}) by Th31;
a in {a} by TARSKI:def 1;
then a in carr H \/ {a} by XBOOLE_0:def 3;
then H <> gr(carr H \/ {a}) by A2,Th29;
hence thesis by A1,A3;
end;
::
:: Frattini subgroup.
::
definition
let G be Group;
::$N Frattini subgroup
func Phi(G) -> strict Subgroup of G means
:Def7:
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 multMagma 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;
end;
suppose
A2: for H being strict Subgroup of G holds H is not maximal;
(Omega).G = the multMagma of G;
hence thesis by A2;
end;
end;
hence thesis;
end;
uniqueness by GROUP_2:59;
correctness;
end;
theorem Th38:
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;
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};
assume
A1: ex H being strict Subgroup of G st H is maximal;
then consider H being strict Subgroup of G such that
A2: H 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 STRUCT_0:def 5;
then
A3: a in meet X by A1,Def7;
let H be strict Subgroup of G;
assume H is maximal;
then carr H in X;
then a in carr H by A3,SETFAM_1:def 1;
hence thesis by STRUCT_0:def 5;
end;
assume
A4: for H being strict Subgroup of G st H is maximal holds a in H;
A5: now
let Y;
assume Y in X;
then consider A being Subset of G such that
A6: Y = A and
A7: 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
A8: A = the carrier of H and
A9: H is maximal by A7;
a in H by A4,A9;
hence a in Y by A6,A8,STRUCT_0:def 5;
end;
carr H in X by A2;
then a in meet X by A5,SETFAM_1:def 1;
then a in the carrier of Phi(G) by A1,Def7;
hence thesis by STRUCT_0:def 5;
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 multMagma of G by Def7;
hence thesis by STRUCT_0:def 5;
end;
theorem Th40:
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 Th38;
hence thesis by GROUP_2:58;
end;
theorem Th41:
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
defpred P[set,set] means ex H1,H2 being strict Subgroup of G st $1 = H1 &
$2 = H2 & H1 is Subgroup of H2;
let x be object;
assume
A1: x in the carrier of Phi(G);
then x in Phi(G) by STRUCT_0:def 5;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def 5;
assume not x in A;
then a is generating;
then consider B being Subset of G such that
A2: gr B = G and
A3: gr(B \ {a}) <> G;
set M = B \ {a};
A4: now
assume
A5: a in gr M;
now
let b be Element of G;
b in gr B by A2,STRUCT_0:def 5;
then consider F being FinSequence of the carrier of G, I such that
len I = len F and
A6: rng F c= B and
A7: b = Product(F |^ I) by Th28;
rng(F |^ I) c= carr gr M
proof
let x be object;
assume x in rng(F |^ I);
then consider y being object such that
A8: y in dom(F |^ I) and
A9: (F |^ I).y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A8;
len(F |^ I) = len F by Def3;
then
A10: y in dom F by A8,FINSEQ_3:29;
then
A11: x = (F/.y) |^ @(I/.y) by A9,Def3;
now
per cases;
suppose
F/.y = a;
then x in gr M by A5,A11,Th4;
hence thesis by STRUCT_0:def 5;
end;
suppose
F/.y <> a;
then
A12: not F/.y in {a} by TARSKI:def 1;
F/.y = F.y & F.y in rng F by A10,FUNCT_1:def 3,PARTFUN1:def 6;
then F/.y in M by A6,A12,XBOOLE_0:def 5;
then x in gr M by A11,Th4,Th29;
hence thesis by STRUCT_0:def 5;
end;
end;
hence thesis;
end;
hence b in gr M by A7,Th18;
end;
hence contradiction by A3,GROUP_2:62;
end;
defpred P[Subgroup of G] means M c= carr $1 & not a in $1;
consider X such that
A13: X c= Subgroups G and
A14: for H being strict Subgroup of G holds H in X iff P[H] from
SubgrSep;
M c= carr gr M by Def4;
then reconsider X as non empty set by A14,A4;
A15: 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
A16: x = H1 and
A17: y = H2 & H1 is Subgroup of H2;
given H3,H4 being strict Subgroup of G such that
A18: y = H3 and
A19: z = H4 and
A20: H3 is Subgroup of H4;
H1 is Subgroup of H4 by A17,A18,A20,GROUP_2:56;
hence thesis by A16,A19;
end;
A21: 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
A22: Y c= 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:76;
assume
A23: for x,y being Element of X st x in Y & y in Y holds P[x,y] or P [y,x];
now
per cases;
suppose
A24: Y = {};
set y = the Element of X;
take y;
let x be Element of X;
assume x in Y;
hence P[x,y] by A24;
end;
suppose
A25: Y <> {};
A26: now
let a,b be Element of G;
assume that
A27: a in E and
A28: b in E;
consider Z being set such that
A29: a in Z and
A30: Z in C by A27,TARSKI:def 4;
consider Z1 being set such that
A31: b in Z1 and
A32: Z1 in C by A28,TARSKI:def 4;
consider D being Subset of G such that
A33: Z = D and
A34: ex H being strict Subgroup of G st H in Y & D = carr H by A30;
consider B being Subset of G such that
A35: Z1 = B and
A36: ex H being strict Subgroup of G st H in Y & B = carr H by A32;
consider H1 being Subgroup of G such that
A37: H1 in Y and
A38: D = carr H1 by A34;
consider H2 being Subgroup of G such that
A39: H2 in Y and
A40: B = carr H2 by A36;
now
per cases by A22,A23,A37,A39;
suppose
P[H1,H2];
then carr H1 c= the carrier of H2 by GROUP_2:def 5;
then a * b in carr H2 by A29,A33,A38,A31,A35,A40,GROUP_2:74;
hence a * b in E by A32,A35,A40,TARSKI:def 4;
end;
suppose
P[H2,H1];
then carr H2 c= the carrier of H1 by GROUP_2:def 5;
then a * b in carr H1 by A29,A33,A38,A31,A35,A40,GROUP_2:74;
hence a * b in E by A30,A33,A38,TARSKI:def 4;
end;
end;
hence a * b in E;
end;
A41: now
let a be Element of G;
assume a in E;
then consider Z being set such that
A42: a in Z and
A43: Z in C by TARSKI:def 4;
consider D being Subset of G such that
A44: Z = D and
A45: ex H being strict Subgroup of G st H in Y & D = carr H by A43;
consider H1 being Subgroup of G such that
H1 in Y and
A46: D = carr H1 by A45;
a" in carr H1 by A42,A44,A46,GROUP_2:75;
hence a" in E by A43,A44,A46,TARSKI:def 4;
end;
set s = the Element of Y;
A47: s in X by A22,A25;
then reconsider s as strict Subgroup of G by A13,GROUP_3:def 1;
A48: carr s in C by A25;
then
A49: carr s c= E by ZFMISC_1:74;
E <> {} by A48,ORDERS_1:6;
then consider H being strict Subgroup of G such that
A50: the carrier of H = E by A26,A41,GROUP_2:52;
A51: now
assume a in H;
then a in E by A50,STRUCT_0:def 5;
then consider Z being set such that
A52: a in Z and
A53: Z in C by TARSKI:def 4;
consider D being Subset of G such that
A54: Z = D and
A55: ex H being strict Subgroup of G st H in Y & D = carr H by A53;
consider H1 being strict Subgroup of G such that
A56: H1 in Y and
A57: D = carr H1 by A55;
not a in H1 by A14,A22,A56;
hence contradiction by A52,A54,A57,STRUCT_0:def 5;
end;
M c= carr s by A14,A47;
then
A58: M c= E by A49;
the carrier of H = carr H;
then reconsider y = H as Element of X by A14,A58,A50,A51;
take y;
let x be Element of X;
assume
A59: x in Y;
x in Subgroups G by A13;
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;
then the carrier of K in C by A59;
hence K is Subgroup of H by A50,GROUP_2:57,ZFMISC_1:74;
end;
end;
hence thesis;
end;
A60: now
let x be Element of X;
x in Subgroups G by A13;
hence x is strict Subgroup of G by GROUP_3:def 1;
end;
A61: 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 A60;
H is Subgroup of H by GROUP_2:54;
hence thesis;
end;
A62: for x,y being Element of X st P[x,y] & P[y,x] holds x = y by GROUP_2:55;
consider s being Element of X such that
A63: for y being Element of X st s <> y holds not P[s,y] from
ORDERS_1:sch 1 (A61,A62,A15,A21);
reconsider H = s as strict Subgroup of G by A60;
H is maximal
proof
not a in H by A14;
hence the multMagma of H <> the multMagma of G by STRUCT_0:def 5;
let K be strict Subgroup of G;
assume that
A64: K <> the multMagma of H and
A65: H is Subgroup of K and
A66: K <> the multMagma of G;
A67: M c= carr H by A14;
the carrier of H c= the carrier of K by A65,GROUP_2:def 5;
then
A68: M c= carr K by A67;
now
A69: B c= M \/ {a}
proof
let x be object;
assume
A70: x in B;
now
per cases;
suppose
x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x <> a;
then not x in {a} by TARSKI:def 1;
then x in M by A70,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
assume a in K;
then a in carr K by STRUCT_0:def 5;
then {a} c= carr K by ZFMISC_1:31;
then M \/ {a} c= carr K by A68,XBOOLE_1:8;
then gr B is Subgroup of gr carr K by A69,Th32,XBOOLE_1:1;
then G is Subgroup of K by A2,Th31;
hence contradiction by A66,GROUP_2:55;
end;
then reconsider v = K as Element of X by A14,A68;
not P[s,v] by A63,A64;
hence thesis by A65;
end;
then Phi(G) is Subgroup of H by Th40;
then the carrier of Phi(G) c= the carrier of H by GROUP_2:def 5;
then x in H by A1,STRUCT_0:def 5;
hence thesis by A14;
end;
let x be object;
assume x in A;
then consider a being Element of G such that
A71: x = a and
A72: 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 Def7;
hence thesis by A71;
end;
suppose
A73: ex H being strict Subgroup of G st H is maximal;
now
let H be strict Subgroup of G;
assume
A74: H is maximal;
now
assume
A75: not a in H;
carr H /\ {a} c= {}
proof
let x be object;
assume
A76: x in carr H /\ {a};
then x in {a} by XBOOLE_0:def 4;
then
A77: x = a by TARSKI:def 1;
x in carr H by A76,XBOOLE_0:def 4;
hence thesis by A75,A77,STRUCT_0:def 5;
end;
then carr H /\ {a} = {};
then
A78: carr H misses {a};
(carr H \/ {a}) \ {a} = carr H \ {a} by XBOOLE_1:40
.= carr H by A78,XBOOLE_1:83;
then
A79: gr((carr H \/ {a}) \ {a}) = H by Th31;
A80: H <> G by A74;
gr(carr H \/ {a}) = G by A74,A75,Th37;
hence contradiction by A72,A79,A80;
end;
hence a in H;
end;
then a in Phi(G) by A73,Th38;
hence thesis by A71,STRUCT_0:def 5;
end;
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 STRUCT_0:def 5;
then a in {b where b is Element of G: b is non generating} by Th41;
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 Th41;
hence thesis by STRUCT_0:def 5;
end;
definition
let G,H1,H2;
func H1 * H2 -> Subset of G equals
carr H1 * carr H2;
correctness;
end;
theorem
H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 & H1 * H2 = carr
H1 * H2;
theorem
H1 * H2 * H3 = H1 * (H2 * H3)
proof
thus H1 * H2 * H3 = carr H1 * (carr H2 * H3) by GROUP_2:96
.= H1 * (H2 * H3);
end;
theorem
a * H1 * H2 = a * (H1 * H2)
proof
thus a * H1 * H2 = a * (carr H1 * H2) by GROUP_2:96
.= a * (H1 * H2);
end;
theorem
H1 * H2 * a = H1 * (H2 * a)
proof
thus H1 * H2 * a = H1 * carr H2 * a .= H1 * (H2 * a) by GROUP_2:98;
end;
theorem
A * H1 * H2 = A * (H1 * H2)
proof
thus A * H1 * H2 = A * (H1 * carr H2) by GROUP_2:99
.= A * (H1 * H2);
end;
theorem
H1 * H2 * A = H1 * (H2 * A)
proof
thus H1 * H2 * A = H1 * carr H2 * A .= H1 * (H2 * A) by GROUP_2:98;
end;
definition
let G,H1,H2;
func H1 "\/" H2 -> strict Subgroup of G equals
gr(carr H1 \/ carr H2);
correctness;
end;
theorem
a in H1 "\/" H2 iff ex F,I st len F = len I & rng F c= carr H1 \/ carr
H2 & a = Product(F |^ I) by Th28;
theorem
H1 "\/" H2 = gr(H1 * H2)
proof
set H = gr(carr H1 * carr H2);
now
let a;
assume a in H;
then consider F,I such that
A1: len F = len I and
A2: rng F c= carr H1 * carr H2 and
A3: a = Product(F |^ I) by Th28;
rng(F |^ I) c= carr(H1 "\/" H2)
proof
set f = F |^ I;
let x be object;
A4: rng I c= INT by FINSEQ_1:def 4;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: f.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A5;
A7: len f = len F by Def3;
then
A8: y in dom I by A1,A5,FINSEQ_3:29;
then
A9: I/.y = I.y by PARTFUN1:def 6;
I.y in rng I by A8,FUNCT_1:def 3;
then reconsider i = I.y as Integer by A4;
A10: @(I/.y) = I/.y;
y in dom F by A5,A7,FINSEQ_3:29;
then F/.y = F.y & F.y in rng F by FUNCT_1:def 3,PARTFUN1:def 6;
then consider b,c such that
A11: F/.y = b * c and
A12: b in carr H1 and
A13: c in carr H2 by A2,GROUP_2:8;
y in dom F by A5,A7,FINSEQ_3:29;
then
A14: x = (F/.y) |^ i by A6,A9,A10,Def3;
now
per cases;
suppose
i >= 0;
then reconsider n = i as Element of NAT by INT_1:3;
defpred P[Nat,object] means
($1 mod 2 = 1 implies $2 = b) & ($1 mod 2 =
0 implies $2 = c);
A15: for k be Nat st k in Seg(2 * n) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg(2 * n);
now
per cases by NAT_D:12;
suppose
A16: 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 A16;
end;
suppose
A17: 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 A17;
end;
end;
hence thesis;
end;
consider p being FinSequence such that
A18: dom p = Seg(2 * n) and
A19: for k be Nat st k in Seg(2 * n) holds P[k,p.k] from
FINSEQ_1:sch 1(A15);
A20: len p = 2 * n by A18,FINSEQ_1:def 3;
A21: rng p c= {b,c}
proof
let x be object;
assume x in rng p;
then consider y being object such that
A22: y in dom p and
A23: p.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A22;
now
per cases by NAT_D:12;
suppose
y mod 2 = 0;
then x = c by A18,A19,A22,A23;
hence thesis by TARSKI:def 2;
end;
suppose
y mod 2 = 1;
then x = b by A18,A19,A22,A23;
hence thesis by TARSKI:def 2;
end;
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;
A24: 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 Def4;
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);
A25: for k being Nat st for l being Nat st l < k holds Q[l] holds Q[ k]
proof
let k be Nat;
assume
A26: for l being Nat st l < k holds Q[l];
assume that
A27: k <= 2 * n and
A28: k mod 2 = 0;
let F1;
assume
A29: F1 = p | Seg k;
now
per cases;
suppose
A30: k = 0;
F1 = <*> the carrier of G by A29,A30;
then Product F1 = 1_G by Th8;
hence thesis by A30,GROUP_1:25;
end;
suppose
A32: k <> 0;
A33: k <> 1 by A28,NAT_D:14;
k >= 1 by A32,NAT_1:14;
then k > 1 by A33,XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | Seg m as FinSequence of the carrier of G by
FINSEQ_1:18;
1 * 2 = 2;
then
A34: m mod 2 = 0 by A28,NAT_D:15;
A35: m + 2 = k;
then
A36: m <= 2 * n by A27,NAT_1:16,XXREAL_0:2;
then ex o being Nat st 2 * n = m + o by NAT_1:10;
then
A37: len q = m by A20,FINSEQ_3:53;
A38: ex j being Nat st 2 * n = k + j by A27,NAT_1:10;
then
A39: len F1 = k by A20,A29,FINSEQ_3:53;
A40: now
let l;
assume
A41: l in dom q;
then l <= len q by FINSEQ_3:25;
then
A42: l <= len F1 by A35,A39,A37,NAT_1:16,XXREAL_0:2;
1 <= l by A41,FINSEQ_3:25;
then l in dom F1 by A42,FINSEQ_3:25;
then F1.l = p.l by A29,FUNCT_1:47;
hence F1.l = q.l by A41,FUNCT_1:47;
end;
A43: m < k by A35,NAT_1:16;
then
A44: Product q = (F/.y) |^ (m div 2) by A26,A36,A34;
A45: now
let l;
assume l in dom<* b,c *>;
then
A46: l in {1,2} by FINSEQ_1:2,89;
now
per cases by A46,TARSKI:def 2;
suppose
A47: l = 1;
then
A48: <* b,c *>.l = b;
A49: m + 1 mod 2 = 1 & dom F1 c= dom p by A29,A34,NAT_D:16
,RELAT_1:60;
m + 1 <= k & 1 <= m + 1 by A43,NAT_1:12,13;
then
A50: m + 1 in dom F1 by A39,FINSEQ_3:25;
then F1.(len q + l) = p.(m + 1) by A29,A37,A47,FUNCT_1:47
;
hence F1.(len q + l) = <* b,c *>.l by A18,A19,A48,A50,A49
;
end;
suppose
A51: l = 2;
then
A52: <* b,c *>.l = c;
A53: dom F1 c= dom p by A29,RELAT_1:60;
1 <= m + (1 + 1) by NAT_1:12;
then
A54: m + 2 in dom F1 by A39,FINSEQ_3:25;
then F1.(len q + l) = p.(m + 2) by A29,A37,A51,FUNCT_1:47
;
hence F1.(len q + l) = <* b,c *>.l by A18,A19,A28,A52,A54
,A53;
end;
end;
hence F1.(len q + l) = <* b,c *>.l;
end;
A55: m div 2*1 + 1 = (m div 2) + (2 div 2)
.= k div 2 by A35,A34,NAT_D:19;
len F1 = m + 2 by A20,A29,A38,FINSEQ_3:53
.= len q + len<* b,c *> by A37,FINSEQ_1:44;
then F1 = q ^ <* b,c *> by A40,A45,FINSEQ_3:38;
then Product F1 = Product q * Product<* b,c *> by FINSOP_1:5
.= Product q * (F/.y) by A11,FINSOP_1:12
.= (F/.y) |^ ((m div 2) + 1) by A44,GROUP_1:34;
hence thesis by A55;
end;
end;
hence thesis;
end;
A56: for k being Nat holds Q[k] from NAT_1:sch 4(A25);
b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A12,A13,
XBOOLE_0:def 3;
then {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:32;
then
A57: rng p c= carr H1 \/ carr H2 by A21;
len p = 2 * n by A18,FINSEQ_1:def 3;
then
A58: p = p | Seg(2 * n) by FINSEQ_3:49;
2 * n mod 2 = 0 & 2 * n div 2 = n;
then x = Product(p) by A14,A56,A58;
then x in gr(carr H1 \/ carr H2) by A57,A24,Th18,XBOOLE_1:1;
hence thesis by STRUCT_0:def 5;
end;
suppose
A59: i < 0;
defpred P[Nat,object] means
($1 mod 2 = 1 implies $2 = c") & ($1 mod 2
= 0 implies $2 = b");
set n = |.i.|;
A60: 2 * n mod 2 = 0 & 2 * n div 2 = n;
A61: for k be Nat st k in Seg(2 * n) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg(2 * n);
now
per cases by NAT_D:12;
suppose
A62: 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 A62;
end;
suppose
A63: 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 A63;
end;
end;
hence thesis;
end;
consider p being FinSequence such that
A64: dom p = Seg(2 * n) and
A65: for k be Nat st k in Seg(2 * n) holds P[k,p.k] from
FINSEQ_1:sch 1(A61);
A66: len p = 2 * n by A64,FINSEQ_1:def 3;
A67: rng p c= {b",c"}
proof
let x be object;
assume x in rng p;
then consider y being object such that
A68: y in dom p and
A69: p.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A68;
now
per cases by NAT_D:12;
suppose
y mod 2 = 0;
then x = b" by A64,A65,A68,A69;
hence thesis by TARSKI:def 2;
end;
suppose
y mod 2 = 1;
then x = c" by A64,A65,A68,A69;
hence thesis by TARSKI:def 2;
end;
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;
A70: 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 Def4;
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))";
A71: for k being Nat st for l being Nat st l < k holds Q[l] holds Q [k]
proof
let k be Nat;
assume
A72: for l being Nat st l < k holds Q[l];
assume that
A73: k <= 2 * n and
A74: k mod 2 = 0;
let F1;
assume
A75: F1 = p | Seg k;
now
per cases;
suppose
A76: k = 0;
then
A77: (F/.y) |^ (k div 2) = 1_G by GROUP_1:25;
F1 = <*> the carrier of G by A75,A76;
then Product F1 = 1_G by Th8;
hence thesis by A77,GROUP_1:8;
end;
suppose
A78: k <> 0;
A79: k <> 1 by A74,NAT_D:14;
k >= 1 by A78,NAT_1:14;
then k > 1 by A79,XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | Seg m as FinSequence of the carrier of G by
FINSEQ_1:18;
1 * 2 = 2;
then
A80: m mod 2 = 0 by A74,NAT_D:15;
A81: m + 2 = k;
then
A82: m <= 2 * n by A73,NAT_1:16,XXREAL_0:2;
then ex o being Nat st 2 * n = m + o by NAT_1:10;
then
A83: len q = m by A66,FINSEQ_3:53;
A84: ex j being Nat st 2 * n = k + j by A73,NAT_1:10;
then
A85: len F1 = k by A66,A75,FINSEQ_3:53;
A86: now
let l;
assume
A87: l in dom q;
then l <= len q by FINSEQ_3:25;
then
A88: l <= len F1 by A81,A85,A83,NAT_1:16,XXREAL_0:2;
1 <= l by A87,FINSEQ_3:25;
then l in dom F1 by A88,FINSEQ_3:25;
then F1.l = p.l by A75,FUNCT_1:47;
hence F1.l = q.l by A87,FUNCT_1:47;
end;
A89: m < k by A81,NAT_1:16;
then
A90: Product q = ((F/.y) |^ (m div 2))" by A72,A82,A80;
A91: now
let l;
assume l in dom<* c",b" *>;
then
A92: l in {1,2} by FINSEQ_1:2,89;
now
per cases by A92,TARSKI:def 2;
suppose
A93: l = 1;
then
A94: <* c",b" *>.l = c";
A95: m + 1 mod 2 = 1 & dom F1 c= dom p by A75,A80,NAT_D:16
,RELAT_1:60;
m + 1 <= k & 1 <= m + 1 by A89,NAT_1:12,13;
then
A96: m + 1 in dom F1 by A85,FINSEQ_3:25;
then
F1.(len q + l) = p.(m + 1) by A75,A83,A93,FUNCT_1:47;
hence F1.(len q + l) = <* c",b" *>.l by A64,A65,A94,A96
,A95;
end;
suppose
A97: l = 2;
then
A98: <* c",b" *>.l = b";
A99: dom F1 c= dom p by A75,RELAT_1:60;
1 <= m + (1 + 1) by NAT_1:12;
then
A100: m + 2 in dom F1 by A85,FINSEQ_3:25;
then
F1.(len q + l) = p.(m + 2) by A75,A83,A97,FUNCT_1:47;
hence F1.(len q + l) = <* c",b" *>.l by A64,A65,A74,A98
,A100,A99;
end;
end;
hence F1.(len q + l) = <* c",b" *>.l;
end;
A101: m div 2*1 + 1 = (m div 2) + (2 div 2)
.= k div 2 by A81,A80,NAT_D:19;
len F1 = m + 2 by A66,A75,A84,FINSEQ_3:53
.= len q + len<* c",b" *> by A83,FINSEQ_1:44;
then F1 = q ^ <* c",b" *> by A86,A91,FINSEQ_3:38;
then Product F1 = Product q * Product<* c",b" *> by FINSOP_1:5
.= Product q * (c" * b") by FINSOP_1:12
.= Product q * (F/.y)" by A11,GROUP_1:17
.= ((F/.y) * ((F/.y) |^ (m div 2)))" by A90,GROUP_1:17
.= ((F/.y) |^ ((m div 2) + 1))" by GROUP_1:34;
hence thesis by A101;
end;
end;
hence thesis;
end;
A102: for k being Nat holds Q[k] from NAT_1:sch 4(A71);
c" in carr H2 by A13,GROUP_2:75;
then
A103: c" in carr H1 \/ carr H2 by XBOOLE_0:def 3;
len p = 2 * n by A64,FINSEQ_1:def 3;
then
A104: p = p | Seg(2 * n) by FINSEQ_3:49;
b" in carr H1 by A12,GROUP_2:75;
then b" in carr H1 \/ carr H2 by XBOOLE_0:def 3;
then {b",c"} c= carr H1 \/ carr H2 by A103,ZFMISC_1:32;
then
A105: rng p c= carr H1 \/ carr H2 by A67;
x = ((F/.y) |^ n)" by A14,A59,GROUP_1:30;
then x = Product(p) by A102,A60,A104;
then x in gr(carr H1 \/ carr H2) by A105,A70,Th18,XBOOLE_1:1;
hence thesis by STRUCT_0:def 5;
end;
end;
hence thesis;
end;
hence a in H1 "\/" H2 by A3,Th18;
end;
then
A106: H is Subgroup of H1 "\/" H2 by GROUP_2:58;
carr H1 \/ carr H2 c= carr H1 * carr H2
proof
let x be object;
assume
A107: x in carr H1 \/ carr H2;
then reconsider a = x as Element of G;
now
per cases by A107,XBOOLE_0:def 3;
suppose
A108: x in carr H1;
1_G in H2 by GROUP_2:46;
then
A109: 1_G in carr H2 by STRUCT_0:def 5;
a * 1_G = a by GROUP_1:def 4;
hence thesis by A108,A109;
end;
suppose
A110: x in carr H2;
1_G in H1 by GROUP_2:46;
then
A111: 1_G in carr H1 by STRUCT_0:def 5;
1_G * a = a by GROUP_1:def 4;
hence thesis by A110,A111;
end;
end;
hence thesis;
end;
then H1 "\/" H2 is Subgroup of H by Th32;
hence gr(H1 * H2) = H1 "\/" H2 by A106,GROUP_2:55;
end;
theorem Th51:
H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2
proof
assume H1 * H2 = H2 * H1;
then consider H being strict Subgroup of G such that
A1: the carrier of H = carr H1 * carr H2 by GROUP_2:78;
now
reconsider p = 1 as Integer;
let a;
assume a in H;
then a in carr H1 * carr H2 by A1,STRUCT_0:def 5;
then consider b,c such that
A2: a = b * c and
A3: b in carr H1 & c in carr H2;
b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A3,XBOOLE_0:def 3;
then
A4: rng<* b,c *> = {b,c} & {b,c} c= carr H1 \/ carr H2 by FINSEQ_2:127
,ZFMISC_1:32;
A5: len<* b,c *> = 2 & len<* @p,@p *> = 2 by FINSEQ_1:44;
a = Product<* b *> * c by A2,FINSOP_1:11
.= Product<* b *> * Product<* c *> by FINSOP_1:11
.= Product(<* b *> ^ <* c *>) by FINSOP_1:5
.= Product<* b,c *> by FINSEQ_1:def 9
.= Product<* b |^ p, c *> by GROUP_1:26
.= Product<* b |^ p, c |^ p *> by GROUP_1:26
.= Product(<* b,c *> |^ <* @p,@p *>) by Th23;
hence a in H1 "\/" H2 by A5,A4,Th28;
end;
then
A6: H is Subgroup of H1 "\/" H2 by GROUP_2:58;
carr H1 \/ carr H2 c= carr H1 * carr H2
proof
let x be object;
assume
A7: x in carr H1 \/ carr H2;
then reconsider a = x as Element of G;
now
per cases by A7,XBOOLE_0:def 3;
suppose
A8: x in carr H1;
1_G in H2 by GROUP_2:46;
then
A9: 1_G in carr H2 by STRUCT_0:def 5;
a * 1_G = a by GROUP_1:def 4;
hence thesis by A8,A9;
end;
suppose
A10: x in carr H2;
1_G in H1 by GROUP_2:46;
then
A11: 1_G in carr H1 by STRUCT_0:def 5;
1_G * a = a by GROUP_1:def 4;
hence thesis by A10,A11;
end;
end;
hence thesis;
end;
then H1 "\/" H2 is Subgroup of H by A1,Def4;
hence thesis by A1,A6,GROUP_2:55;
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 GROUP_2:25;
hence thesis by Th51;
end;
theorem Th53:
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 GROUP_3:125;
hence thesis by Th51;
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;
(ex N being strict normal Subgroup of G st the carrier of N = carr N1 *
carr N2 )& the carrier of N1 "\/" N2 = N1 * N2 by Th53,GROUP_3:126;
hence thesis by GROUP_2:59;
end;
theorem
for H being strict Subgroup of G holds H "\/" H = H by Th31;
theorem
H1 "\/" H2 = H2 "\/" H1;
Lm4: 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) by Def4,XBOOLE_1:7;
hence thesis by GROUP_2:57,XBOOLE_1:1;
end;
Lm5: 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 Th28;
rng F c= carr gr(carr H1 \/ carr(H2 "\/" H3))
proof
let x be object;
assume
A4: x in rng F;
now
per cases by A2,A4,XBOOLE_0:def 3;
suppose
A5: x in carr(H1 "\/" H2);
then reconsider b = x as Element of G;
x in H1 "\/" H2 by A5,STRUCT_0:def 5;
then consider F1,I1 such that
A6: len F1 = len I1 and
A7: rng F1 c= carr H1 \/ carr H2 and
A8: b = Product(F1 |^ I1) by Th28;
H2 is Subgroup of H2 "\/" H3 by Lm4;
then the carrier of H2 c= the carrier of H2 "\/" H3 by GROUP_2:def 5;
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 A7;
then b in H1 "\/" (H2 "\/" H3) by A6,A8,Th28;
hence thesis by STRUCT_0:def 5;
end;
suppose
A9: x in carr H3;
A10: H3 is Subgroup of H3 "\/" H2 by Lm4;
x in H3 by A9,STRUCT_0:def 5;
then x in H3 "\/" H2 by A10,GROUP_2:40;
then x in carr(H2 "\/" H3) by STRUCT_0:def 5;
then
A11: x in carr H1 \/ carr(H2 "\/" H3) by XBOOLE_0:def 3;
carr H1 \/ carr(H2 "\/" H3) c= the carrier of gr(carr H1 \/
carr(H2 "\/" H3)) by Def4;
hence thesis by A11;
end;
end;
hence thesis;
end;
then a in gr carr gr(carr H1 \/ carr(H2 "\/" H3)) by A1,A3,Th28;
hence a in H1 "\/" (H2 "\/" H3) by Th31;
end;
hence thesis by GROUP_2:58;
end;
theorem Th57:
H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3)
proof
H2 "\/" H3 "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) & H3 "\/" H1 "\/"
H2 is Subgroup of H3 "\/" (H1 "\/" H2) by Lm5;
then
A1: H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:56;
H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm5;
hence thesis by A1,GROUP_2:55;
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;
1_G in H by GROUP_2:46;
then 1_G in carr H by STRUCT_0:def 5;
then {1_G} c= carr H by ZFMISC_1:31;
then
A1: carr(1).G = {1_G} & {1_G} \/ carr H = carr H by GROUP_2:def 7,XBOOLE_1:12;
hence (1).G "\/" H = H by Th31;
thus thesis by A1,Th31;
end;
theorem Th59:
(Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G
proof
A1: (the carrier of (Omega). G) \/ carr H = [#] the carrier of G by SUBSET_1:11
;
hence (Omega).G "\/" H = (Omega).G by Th31;
thus thesis by A1,Th31;
end;
theorem Th60:
H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2
proof
H1 "\/" H2 = H2 "\/" H1;
hence thesis by Lm4;
end;
theorem Th61:
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 the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
hence H1 "\/" H2 = gr carr H2 by XBOOLE_1:12
.= H2 by Th31;
end;
thus thesis by Th60;
end;
theorem
H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3
proof
H2 is Subgroup of H2 "\/" H3 by Th60;
hence thesis by GROUP_2:56;
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
A1: H1 is Subgroup of H3 & H2 is Subgroup of H3;
now
let a;
assume a in H1 "\/" H2;
then consider F,I such that
A2: len F = len I and
A3: rng F c= carr H1 \/ carr H2 and
A4: a = Product(F |^ I) by Th28;
the carrier of H1 c= the carrier of H3 & the carrier of H2 c= the
carrier of H3 by A1,GROUP_2:def 5;
then carr H1 \/ carr H2 c= carr H3 by XBOOLE_1:8;
then rng F c= carr H3 by A3;
then a in gr carr H3 by A2,A4,Th28;
hence a in H3 by Th31;
end;
hence thesis by GROUP_2:58;
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 Th57
.= H1 "\/" (H3 "\/" H2) "\/" H3 by Th57
.= H1 "\/" (H2 "\/" H3) "\/" H3
.= H1 "\/" H2 "\/" H3 "\/" H3 by Th57
.= H2 "\/" H3 "\/" H3 by A1,Th61
.= H2 "\/" (H3 "\/" H3) by Th57
.= H2 "\/" H3 by Th31;
hence thesis by Th61;
end;
theorem
H1 /\ H2 is Subgroup of H1 "\/" H2
proof
H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2 by Th60,GROUP_2:88;
hence thesis by GROUP_2:56;
end;
theorem Th66:
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:88;
hence thesis by Th61;
end;
theorem Th67:
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 Th60;
hence thesis by GROUP_2:89;
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 by Th61;
hence thesis by GROUP_2:89;
end;
reserve S1,S2 for Element of Subgroups G;
definition
let G;
func SubJoin G -> BinOp of Subgroups G means
:Def10:
for H1,H2 being strict Subgroup of G holds it.(H1,H2) = 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;
consider o being BinOp of Subgroups G such that
A2: for a,b being Element of Subgroups G holds P[a,b,o.(a,b)] from
BINOP_1:sch 3(A1);
take o;
let H1,H2 be strict Subgroup of G;
H1 in Subgroups G & H2 in Subgroups G by GROUP_3:def 1;
hence thesis by A2;
end;
uniqueness
proof
let o1,o2 be BinOp of Subgroups(G);
assume that
A3: for H1,H2 be strict Subgroup of G holds o1.(H1,H2) = H1 "\/" H2 and
A4: for H1,H2 be strict Subgroup of G holds o2.(H1,H2) = H1 "\/" H2;
now
let x,y be set;
assume
A5: 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 strict Subgroup of G by A5,GROUP_3:def 1;
o1.(A,B) = H1 "\/" H2 by A3;
hence o1.(x,y) = o2.(x,y) by A4;
end;
hence thesis by BINOP_1:1;
end;
end;
definition
let G;
func SubMeet G -> BinOp of Subgroups G means
:Def11:
for H1,H2 being strict Subgroup of G holds it.(H1,H2) = 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;
consider o being BinOp of Subgroups G such that
A2: for a,b being Element of Subgroups G holds P[a,b,o.(a,b)] from
BINOP_1:sch 3(A1);
take o;
let H1,H2 be strict Subgroup of G;
H1 in Subgroups G & H2 in Subgroups G by GROUP_3:def 1;
hence thesis by A2;
end;
uniqueness
proof
let o1,o2 be BinOp of Subgroups(G);
assume that
A3: for H1,H2 be strict Subgroup of G holds o1.(H1,H2) = H1 /\ H2 and
A4: for H1,H2 be strict Subgroup of G holds o2.(H1,H2) = H1 /\ H2;
now
let x,y be set;
assume
A5: 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 strict Subgroup of G by A5,GROUP_3:def 1;
o1.(A,B) = H1 /\ H2 by A3;
hence o1.(x,y) = o2.(x,y) by A4;
end;
hence thesis by BINOP_1:1;
end;
end;
Lm6: 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
set L = LattStr (# Subgroups G, SubJoin G, SubMeet G #);
A1: now
let A,B be Element of L;
let H1,H2 be strict Subgroup of G;
assume
A2: A = H1 & B = H2;
thus A "\/" B = SubJoin(G).(A,B) by LATTICES:def 1
.= H1 "\/" H2 by A2,Def10;
end;
A3: now
let A,B be Element of L;
let H1,H2 be strict Subgroup of G;
assume
A4: A = H1 & B = H2;
thus A "/\" B = SubMeet(G).(A,B) by LATTICES:def 2
.= 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;
A5: H2 "\/" H3 = B "\/" C by A1;
thus A "\/" B = H1 "\/" H2 by A1
.= H2 "\/" H1
.= B "\/" A by A1;
A6: H1 "\/" H2 = A "\/" B by A1;
hence A "\/" B "\/" C = H1 "\/" H2 "\/" H3 by A1
.= H1 "\/" (H2 "\/" H3) by Th57
.= A "\/" (B "\/" C) by A1,A5;
A7: H1 /\ H2 = A "/\" B by A3;
hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A1
.= B by Th66;
A8: H2 /\ H3 = B "/\" C by A3;
thus A "/\" B = H2 /\ H1 by A3
.= B "/\" A by A3;
thus A "/\" B "/\" C = H1 /\ H2 /\ H3 by A3,A7
.= H1 /\ (H2 /\ H3) by GROUP_2:84
.= A "/\" (B "/\" C) by A3,A8;
thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A3,A6
.= A by Th67;
end;
then
A9: 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;
reconsider L as Lattice by A9;
reconsider E = (1).G as Element of L by GROUP_3:def 1;
now
let A be Element of L;
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus E "/\" A = (1).G /\ H by A3
.= E by GROUP_2:85;
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 strict Subgroup of G by GROUP_3:def 1;
thus F "\/" A = (Omega).G "\/" H by A1
.= F by Th59;
hence A "\/" F = F;
end;
hence thesis by LATTICES:def 14;
end;
definition
let G be Group;
func lattice G -> strict Lattice equals
LattStr (# Subgroups G, SubJoin G,
SubMeet G #);
coherence by Lm6;
end;
theorem
the carrier of lattice G = Subgroups G;
theorem
the L_join of lattice G = SubJoin G;
theorem
the L_meet of lattice G = SubMeet G;
registration
let G be Group;
cluster lattice G -> lower-bounded upper-bounded;
coherence by Lm6;
end;
theorem
Bottom lattice G = (1).G
proof
set L = lattice G;
reconsider E = (1).G as Element of L by GROUP_3:def 1;
now
let A be Element of L;
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus A "/\" E = SubMeet(G).(A,E) by LATTICES:def 2
.= H /\ (1).G by Def11
.= E by GROUP_2:85;
end;
hence thesis by RLSUB_2:64;
end;
theorem
Top lattice G = (Omega).G
proof
set L = lattice G;
reconsider E = (Omega). G as Element of L by GROUP_3:def 1;
now
let A be Element of L;
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus A "\/" E = SubJoin(G).(A,E) by LATTICES:def 1
.= H "\/" (Omega).G by Def10
.= E by Th59;
end;
hence thesis by RLSUB_2:65;
end;