:: GROUP_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let D be non empty set ;
let F be FinSequence of D;
let X be set ;
:: original: -
redefine func F - X -> FinSequence of D;
coherence
F - X is FinSequence of D
by FINSEQ_3:93;
end;

scheme :: GROUP_4:sch 1
MeetSbgEx{ F1() -> Group, P1[ set ] } :
ex H being strict Subgroup of F1() st the carrier of H = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )
}
provided
A1: ex H being strict Subgroup of F1() st P1[H]
proof end;

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

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

:: deftheorem GROUP_4:def 1 :
canceled;

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

theorem :: GROUP_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: GROUP_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
proof end;

theorem :: GROUP_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ i = h |^ i
proof end;

theorem Th5: :: GROUP_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
proof end;

theorem Th6: :: GROUP_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ i in H
proof end;

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

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

theorem :: GROUP_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: GROUP_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty unital associative HGrStr
for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2)
proof end;

theorem Th9: :: GROUP_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty unital HGrStr
for F being FinSequence of the carrier of G
for a being Element of G holds Product (F ^ <*a*>) = (Product F) * a
proof end;

theorem Th10: :: GROUP_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty unital associative HGrStr
for F being FinSequence of the carrier of G
for a being Element of G holds Product (<*a*> ^ F) = a * (Product F)
proof end;

theorem Th11: :: GROUP_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty unital HGrStr holds Product (<*> the carrier of G) = 1. G
proof end;

theorem Th12: :: GROUP_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for a being Element of G holds Product <*a*> = a by FINSOP_1:12;

theorem Th13: :: GROUP_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for a, b being Element of G holds Product <*a,b*> = a * b
proof end;

theorem :: GROUP_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a, b, c being Element of G holds
( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
proof end;

Lm1: now
let G be Group; :: thesis: for a being Element of G holds Product (0 |-> a) = a |^ 0
let a be Element of G; :: thesis: Product (0 |-> a) = a |^ 0
thus Product (0 |-> a) = Product (<*> the carrier of G) by FINSEQ_2:72
.= 1. G by Th11
.= a |^ 0 by GROUP_1:43 ; :: thesis: verum
end;

Lm2: now
let G be Group; :: thesis: for a being Element of G
for n being Nat st Product (n |-> a) = a |^ n holds
Product ((n + 1) |-> a) = a |^ (n + 1)

let a be Element of G; :: thesis: for n being Nat st Product (n |-> a) = a |^ n holds
Product ((n + 1) |-> a) = a |^ (n + 1)

let n be Nat; :: thesis: ( Product (n |-> a) = a |^ n implies Product ((n + 1) |-> a) = a |^ (n + 1) )
assume A1: Product (n |-> a) = a |^ n ; :: thesis: Product ((n + 1) |-> a) = a |^ (n + 1)
thus Product ((n + 1) |-> a) = Product ((n |-> a) ^ <*a*>) by FINSEQ_2:74
.= (Product (n |-> a)) * (Product <*a*>) by Th8
.= (a |^ n) * a by A1, Th12
.= a |^ (n + 1) by GROUP_1:49 ; :: thesis: verum
end;

theorem :: GROUP_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Group
for a being Element of G holds Product (n |-> a) = a |^ n
proof end;

theorem :: GROUP_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F being FinSequence of the carrier of G holds Product (F - {(1. G)}) = Product F
proof end;

Lm3: for F1 being FinSequence
for y being Nat st y in dom F1 holds
( ((len F1) - y) + 1 is Nat & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
proof end;

theorem Th17: :: GROUP_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "
proof end;

theorem :: GROUP_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F1, F2 being FinSequence of the carrier of G st G is commutative Group holds
for P being Permutation of dom F1 st F2 = F1 * P holds
Product F1 = Product F2
proof end;

theorem :: GROUP_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F1, F2 being FinSequence of the carrier of G st G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 holds
Product F1 = Product F2
proof end;

theorem :: GROUP_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F, F1, F2 being FinSequence of the carrier of G st G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
proof end;

theorem Th21: :: GROUP_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being Subgroup of G
for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
proof end;

definition
let G be Group;
let I be FinSequence of INT ;
let F be FinSequence of the carrier of G;
func F |^ I -> FinSequence of the carrier of G means :Def4: :: GROUP_4:def 4
( len it = len F & ( for k being Nat st k in dom F holds
it . k = (F /. k) |^ (@ (I /. k)) ) );
existence
ex b1 being FinSequence of the carrier of G st
( len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ (@ (I /. k)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ (@ (I /. k)) ) & len b2 = len F & ( for k being Nat st k in dom F holds
b2 . k = (F /. k) |^ (@ (I /. k)) ) holds
b1 = b2
proof end;
end;

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

theorem :: GROUP_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th25: :: GROUP_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F1, F2 being FinSequence of the carrier of G
for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
proof end;

theorem Th26: :: GROUP_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being Subgroup of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
proof end;

theorem Th27: :: GROUP_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds (<*> the carrier of G) |^ (<*> INT ) = {}
proof end;

theorem Th28: :: GROUP_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for G being Group
for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
proof end;

theorem Th29: :: GROUP_4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer
for G being Group
for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
proof end;

theorem :: GROUP_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i3 being Integer
for G being Group
for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
proof end;

theorem :: GROUP_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 1)) = F
proof end;

theorem :: GROUP_4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1. G)
proof end;

