:: by Wojciech A. Trybulec

::

:: Received August 22, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

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:86;

end;
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:86;

theorem Th1: :: GROUP_4:1

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

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:2

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

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 Th3: :: GROUP_4:3

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

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 Th4: :: GROUP_4:4

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

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 multMagma ;

let F be FinSequence of the carrier of G;

correctness

coherence

the multF of G "**" F is Element of G;

;

end;
let F be FinSequence of the carrier of G;

correctness

coherence

the multF of G "**" F is Element of G;

;

:: deftheorem defines Product GROUP_4:def 2 :

for G being non empty multMagma

for F being FinSequence of the carrier of G holds Product F = the multF of G "**" F;

for G being non empty multMagma

for F being FinSequence of the carrier of G holds Product F = the multF of G "**" F;

theorem :: GROUP_4:5

for G being non empty unital associative multMagma

for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:5;

for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:5;

theorem :: GROUP_4:6

theorem :: GROUP_4:7

for G being non empty unital associative multMagma

for F being FinSequence of the carrier of G

for a being Element of G holds Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:6;

for F being FinSequence of the carrier of G

for a being Element of G holds Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:6;

theorem :: GROUP_4:9

theorem :: GROUP_4:10

theorem :: GROUP_4:11

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) )

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 :: thesis: for G being Group

for a being Element of G holds Product (0 |-> a) = a |^ 0

for a being Element of G holds Product (0 |-> a) = a |^ 0

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)

.= 1_ G by Th8

.= a |^ 0 by GROUP_1:25 ; :: thesis: verum

end;
let a be Element of G; :: thesis: Product (0 |-> a) = a |^ 0

thus Product (0 |-> a) = Product (<*> the carrier of G)

.= 1_ G by Th8

.= a |^ 0 by GROUP_1:25 ; :: thesis: verum

Lm2: now :: thesis: for G being Group

for a being Element of G

for n being Nat st Product (n |-> a) = a |^ n holds

Product ((n + 1) |-> a) = a |^ (n + 1)

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 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: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 ; :: thesis: verum

end;
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: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 ; :: thesis: verum

theorem :: GROUP_4:13

for G being Group

for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F

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 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 end;

theorem Th14: :: GROUP_4:14

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) "

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:15

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

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:16

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

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:17

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)

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 Th18: :: GROUP_4:18

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

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;

ex b_{1} being FinSequence of the carrier of G st

( len b_{1} = len F & ( for k being Nat st k in dom F holds

b_{1} . k = (F /. k) |^ (@ (I /. k)) ) )

for b_{1}, b_{2} being FinSequence of the carrier of G st len b_{1} = len F & ( for k being Nat st k in dom F holds

b_{1} . k = (F /. k) |^ (@ (I /. k)) ) & len b_{2} = len F & ( for k being Nat st k in dom F holds

b_{2} . k = (F /. k) |^ (@ (I /. k)) ) holds

b_{1} = b_{2}

end;
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 :Def3: :: GROUP_4:def 3

( len it = len F & ( for k being Nat st k in dom F holds

it . k = (F /. k) |^ (@ (I /. k)) ) );

existence ( len it = len F & ( for k being Nat st k in dom F holds

it . k = (F /. k) |^ (@ (I /. k)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines |^ GROUP_4:def 3 :

for G being Group

for I being FinSequence of INT

for F, b_{4} being FinSequence of the carrier of G holds

( b_{4} = F |^ I iff ( len b_{4} = len F & ( for k being Nat st k in dom F holds

b_{4} . k = (F /. k) |^ (@ (I /. k)) ) ) );

for G being Group

for I being FinSequence of INT

for F, b

( b

b

theorem Th19: :: GROUP_4:19

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)

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 Th20: :: GROUP_4:20

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

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 Th22: :: GROUP_4:22

for i being Integer

for G being Group

for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>

for G being Group

for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>

proof end;

theorem Th23: :: GROUP_4:23

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)*>

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:24

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)*>

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:26

for G being Group

for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G)

for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G)

proof end;

theorem :: GROUP_4:27

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)

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;

ex b_{1} being strict Subgroup of G st

( A c= the carrier of b_{1} & ( for H being strict Subgroup of G st A c= the carrier of H holds

b_{1} is Subgroup of H ) )

for b_{1}, b_{2} being strict Subgroup of G st A c= the carrier of b_{1} & ( for H being strict Subgroup of G st A c= the carrier of H holds

b_{1} is Subgroup of H ) & A c= the carrier of b_{2} & ( for H being strict Subgroup of G st A c= the carrier of H holds

b_{2} is Subgroup of H ) holds

