:: GROUP_4 semantic presentation

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be set ;
redefine func - as c2 - c3 -> FinSequence of a1;
coherence
c2 - c3 is FinSequence of c1
by FINSEQ_3:93;
end;

scheme :: GROUP_4:sch 1
s1{ F1() -> Group, P1[ set ] } :
ex b1 being strict Subgroup of F1() st the carrier of b1 = meet { b2 where B is Subset of F1() : ex b1 being strict Subgroup of F1() st
( b2 = the carrier of b3 & P1[b3] )
}
provided
E1: ex b1 being strict Subgroup of F1() st P1[b1]
proof end;

scheme :: GROUP_4:sch 2
s2{ F1() -> Group, P1[ set ] } :
ex b1 being set st
( b1 c= Subgroups F1() & ( for b2 being strict Subgroup of F1() holds
( b2 in b1 iff P1[b2] ) ) )
proof end;

definition
let c1 be Integer;
canceled;
func @ c1 -> Element of INT equals :: GROUP_4:def 2
a1;
coherence
c1 is Element of INT
by INT_1:def 2;
end;

:: deftheorem Def1 GROUP_4:def 1 :
canceled;

:: deftheorem Def2 defines @ GROUP_4:def 2 :
for b1 being Integer holds @ b1 = b1;

theorem Th1: :: GROUP_4:1
canceled;

theorem Th2: :: GROUP_4:2
canceled;

theorem Th3: :: GROUP_4:3
for b1 being Nat
for b2 being Group
for b3 being Element of b2
for b4 being Subgroup of b2
for b5 being Element of b4 st b3 = b5 holds
b3 |^ b1 = b5 |^ b1
proof end;

theorem Th4: :: GROUP_4:4
for b1 being Integer
for b2 being Group
for b3 being Element of b2
for b4 being Subgroup of b2
for b5 being Element of b4 st b3 = b5 holds
b3 |^ b1 = b5 |^ b1
proof end;

theorem Th5: :: GROUP_4:5
for b1 being Nat
for b2 being Group
for b3 being Element of b2
for b4 being Subgroup of b2 st b3 in b4 holds
b3 |^ b1 in b4
proof end;

theorem Th6: :: GROUP_4:6
for b1 being Integer
for b2 being Group
for b3 being Element of b2
for b4 being Subgroup of b2 st b3 in b4 holds
b3 |^ b1 in b4
proof end;

definition
let c1 be non empty HGrStr ;
let c2 be FinSequence of the carrier of c1;
func Product c2 -> Element of a1 equals :: GROUP_4:def 3
the mult of a1 "**" a2;
correctness
coherence
the mult of c1 "**" c2 is Element of c1
;
;
end;

:: deftheorem Def3 defines Product GROUP_4:def 3 :
for b1 being non empty HGrStr
for b2 being FinSequence of the carrier of b1 holds Product b2 = the mult of b1 "**" b2;

theorem Th7: :: GROUP_4:7
canceled;

theorem Th8: :: GROUP_4:8
for b1 being non empty unital associative HGrStr
for b2, b3 being FinSequence of the carrier of b1 holds Product (b2 ^ b3) = (Product b2) * (Product b3)
proof end;

theorem Th9: :: GROUP_4:9
for b1 being non empty unital HGrStr
for b2 being FinSequence of the carrier of b1
for b3 being Element of b1 holds Product (b2 ^ <*b3*>) = (Product b2) * b3
proof end;

theorem Th10: :: GROUP_4:10
for b1 being non empty unital associative HGrStr
for b2 being FinSequence of the carrier of b1
for b3 being Element of b1 holds Product (<*b3*> ^ b2) = b3 * (Product b2)
proof end;

theorem Th11: :: GROUP_4:11
for b1 being non empty unital HGrStr holds Product (<*> the carrier of b1) = 1. b1
proof end;

theorem Th12: :: GROUP_4:12
for b1 being non empty HGrStr
for b2 being Element of b1 holds Product <*b2*> = b2 by FINSOP_1:12;

theorem Th13: :: GROUP_4:13
for b1 being non empty HGrStr
for b2, b3 being Element of b1 holds Product <*b2,b3*> = b2 * b3
proof end;