theorem :: GROUP_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Group
for I being FinSequence of INT st len I = n holds
(n |-> (1. G)) |^ I = n |-> (1. G)
proof end;

definition
let G be Group;
let A be Subset of G;
func gr A -> strict Subgroup of G means :Def5: :: GROUP_4:def 5
( 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
ex b1 being strict Subgroup of G st
( A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b1 is Subgroup of H ) )
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b1 is Subgroup of H ) & A c= the carrier of b2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b2 is Subgroup of H ) holds
b1 = b2
proof end;
end;

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

theorem :: GROUP_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th37: :: GROUP_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
proof end;

theorem Th38: :: GROUP_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for A being Subset of G st a in A holds
a in gr A
proof end;

theorem :: GROUP_4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds gr ({} the carrier of G) = (1). G
proof end;

theorem Th40: :: GROUP_4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G holds gr (carr H) = H
proof end;

theorem Th41: :: GROUP_4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A, B being Subset of G st A c= B holds
gr A is Subgroup of gr B
proof end;

theorem :: GROUP_4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A, B being Subset of G holds gr (A /\ B) is Subgroup of (gr A) /\ (gr B)
proof end;

theorem Th43: :: GROUP_4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G holds the carrier of (gr A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )
}
proof end;

theorem Th44: :: GROUP_4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G holds gr A = gr (A \ {(1. G)})
proof end;

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

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

theorem :: GROUP_4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds not 1. G is generating
proof end;

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

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

theorem :: GROUP_4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th48: :: GROUP_4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for H being strict Subgroup of G
for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
proof end;

definition
let G be Group;
func Phi G -> strict Subgroup of G means :Def8: :: GROUP_4:def 8
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 = HGrStr(# the carrier of G,the mult of G #);
existence
( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )
}
) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = HGrStr(# the carrier of G,the mult of G #) ) )
proof end;
uniqueness
for b1, b2 being strict Subgroup of G holds
( ( ex H being strict Subgroup of G st H is maximal & the carrier of b1 = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )
}
& the carrier of b2 = meet { A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )
}
implies b1 = b2 ) & ( ( for H being strict Subgroup of G holds not H is maximal ) & b1 = HGrStr(# the carrier of G,the mult of G #) & b2 = HGrStr(# the carrier of G,the mult of G #) implies b1 = b2 ) )
by GROUP_2:68;
correctness
consistency
for b1 being strict Subgroup of G holds verum
;
;
end;

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

theorem :: GROUP_4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th52: :: GROUP_4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
proof end;

theorem :: GROUP_4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G st ( for H being strict Subgroup of G holds not H is maximal ) holds
a in Phi G
proof end;

theorem Th54: :: GROUP_4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G st H is maximal holds
Phi G is Subgroup of H
proof end;

theorem Th55: :: GROUP_4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group holds the carrier of (Phi G) = { a where a is Element of G : not a is generating }
proof end;

theorem :: GROUP_4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being strict Group
for a being Element of G holds
( a in Phi G iff not a is generating )
proof end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
func H1 * H2 -> Subset of G equals :: GROUP_4:def 9
(carr H1) * (carr H2);
correctness
coherence
(carr H1) * (carr H2) is Subset of G
;
;
end;

:: deftheorem defines * GROUP_4:def 9 :
for G being Group
for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2);

theorem Th57: :: GROUP_4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds
( H1 * H2 = (carr H1) * (carr H2) & H1 * H2 = H1 * (carr H2) & H1 * H2 = (carr H1) * H2 ) by GROUP_2:def 11, GROUP_2:def 12;

theorem :: GROUP_4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being Subgroup of G holds H * H = carr H by GROUP_2:91;

theorem :: GROUP_4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 * H2) * H3 = H1 * (H2 * H3)
proof end;

theorem :: GROUP_4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * H2)
proof end;

theorem :: GROUP_4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 * H2) * a = H1 * (H2 * a)
proof end;

theorem :: GROUP_4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2)
proof end;

theorem :: GROUP_4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
proof end;

theorem Th64: :: GROUP_4:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for N1, N2 being strict normal Subgroup of G holds N1 * N2 = N2 * N1 by GROUP_3:148;