b_{1} = b_{2}

end;
let A be Subset of G;

func gr A -> strict Subgroup of G means :Def4: :: GROUP_4:def 4

( 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 ( 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 ) );

ex b

( A c= the carrier of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines gr GROUP_4:def 4 :

for G being Group

for A being Subset of G

for b_{3} being strict Subgroup of G holds

( b_{3} = gr A iff ( A c= the carrier of b_{3} & ( for H being strict Subgroup of G st A c= the carrier of H holds

b_{3} is Subgroup of H ) ) );

for G being Group

for A being Subset of G

for b

( b

b

theorem Th28: :: GROUP_4:28

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 ) )

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 Th34: :: GROUP_4:34

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 ) }

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;

:: deftheorem defines generating GROUP_4:def 5 :

for G being Group

for a being Element of G holds

( a is generating iff ex A being Subset of G st

( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ) );

for G being Group

for a being Element of G holds

( a is generating iff ex A being Subset of G st

( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ) );

definition

let G be Group;

let H be Subgroup of G;

end;
let H be Subgroup of G;

attr H is maximal means :: GROUP_4:def 6

( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds

K = multMagma(# the carrier of G, the multF of G #) ) );

( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds

K = multMagma(# the carrier of G, the multF of G #) ) );

:: deftheorem defines maximal GROUP_4:def 6 :

for G being Group

for H being Subgroup of G holds

( H is maximal iff ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds

K = multMagma(# the carrier of G, the multF of G #) ) ) );

for G being Group

for H being Subgroup of G holds

( H is maximal iff ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds

K = multMagma(# the carrier of G, the multF of G #) ) ) );

theorem Th37: :: GROUP_4:37

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

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;

( ( ex H being strict Subgroup of G st H is maximal implies ex b_{1} being strict Subgroup of G st the carrier of b_{1} = 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 b_{1} being strict Subgroup of G st b_{1} = multMagma(# the carrier of G, the multF of G #) ) )

for b_{1}, b_{2} being strict Subgroup of G holds

( ( ex H being strict Subgroup of G st H is maximal & the carrier of b_{1} = 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 b_{2} = 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 b_{1} = b_{2} ) & ( ( for H being strict Subgroup of G holds not H is maximal ) & b_{1} = multMagma(# the carrier of G, the multF of G #) & b_{2} = multMagma(# the carrier of G, the multF of G #) implies b_{1} = b_{2} ) )
by GROUP_2:59;

correctness

consistency

for b_{1} being strict Subgroup of G holds verum;

;

end;
func Phi G -> strict Subgroup of G means :Def7: :: GROUP_4:def 7

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 = multMagma(# the carrier of G, the multF of G #);

existence 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 = multMagma(# the carrier of G, the multF of G #);

( ( ex H being strict Subgroup of G st H is maximal implies ex b

( A = the carrier of H & H is maximal ) } ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b

proof end;

uniqueness for b

( ( ex H being strict Subgroup of G st H is maximal & the carrier of b

( A = the carrier of H & H is maximal ) } & the carrier of b

( A = the carrier of H & H is maximal ) } implies b

correctness

consistency

for b

;

:: deftheorem Def7 defines Phi GROUP_4:def 7 :

for G being Group

for b_{2} being strict Subgroup of G holds

( ( ex H being strict Subgroup of G st H is maximal implies ( b_{2} = Phi G iff the carrier of b_{2} = 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 ( b_{2} = Phi G iff b_{2} = multMagma(# the carrier of G, the multF of G #) ) ) );

for G being Group

for b

( ( ex H being strict Subgroup of G st H is maximal implies ( b

( A = the carrier of H & H is maximal ) } ) ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ( b

theorem Th38: :: GROUP_4:38

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 )

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:39

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

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 Th41: :: GROUP_4:41

for G being strict Group holds the carrier of (Phi G) = { a where a is Element of G : not a is generating }

proof end;

definition

let G be Group;

let H1, H2 be Subgroup of G;

correctness

coherence

(carr H1) * (carr H2) is Subset of G;

;

end;
let H1, H2 be Subgroup of G;

correctness

coherence

(carr H1) * (carr H2) is Subset of G;

;

:: deftheorem defines * GROUP_4:def 8 :

for G being Group

for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2);

for G being Group

for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2);

theorem :: GROUP_4:43

theorem :: GROUP_4:45

for G being Group

for a being Element of G

for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * H2)

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:46

for G being Group

for a being Element of G

for H1, H2 being Subgroup of G holds (H1 * H2) * a = H1 * (H2 * a)

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:47

for G being Group

for A being Subset of G

for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2)

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:48

for G being Group

for A being Subset of G

for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)

for A being Subset of G

for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)

proof end;

definition

let G be Group;

let H1, H2 be Subgroup of G;

correctness

coherence

gr ((carr H1) \/ (carr H2)) is strict Subgroup of G;

;

end;
let H1, H2 be Subgroup of G;

correctness

coherence

gr ((carr H1) \/ (carr H2)) is strict Subgroup of G;

;

:: deftheorem defines "\/" GROUP_4:def 9 :

for G being Group

for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2));

for G being Group

for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2));

theorem :: GROUP_4:49

theorem Th51: :: GROUP_4:51

for G being Group

for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds

the carrier of (H1 "\/" H2) = H1 * H2

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:52

for G being Group

for H1, H2 being Subgroup of G st G is commutative Group holds

the carrier of (H1 "\/" H2) = H1 * H2

for H1, H2 being Subgroup of G st G is commutative Group holds

the carrier of (H1 "\/" H2) = H1 * H2

proof end;

theorem Th53: :: GROUP_4:53

for G being Group

for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2

for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2

proof end;

theorem :: GROUP_4:54

for G being Group

for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G

for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G

proof end;

theorem :: GROUP_4:55

theorem :: GROUP_4:56

Lm4: for G being Group

for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2

proof end;

Lm5: 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 Th57: :: GROUP_4:57

for G being Group

for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3)

for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3)

proof end;

theorem :: GROUP_4:58

for G being Group

for H being strict Subgroup of G holds

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

for H being strict Subgroup of G holds

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

proof end;

theorem Th59: :: GROUP_4:59

for G being Group

for H being Subgroup of G holds

( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )

for H being Subgroup of G holds

( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )

proof end;

theorem Th60: :: GROUP_4:60

for G being Group

for H1, H2 being Subgroup of G holds

( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )

for H1, H2 being Subgroup of G holds

( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )

proof end;

theorem Th61: :: GROUP_4:61

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 )

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:62

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

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:63

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

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:64

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

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 Th66: :: GROUP_4:66

for G being Group

for H1 being Subgroup of G

for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2

for H1 being Subgroup of G

for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2

proof end;

theorem Th67: :: GROUP_4:67

for G being Group

for H2 being Subgroup of G

for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1

for H2 being Subgroup of G

for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1

proof end;

definition

let G be Group;

ex b_{1} being BinOp of (Subgroups G) st

for H1, H2 being strict Subgroup of G holds b_{1} . (H1,H2) = H1 "\/" H2

for b_{1}, b_{2} being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b_{1} . (H1,H2) = H1 "\/" H2 ) & ( for H1, H2 being strict Subgroup of G holds b_{2} . (H1,H2) = H1 "\/" H2 ) holds

b_{1} = b_{2}

end;
func SubJoin G -> BinOp of (Subgroups G) means :Def10: :: GROUP_4:def 10

for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 "\/" H2;

existence for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 "\/" H2;

ex b

for H1, H2 being strict Subgroup of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines SubJoin GROUP_4:def 10 :

for G being Group

for b_{2} being BinOp of (Subgroups G) holds

( b_{2} = SubJoin G iff for H1, H2 being strict Subgroup of G holds b_{2} . (H1,H2) = H1 "\/" H2 );

for G being Group

for b

( b

definition

let G be Group;

ex b_{1} being BinOp of (Subgroups G) st

for H1, H2 being strict Subgroup of G holds b_{1} . (H1,H2) = H1 /\ H2

for b_{1}, b_{2} being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b_{1} . (H1,H2) = H1 /\ H2 ) & ( for H1, H2 being strict Subgroup of G holds b_{2} . (H1,H2) = H1 /\ H2 ) holds

b_{1} = b_{2}

end;
func SubMeet G -> BinOp of (Subgroups G) means :Def11: :: GROUP_4:def 11

for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 /\ H2;

existence for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 /\ H2;

ex b

for H1, H2 being strict Subgroup of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines SubMeet GROUP_4:def 11 :

for G being Group

for b_{2} being BinOp of (Subgroups G) holds

( b_{2} = SubMeet G iff for H1, H2 being strict Subgroup of G holds b_{2} . (H1,H2) = H1 /\ H2 );

for G being Group

for b

( b

Lm6: 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;

LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is strict Lattice by Lm6;

end;
func lattice G -> strict Lattice equals :: GROUP_4:def 12

LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);

coherence LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);

LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is strict Lattice by Lm6;

:: deftheorem defines lattice GROUP_4:def 12 :

for G being Group holds lattice G = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);

for G being Group holds lattice G = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);

registration
end;

:: Frattini subgroup.

::