theorem Th14: :: GROUP_4:14
for b1 being Group
for b2, b3, b4 being Element of b1 holds
( Product <*b2,b3,b4*> = (b2 * b3) * b4 & Product <*b2,b3,b4*> = b2 * (b3 * b4) )
proof end;

E10: now
let c1 be Group;
let c2 be Element of c1;
thus Product (0 |-> c2) = Product (<*> the carrier of c1) by FINSEQ_2:72
.= 1. c1 by Th11
.= c2 |^ 0 by GROUP_1:43 ;
end;

E11: now
let c1 be Group;
let c2 be Element of c1;
let c3 be Nat;
assume E12: Product (c3 |-> c2) = c2 |^ c3 ;
thus Product ((c3 + 1) |-> c2) = Product ((c3 |-> c2) ^ <*c2*>) by FINSEQ_2:74
.= (Product (c3 |-> c2)) * (Product <*c2*>) by Th8
.= (c2 |^ c3) * c2 by E12, Th12
.= c2 |^ (c3 + 1) by GROUP_1:49 ;
end;

theorem Th15: :: GROUP_4:15
for b1 being Nat
for b2 being Group
for b3 being Element of b2 holds Product (b1 |-> b3) = b3 |^ b1
proof end;

theorem Th16: :: GROUP_4:16
for b1 being Group
for b2 being FinSequence of the carrier of b1 holds Product (b2 - {(1. b1)}) = Product b2
proof end;

Lemma12: for b1 being FinSequence
for b2 being Nat st b2 in dom b1 holds
( ((len b1) - b2) + 1 is Nat & ((len b1) - b2) + 1 >= 1 & ((len b1) - b2) + 1 <= len b1 )
proof end;