theorem Th65: :: GROUP_4:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
H1 * H2 = H2 * H1 by GROUP_2:29;

definition
let G be Group;
let H1, H2 be Subgroup of G;
func H1 "\/" H2 -> strict Subgroup of G equals :: GROUP_4:def 10
gr ((carr H1) \/ (carr H2));
correctness
coherence
gr ((carr H1) \/ (carr H2)) is strict Subgroup of G
;
;
end;

:: deftheorem defines "\/" GROUP_4:def 10 :
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2));

theorem :: GROUP_4:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th67: :: GROUP_4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds
( a in H1 "\/" H2 iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= (carr H1) \/ (carr H2) & a = Product (F |^ I) ) ) by Th37;

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

Lm5: for k, n being natural number holds (k * n) mod k = 0
by NAT_1:63;

Lm6: for k, l being natural number st k > 1 holds
1 mod k = 1
by NAT_1:64;

Lm7: for k, l, n, m being natural number st k mod n = 0 & l = k - (m * n) holds
l mod n = 0
by NAT_1:65;

Lm8: for k, l, n being natural number st n <> 0 & k mod n = 0 & l < n holds
(k + l) mod n = l
by NAT_1:66;

Lm9: for k, n being natural number st k <> 0 holds
(k * n) div k = n
by NAT_1:68;

Lm10: for k, n, l being natural number st k mod n = 0 holds
(k + l) div n = (k div n) + (l div n)
by NAT_1:69;

theorem :: GROUP_4:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2)
proof end;

theorem Th69: :: GROUP_4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
proof end;

theorem :: GROUP_4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
the carrier of (H1 "\/" H2) = H1 * H2
proof end;

theorem Th71: :: GROUP_4:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2
proof end;

theorem :: GROUP_4:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G
proof end;

theorem Th73: :: GROUP_4:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G holds H "\/" H = H by Th40;

theorem :: GROUP_4:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = H2 "\/" H1 ;

Lm11: for G being Group
for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2
proof end;

Lm12: for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
proof end;

theorem Th75: :: GROUP_4:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3)
proof end;

theorem :: GROUP_4:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
proof end;

theorem Th77: :: GROUP_4:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being Subgroup of G holds
( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
proof end;

theorem Th78: :: GROUP_4:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds
( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
proof end;

theorem Th79: :: GROUP_4:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1 being Subgroup of G
for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
proof end;

theorem :: GROUP_4:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 is Subgroup of H2 "\/" H3
proof end;

theorem :: GROUP_4:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
proof end;

theorem :: GROUP_4:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1 being Subgroup of G
for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds
H1 "\/" H3 is Subgroup of H2 "\/" H3
proof end;

theorem :: GROUP_4:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 "\/" H2
proof end;

theorem Th84: :: GROUP_4:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1 being Subgroup of G
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
proof end;

theorem Th85: :: GROUP_4:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
proof end;

theorem :: GROUP_4:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
proof end;

definition
let G be Group;
func SubJoin G -> BinOp of Subgroups G means :Def11: :: GROUP_4:def 11
for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
it . S1,S2 = H1 "\/" H2;
existence
ex b1 being BinOp of Subgroups G st
for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b1 . S1,S2 = H1 "\/" H2
proof end;
uniqueness
for b1, b2 being BinOp of Subgroups G st ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b1 . S1,S2 = H1 "\/" H2 ) & ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b2 . S1,S2 = H1 "\/" H2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SubJoin GROUP_4:def 11 :
for G being Group
for b2 being BinOp of Subgroups G holds
( b2 = SubJoin G iff for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b2 . S1,S2 = H1 "\/" H2 );

definition
let G be Group;
func SubMeet G -> BinOp of Subgroups G means :Def12: :: GROUP_4:def 12
for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
it . S1,S2 = H1 /\ H2;
existence
ex b1 being BinOp of Subgroups G st
for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b1 . S1,S2 = H1 /\ H2
proof end;
uniqueness
for b1, b2 being BinOp of Subgroups G st ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b1 . S1,S2 = H1 /\ H2 ) & ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b2 . S1,S2 = H1 /\ H2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines SubMeet GROUP_4:def 12 :
for G being Group
for b2 being BinOp of Subgroups G holds
( b2 = SubMeet G iff for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
b2 . S1,S2 = H1 /\ H2 );

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

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

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

theorem :: GROUP_4:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds the carrier of (lattice G) = Subgroups G ;

theorem :: GROUP_4:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds the L_join of (lattice G) = SubJoin G ;

theorem :: GROUP_4:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds the L_meet of (lattice G) = SubMeet G ;

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

theorem :: GROUP_4:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GROUP_4:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds Bottom (lattice G) = (1). G
proof end;

theorem :: GROUP_4:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds Top (lattice G) = (Omega). G
proof end;