theorem Th17: :: GROUP_4:17
for b1 being Group
for b2, b3 being FinSequence of the carrier of b1 st len b2 = len b3 & ( for b4 being Nat st b4 in dom b2 holds
b3 . (((len b2) - b4) + 1) = (b2 /. b4) " ) holds
Product b2 = (Product b3) "
proof end;

theorem Th18: :: GROUP_4:18
for b1 being Group
for b2, b3 being FinSequence of the carrier of b1 st b1 is commutative Group holds
for b4 being Permutation of dom b2 st b3 = b2 * b4 holds
Product b2 = Product b3
proof end;

theorem Th19: :: GROUP_4:19
for b1 being Group
for b2, b3 being FinSequence of the carrier of b1 st b1 is commutative Group & b2 is one-to-one & b3 is one-to-one & rng b2 = rng b3 holds
Product b2 = Product b3
proof end;

theorem Th20: :: GROUP_4:20
for b1 being Group
for b2, b3, b4 being FinSequence of the carrier of b1 st b1 is commutative Group & len b2 = len b3 & len b2 = len b4 & ( for b5 being Nat st b5 in dom b2 holds
b2 . b5 = (b3 /. b5) * (b4 /. b5) ) holds
Product b2 = (Product b3) * (Product b4)
proof end;

theorem Th21: :: GROUP_4:21
for b1 being Group
for b2 being Subgroup of b1
for b3 being FinSequence of the carrier of b1 st rng b3 c= carr b2 holds
Product b3 in b2
proof end;

definition
let c1 be Group;
let c2 be FinSequence of INT ;
let c3 be FinSequence of the carrier of c1;
func c3 |^ c2 -> FinSequence of the carrier of a1 means :Def4: :: GROUP_4:def 4
( len a4 = len a3 & ( for b1 being Nat st b1 in dom a3 holds
a4 . b1 = (a3 /. b1) |^ (@ (a2 /. b1)) ) );
existence
ex b1 being FinSequence of the carrier of c1 st
( len b1 = len c3 & ( for b2 being Nat st b2 in dom c3 holds
b1 . b2 = (c3 /. b2) |^ (@ (c2 /. b2)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of c1 st len b1 = len c3 & ( for b3 being Nat st b3 in dom c3 holds
b1 . b3 = (c3 /. b3) |^ (@ (c2 /. b3)) ) & len b2 = len c3 & ( for b3 being Nat st b3 in dom c3 holds
b2 . b3 = (c3 /. b3) |^ (@ (c2 /. b3)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines |^ GROUP_4:def 4 :
for b1 being Group
for b2 being FinSequence of INT
for b3, b4 being FinSequence of the carrier of b1 holds
( b4 = b3 |^ b2 iff ( len b4 = len b3 & ( for b5 being Nat st b5 in dom b3 holds
b4 . b5 = (b3 /. b5) |^ (@ (b2 /. b5)) ) ) );

theorem Th22: :: GROUP_4:22
canceled;

theorem Th23: :: GROUP_4:23
canceled;

theorem Th24: :: GROUP_4:24
canceled;

theorem Th25: :: GROUP_4:25
for b1 being Group
for b2, b3 being FinSequence of the carrier of b1
for b4, b5 being FinSequence of INT st len b2 = len b4 & len b3 = len b5 holds
(b2 ^ b3) |^ (b4 ^ b5) = (b2 |^ b4) ^ (b3 |^ b5)
proof end;

theorem Th26: :: GROUP_4:26
for b1 being Group
for b2 being Subgroup of b1
for b3 being FinSequence of the carrier of b1
for b4 being FinSequence of INT st rng b3 c= carr b2 holds
Product (b3 |^ b4) in b2
proof end;

theorem Th27: :: GROUP_4:27
for b1 being Group holds (<*> the carrier of b1) |^ (<*> INT ) = {}
proof end;

theorem Th28: :: GROUP_4:28
for b1 being Integer
for b2 being Group
for b3 being Element of b2 holds <*b3*> |^ <*(@ b1)*> = <*(b3 |^ b1)*>
proof end;

theorem Th29: :: GROUP_4:29
for b1, b2 being Integer
for b3 being Group
for b4, b5 being Element of b3 holds <*b4,b5*> |^ <*(@ b1),(@ b2)*> = <*(b4 |^ b1),(b5 |^ b2)*>
proof end;

theorem Th30: :: GROUP_4:30
for b1, b2, b3 being Integer
for b4 being Group
for b5, b6, b7 being Element of b4 holds <*b5,b6,b7*> |^ <*(@ b1),(@ b2),(@ b3)*> = <*(b5 |^ b1),(b6 |^ b2),(b7 |^ b3)*>
proof end;

theorem Th31: :: GROUP_4:31
for b1 being Group
for b2 being FinSequence of the carrier of b1 holds b2 |^ ((len b2) |-> (@ 1)) = b2
proof end;

theorem Th32: :: GROUP_4:32
for b1 being Group
for b2 being FinSequence of the carrier of b1 holds b2 |^ ((len b2) |-> (@ 0)) = (len b2) |-> (1. b1)
proof end;

theorem Th33: :: GROUP_4:33
for b1 being Nat
for b2 being Group
for b3 being FinSequence of INT st len b3 = b1 holds
(b1 |-> (1. b2)) |^ b3 = b1 |-> (1. b2)
proof end;

definition
let c1 be Group;
let c2 be Subset of c1;
func gr c2 -> strict Subgroup of a1 means :Def5: :: GROUP_4:def 5
( a2 c= the carrier of a3 & ( for b1 being strict Subgroup of a1 st a2 c= the carrier of b1 holds
a3 is Subgroup of b1 ) );
existence
ex b1 being strict Subgroup of c1 st
( c2 c= the carrier of b1 & ( for b2 being strict Subgroup of c1 st c2 c= the carrier of b2 holds
b1 is Subgroup of b2 ) )
proof end;
uniqueness
for b1, b2 being strict Subgroup of c1 st c2 c= the carrier of b1 & ( for b3 being strict Subgroup of c1 st c2 c= the carrier of b3 holds
b1 is Subgroup of b3 ) & c2 c= the carrier of b2 & ( for b3 being strict Subgroup of c1 st c2 c= the carrier of b3 holds
b2 is Subgroup of b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines gr GROUP_4:def 5 :
for b1 being Group
for b2 being Subset of b1
for b3 being strict Subgroup of b1 holds
( b3 = gr b2 iff ( b2 c= the carrier of b3 & ( for b4 being strict Subgroup of b1 st b2 c= the carrier of b4 holds
b3 is Subgroup of b4 ) ) );

theorem Th34: :: GROUP_4:34
canceled;

theorem Th35: :: GROUP_4:35
canceled;

theorem Th36: :: GROUP_4:36
canceled;

theorem Th37: :: GROUP_4:37
for b1 being Group
for b2 being Element of b1
for b3 being Subset of b1 holds
( b2 in gr b3 iff ex b4 being FinSequence of the carrier of b1ex b5 being FinSequence of INT st
( len b4 = len b5 & rng b4 c= b3 & Product (b4 |^ b5) = b2 ) )
proof end;

theorem Th38: :: GROUP_4:38
for b1 being Group
for b2 being Element of b1
for b3 being Subset of b1 st b2 in b3 holds
b2 in gr b3
proof end;

theorem Th39: :: GROUP_4:39
for b1 being Group holds gr ({} the carrier of b1) = (1). b1
proof end;

theorem Th40: :: GROUP_4:40
for b1 being Group
for b2 being strict Subgroup of b1 holds gr (carr b2) = b2
proof end;

theorem Th41: :: GROUP_4:41
for b1 being Group
for b2, b3 being Subset of b1 st b2 c= b3 holds
gr b2 is Subgroup of gr b3
proof end;

theorem Th42: :: GROUP_4:42
for b1 being Group
for b2, b3 being Subset of b1 holds gr (b2 /\ b3) is Subgroup of (gr b2) /\ (gr b3)
proof end;

theorem Th43: :: GROUP_4:43
for b1 being Group
for b2 being Subset of b1 holds the carrier of (gr b2) = meet { b3 where B is Subset of b1 : ex b1 being strict Subgroup of b1 st
( b3 = the carrier of b4 & b2 c= carr b4 )
}
proof end;

theorem Th44: :: GROUP_4:44
for b1 being Group
for b2 being Subset of b1 holds gr b2 = gr (b2 \ {(1. b1)})
proof end;

definition
let c1 be Group;
let c2 be Element of c1;
attr a2 is generating means :Def6: :: GROUP_4:def 6
ex b1 being Subset of a1 st
( gr b1 = HGrStr(# the carrier of a1,the mult of a1 #) & not gr (b1 \ {a2}) = HGrStr(# the carrier of a1,the mult of a1 #) );
end;

:: deftheorem Def6 defines generating GROUP_4:def 6 :
for b1 being Group
for b2 being Element of b1 holds
( b2 is generating iff ex b3 being Subset of b1 st
( gr b3 = HGrStr(# the carrier of b1,the mult of b1 #) & not gr (b3 \ {b2}) = HGrStr(# the carrier of b1,the mult of b1 #) ) );

theorem Th45: :: GROUP_4:45
canceled;

theorem Th46: :: GROUP_4:46
for b1 being Group holds not 1. b1 is generating
proof end;

definition
let c1 be Group;
let c2 be Subgroup of c1;
attr a2 is maximal means :Def7: :: GROUP_4:def 7
( HGrStr(# the carrier of a2,the mult of a2 #) <> HGrStr(# the carrier of a1,the mult of a1 #) & ( for b1 being strict Subgroup of a1 st HGrStr(# the carrier of a2,the mult of a2 #) <> b1 & a2 is Subgroup of b1 holds
b1 = HGrStr(# the carrier of a1,the mult of a1 #) ) );
end;

:: deftheorem Def7 defines maximal GROUP_4:def 7 :
for b1 being Group
for b2 being Subgroup of b1 holds
( b2 is maximal iff ( HGrStr(# the carrier of b2,the mult of b2 #) <> HGrStr(# the carrier of b1,the mult of b1 #) & ( for b3 being strict Subgroup of b1 st HGrStr(# the carrier of b2,the mult of b2 #) <> b3 & b2 is Subgroup of b3 holds
b3 = HGrStr(# the carrier of b1,the mult of b1 #) ) ) );

theorem Th47: :: GROUP_4:47
canceled;

theorem Th48: :: GROUP_4:48
for b1 being strict Group
for b2 being strict Subgroup of b1
for b3 being Element of b1 st b2 is maximal & not b3 in b2 holds
gr ((carr b2) \/ {b3}) = b1
proof end;

definition
let c1 be Group;
func Phi c1 -> strict Subgroup of a1 means :Def8: :: GROUP_4:def 8
the carrier of a2 = meet { b1 where B is Subset of a1 : ex b1 being strict Subgroup of a1 st
( b1 = the carrier of b2 & b2 is maximal )
}
if ex b1 being strict Subgroup of a1 st b1 is maximal
otherwise a2 = HGrStr(# the carrier of a1,the mult of a1 #);
existence
( ( ex b1 being strict Subgroup of c1 st b1 is maximal implies ex b1 being strict Subgroup of c1 st the carrier of b1 = meet { b2 where B is Subset of c1 : ex b1 being strict Subgroup of c1 st
( b2 = the carrier of b3 & b3 is maximal )
}
) & ( ( for b1 being strict Subgroup of c1 holds not b1 is maximal ) implies ex b1 being strict Subgroup of c1 st b1 = HGrStr(# the carrier of c1,the mult of c1 #) ) )
proof end;
uniqueness
for b1, b2 being strict Subgroup of c1 holds
( ( ex b3 being strict Subgroup of c1 st b3 is maximal & the carrier of b1 = meet { b3 where B is Subset of c1 : ex b1 being strict Subgroup of c1 st
( b3 = the carrier of b4 & b4 is maximal )
}
& the carrier of b2 = meet { b3 where B is Subset of c1 : ex b1 being strict Subgroup of c1 st
( b3 = the carrier of b4 & b4 is maximal )
}
implies b1 = b2 ) & ( ( for b3 being strict Subgroup of c1 holds not b3 is maximal ) & b1 = HGrStr(# the carrier of c1,the mult of c1 #) & b2 = HGrStr(# the carrier of c1,the mult of c1 #) implies b1 = b2 ) )
by GROUP_2:68;
correctness
consistency
for b1 being strict Subgroup of c1 holds verum
;
;
end;

:: deftheorem Def8 defines Phi GROUP_4:def 8 :
for b1 being Group
for b2 being strict Subgroup of b1 holds
( ( ex b3 being strict Subgroup of b1 st b3 is maximal implies ( b2 = Phi b1 iff the carrier of b2 = meet { b3 where B is Subset of b1 : ex b1 being strict Subgroup of b1 st
( b3 = the carrier of b4 & b4 is maximal )
}
) ) & ( ( for b3 being strict Subgroup of b1 holds not b3 is maximal ) implies ( b2 = Phi b1 iff b2 = HGrStr(# the carrier of b1,the mult of b1 #) ) ) );

theorem Th49: :: GROUP_4:49
canceled;

theorem Th50: :: GROUP_4:50
canceled;

theorem Th51: :: GROUP_4:51
canceled;

theorem Th52: :: GROUP_4:52
for b1 being Group
for b2 being Element of b1
for b3 being Group st ex b4 being strict Subgroup of b3 st b4 is maximal holds
( b2 in Phi b3 iff for b4 being strict Subgroup of b3 st b4 is maximal holds
b2 in b4 )
proof end;

theorem Th53: :: GROUP_4:53
for b1 being Group
for b2 being Element of b1 st ( for b3 being strict Subgroup of b1 holds not b3 is maximal ) holds
b2 in Phi b1
proof end;

theorem Th54: :: GROUP_4:54
for b1 being Group
for b2 being strict Subgroup of b1 st b2 is maximal holds
Phi b1 is Subgroup of b2
proof end;

theorem Th55: :: GROUP_4:55
for b1 being strict Group holds the carrier of (Phi b1) = { b2 where B is Element of b1 : not b2 is generating }
proof end;

theorem Th56: :: GROUP_4:56
for b1 being strict Group
for b2 being Element of b1 holds
( b2 in Phi b1 iff not b2 is generating )
proof end;

definition
let c1 be Group;
let c2, c3 be Subgroup of c1;
func c2 * c3 -> Subset of a1 equals :: GROUP_4:def 9
(carr a2) * (carr a3);
correctness
coherence
(carr c2) * (carr c3) is Subset of c1
;
;
end;

:: deftheorem Def9 defines * GROUP_4:def 9 :
for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 * b3 = (carr b2) * (carr b3);

theorem Th57: :: GROUP_4:57
for b1 being Group
for b2, b3 being Subgroup of b1 holds
( b2 * b3 = (carr b2) * (carr b3) & b2 * b3 = b2 * (carr b3) & b2 * b3 = (carr b2) * b3 ) by GROUP_2:def 11, GROUP_2:def 12;

theorem Th58: :: GROUP_4:58
for b1 being Group
for b2 being Subgroup of b1 holds b2 * b2 = carr b2 by GROUP_2:91;

theorem Th59: :: GROUP_4:59
for b1 being Group
for b2, b3, b4 being Subgroup of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4)
proof end;

theorem Th60: :: GROUP_4:60
for b1 being Group
for b2 being Element of b1
for b3, b4 being Subgroup of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4)
proof end;

theorem Th61: :: GROUP_4:61
for b1 being Group
for b2 being Element of b1
for b3, b4 being Subgroup of b1 holds (b3 * b4) * b2 = b3 * (b4 * b2)
proof end;

theorem Th62: :: GROUP_4:62
for b1 being Group
for b2 being Subset of b1
for b3, b4 being Subgroup of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4)
proof end;

theorem Th63: :: GROUP_4:63
for b1 being Group
for b2 being Subset of b1
for b3, b4 being Subgroup of b1 holds (b3 * b4) * b2 = b3 * (b4 * b2)
proof end;

theorem Th64: :: GROUP_4:64
for b1 being Group
for b2, b3 being strict normal Subgroup of b1 holds b2 * b3 = b3 * b2 by GROUP_3:148;

theorem Th65: :: GROUP_4:65
for b1 being Group
for b2, b3 being Subgroup of b1 st b1 is commutative Group holds
b2 * b3 = b3 * b2 by GROUP_2:29;

definition
let c1 be Group;
let c2, c3 be Subgroup of c1;
func c2 "\/" c3 -> strict Subgroup of a1 equals :: GROUP_4:def 10
gr ((carr a2) \/ (carr a3));
correctness
coherence
gr ((carr c2) \/ (carr c3)) is strict Subgroup of c1
;
;
end;

:: deftheorem Def10 defines "\/" GROUP_4:def 10 :
for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 "\/" b3 = gr ((carr b2) \/ (carr b3));

theorem Th66: :: GROUP_4:66
canceled;

theorem Th67: :: GROUP_4:67
for b1 being Group
for b2 being Element of b1
for b3, b4 being Subgroup of b1 holds
( b2 in b3 "\/" b4 iff ex b5 being FinSequence of the carrier of b1ex b6 being FinSequence of INT st
( len b5 = len b6 & rng b5 c= (carr b3) \/ (carr b4) & b2 = Product (b5 |^ b6) ) ) by Th37;

Lemma39: for b1 being natural number holds
( b1 mod 2 = 0 or b1 mod 2 = 1 )
by NAT_1:62;

Lemma40: for b1, b2 being natural number holds (b1 * b2) mod b1 = 0
by NAT_1:63;

Lemma41: for b1, b2 being natural number st b1 > 1 holds
1 mod b1 = 1
by NAT_1:64;

Lemma42: for b1, b2, b3, b4 being natural number st b1 mod b3 = 0 & b2 = b1 - (b4 * b3) holds
b2 mod b3 = 0
by NAT_1:65;

Lemma43: for b1, b2, b3 being natural number st b3 <> 0 & b1 mod b3 = 0 & b2 < b3 holds
(b1 + b2) mod b3 = b2
by NAT_1:66;

Lemma44: for b1, b2 being natural number st b1 <> 0 holds
(b1 * b2) div b1 = b2
by NAT_1:68;

Lemma45: for b1, b2, b3 being natural number st b1 mod b2 = 0 holds
(b1 + b3) div b2 = (b1 div b2) + (b3 div b2)
by NAT_1:69;

theorem Th68: :: GROUP_4:68
for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 "\/" b3 = gr (b2 * b3)
proof end;

theorem Th69: :: GROUP_4:69
for b1 being Group
for b2, b3 being Subgroup of b1 st b2 * b3 = b3 * b2 holds
the carrier of (b2 "\/" b3) = b2 * b3
proof end;

theorem Th70: :: GROUP_4:70
for b1 being Group
for b2, b3 being Subgroup of b1 st b1 is commutative Group holds
the carrier of (b2 "\/" b3) = b2 * b3
proof end;

theorem Th71: :: GROUP_4:71
for b1 being Group
for b2, b3 being strict normal Subgroup of b1 holds the carrier of (b2 "\/" b3) = b2 * b3
proof end;

theorem Th72: :: GROUP_4:72
for b1 being Group
for b2, b3 being strict normal Subgroup of b1 holds b2 "\/" b3 is normal Subgroup of b1
proof end;

theorem Th73: :: GROUP_4:73
for b1 being Group
for b2 being strict Subgroup of b1 holds b2 "\/" b2 = b2 by Th40;

theorem Th74: :: GROUP_4:74
for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 "\/" b3 = b3 "\/" b2 ;

Lemma49: for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 is Subgroup of b2 "\/" b3
proof end;

Lemma50: for b1 being Group
for b2, b3, b4 being Subgroup of b1 holds (b2 "\/" b3) "\/" b4 is Subgroup of b2 "\/" (b3 "\/" b4)
proof end;

theorem Th75: :: GROUP_4:75
for b1 being Group
for b2, b3, b4 being Subgroup of b1 holds (b2 "\/" b3) "\/" b4 = b2 "\/" (b3 "\/" b4)
proof end;

theorem Th76: :: GROUP_4:76
for b1 being Group
for b2 being strict Subgroup of b1 holds
( ((1). b1) "\/" b2 = b2 & b2 "\/" ((1). b1) = b2 )
proof end;

theorem Th77: :: GROUP_4:77
for b1 being Group
for b2 being Subgroup of b1 holds
( ((Omega). b1) "\/" b2 = (Omega). b1 & b2 "\/" ((Omega). b1) = (Omega). b1 )
proof end;

theorem Th78: :: GROUP_4:78
for b1 being Group
for b2, b3 being Subgroup of b1 holds
( b2 is Subgroup of b2 "\/" b3 & b3 is Subgroup of b2 "\/" b3 )
proof end;

theorem Th79: :: GROUP_4:79
for b1 being Group
for b2 being Subgroup of b1
for b3 being strict Subgroup of b1 holds
( b2 is Subgroup of b3 iff b2 "\/" b3 = b3 )
proof end;

theorem Th80: :: GROUP_4:80
for b1 being Group
for b2, b3, b4 being Subgroup of b1 st b2 is Subgroup of b3 holds
b2 is Subgroup of b3 "\/" b4
proof end;

theorem Th81: :: GROUP_4:81
for b1 being Group
for b2, b3 being Subgroup of b1
for b4 being strict Subgroup of b1 st b2 is Subgroup of b4 & b3 is Subgroup of b4 holds
b2 "\/" b3 is Subgroup of b4
proof end;

theorem Th82: :: GROUP_4:82
for b1 being Group
for b2 being Subgroup of b1
for b3, b4 being strict Subgroup of b1 st b2 is Subgroup of b4 holds
b2 "\/" b3 is Subgroup of b4 "\/" b3
proof end;

theorem Th83: :: GROUP_4:83
for b1 being Group
for b2, b3 being Subgroup of b1 holds b2 /\ b3 is Subgroup of b2 "\/" b3
proof end;

theorem Th84: :: GROUP_4:84
for b1 being Group
for b2 being Subgroup of b1
for b3 being strict Subgroup of b1 holds (b2 /\ b3) "\/" b3 = b3
proof end;

theorem Th85: :: GROUP_4:85
for b1 being Group
for b2 being Subgroup of b1
for b3 being strict Subgroup of b1 holds b3 /\ (b3 "\/" b2) = b3
proof end;

theorem Th86: :: GROUP_4:86
for b1 being Group
for b2, b3 being strict Subgroup of b1 holds
( b2 "\/" b3 = b3 iff b2 /\ b3 = b2 )
proof end;

definition
let c1 be Group;
func SubJoin c1 -> BinOp of Subgroups a1 means :Def11: :: GROUP_4:def 11
for b1, b2 being Element of Subgroups a1
for b3, b4 being Subgroup of a1 st b1 = b3 & b2 = b4 holds
a2 . b1,b2 = b3 "\/" b4;
existence
ex b1 being BinOp of Subgroups c1 st
for b2, b3 being Element of Subgroups c1
for b4, b5 being Subgroup of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 "\/" b5
proof end;
uniqueness
for b1, b2 being BinOp of Subgroups c1 st ( for b3, b4 being Element of Subgroups c1
for b5, b6 being Subgroup of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 "\/" b6 ) & ( for b3, b4 being Element of Subgroups c1
for b5, b6 being Subgroup of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 "\/" b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SubJoin GROUP_4:def 11 :
for b1 being Group
for b2 being BinOp of Subgroups b1 holds
( b2 = SubJoin b1 iff for b3, b4 being Element of Subgroups b1
for b5, b6 being Subgroup of b1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 "\/" b6 );

definition
let c1 be Group;
func SubMeet c1 -> BinOp of Subgroups a1 means :Def12: :: GROUP_4:def 12
for b1, b2 being Element of Subgroups a1
for b3, b4 being Subgroup of a1 st b1 = b3 & b2 = b4 holds
a2 . b1,b2 = b3 /\ b4;
existence
ex b1 being BinOp of Subgroups c1 st
for b2, b3 being Element of Subgroups c1
for b4, b5 being Subgroup of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 /\ b5
proof end;
uniqueness
for b1, b2 being BinOp of Subgroups c1 st ( for b3, b4 being Element of Subgroups c1
for b5, b6 being Subgroup of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 /\ b6 ) & ( for b3, b4 being Element of Subgroups c1
for b5, b6 being Subgroup of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines SubMeet GROUP_4:def 12 :
for b1 being Group
for b2 being BinOp of Subgroups b1 holds
( b2 = SubMeet b1 iff for b3, b4 being Element of Subgroups b1
for b5, b6 being Subgroup of b1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 );

Lemma59: for b1 being Group holds
( LattStr(# (Subgroups b1),(SubJoin b1),(SubMeet b1) #) is Lattice & LattStr(# (Subgroups b1),(SubJoin b1),(SubMeet b1) #) is 0_Lattice & LattStr(# (Subgroups b1),(SubJoin b1),(SubMeet b1) #) is 1_Lattice )
proof end;

definition
let c1 be Group;
func lattice c1 -> strict Lattice equals :: GROUP_4:def 13
LattStr(# (Subgroups a1),(SubJoin a1),(SubMeet a1) #);
coherence
LattStr(# (Subgroups c1),(SubJoin c1),(SubMeet c1) #) is strict Lattice
by Lemma59;
end;

:: deftheorem Def13 defines lattice GROUP_4:def 13 :
for b1 being Group holds lattice b1 = LattStr(# (Subgroups b1),(SubJoin b1),(SubMeet b1) #);

theorem Th87: :: GROUP_4:87
canceled;

theorem Th88: :: GROUP_4:88
canceled;

theorem Th89: :: GROUP_4:89
canceled;

theorem Th90: :: GROUP_4:90
canceled;

theorem Th91: :: GROUP_4:91
canceled;

theorem Th92: :: GROUP_4:92
for b1 being Group holds the carrier of (lattice b1) = Subgroups b1 ;

theorem Th93: :: GROUP_4:93
for b1 being Group holds the L_join of (lattice b1) = SubJoin b1 ;

theorem Th94: :: GROUP_4:94
for b1 being Group holds the L_meet of (lattice b1) = SubMeet b1 ;

registration
let c1 be Group;
cluster lattice a1 -> strict lower-bounded upper-bounded ;
coherence
( lattice c1 is lower-bounded & lattice c1 is upper-bounded )
by Lemma59;
end;

theorem Th95: :: GROUP_4:95
canceled;

theorem Th96: :: GROUP_4:96
canceled;

theorem Th97: :: GROUP_4:97
canceled;

theorem Th98: :: GROUP_4:98
for b1 being Group holds Bottom (lattice b1) = (1). b1
proof end;

theorem Th99: :: GROUP_4:99
for b1 being Group holds Top (lattice b1) = (Omega). b1
proof end;