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

theorem Th1: :: GROUP_3:1  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 Element of G holds
( (a * b) * (b " ) = a & (a * (b " )) * b = a & ((b " ) * b) * a = a & (b * (b " )) * a = a & a * (b * (b " )) = a & a * ((b " ) * b) = a & (b " ) * (b * a) = a & b * ((b " ) * a) = a )
proof end;

Lm1: for A being commutative Group
for a, b being Element of A holds a * b = b * a
;

theorem :: GROUP_3:2  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
( G is commutative Group iff the mult of G is commutative )
proof end;

theorem :: GROUP_3:3  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 (1). G is commutative
proof end;

theorem Th4: :: GROUP_3:4  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, D being Subset of G st A c= B & C c= D holds
A * C c= B * D
proof end;

theorem Th5: :: GROUP_3:5  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, B being Subset of G st A c= B holds
( a * A c= a * B & A * a c= B * a ) by Th4;

theorem Th6: :: GROUP_3:6  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 st H1 is Subgroup of H2 holds
( a * H1 c= a * H2 & H1 * a c= H2 * a )
proof end;

theorem :: GROUP_3:7  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 H being Subgroup of G holds a * H = {a} * H ;

theorem :: GROUP_3:8  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 H being Subgroup of G holds H * a = H * {a} ;

theorem :: GROUP_3:9  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
for H being Subgroup of G holds (a * A) * H = a * (A * H) by GROUP_2:116;

theorem Th10: :: GROUP_3:10  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
for H being Subgroup of G holds (A * a) * H = A * (a * H)
proof end;

theorem :: GROUP_3:11  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
for H being Subgroup of G holds (a * H) * A = a * (H * A)
proof end;

theorem :: GROUP_3:12  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
for H being Subgroup of G holds (A * H) * a = A * (H * a)
proof end;

theorem :: GROUP_3:13  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
for H being Subgroup of G holds (H * a) * A = H * (a * A)
proof end;

theorem :: GROUP_3: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 being Element of G
for A being Subset of G
for H being Subgroup of G holds (H * A) * a = H * (A * a) by GROUP_2:118;

theorem :: GROUP_3:15  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 * a) * H2 = H1 * (a * H2) by Th10;

definition
let G be Group;
func Subgroups G -> set means :Def1: :: GROUP_3:def 1
for x being set holds
( x in it iff x is strict Subgroup of G );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subgroup of G )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Subgroup of G ) ) & ( for x being set holds
( x in b2 iff x is strict Subgroup of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :
for G being Group
for b2 being set holds
( b2 = Subgroups G iff for x being set holds
( x in b2 iff x is strict Subgroup of G ) );

registration
let G be Group;
cluster Subgroups G -> non empty ;
coherence
not Subgroups G is empty
proof end;
end;

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

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

theorem :: GROUP_3:18  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 G in Subgroups G
proof end;

theorem Th19: :: GROUP_3: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 st G is finite holds
Subgroups G is finite
proof end;

definition
let G be Group;
let a, b be Element of G;
func a |^ b -> Element of G equals :: GROUP_3:def 2
((b " ) * a) * b;
correctness
coherence
((b " ) * a) * b is Element of G
;
;
end;

:: deftheorem defines |^ GROUP_3:def 2 :
for G being Group
for a, b being Element of G holds a |^ b = ((b " ) * a) * b;

theorem Th20: :: GROUP_3: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 a, b being Element of G holds
( a |^ b = ((b " ) * a) * b & a |^ b = (b " ) * (a * b) ) by GROUP_1:def 4;

theorem Th21: :: GROUP_3: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 a, g, b being Element of G st a |^ g = b |^ g holds
a = b
proof end;

theorem Th22: :: GROUP_3:22  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 holds (1. G) |^ a = 1. G
proof end;

theorem Th23: :: GROUP_3:23  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 Element of G st a |^ b = 1. G holds
a = 1. G
proof end;

theorem Th24: :: GROUP_3:24  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 holds a |^ (1. G) = a
proof end;

theorem Th25: :: GROUP_3: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 a being Element of G holds a |^ a = a
proof end;

theorem Th26: :: GROUP_3: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 a being Element of G holds
( a |^ (a " ) = a & (a " ) |^ a = a " )
proof end;

theorem Th27: :: GROUP_3: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
for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )
proof end;

theorem Th28: :: GROUP_3:28  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, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)
proof end;

theorem Th29: :: GROUP_3:29  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, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h)
proof end;

theorem Th30: :: GROUP_3:30  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 Element of G holds
( (a |^ b) |^ (b " ) = a & (a |^ (b " )) |^ b = a )
proof end;

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

theorem Th32: :: GROUP_3: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 a, b being Element of G holds (a " ) |^ b = (a |^ b) "
proof end;

Lm2: now
let G be Group; :: thesis: for a, b being Element of G holds (a |^ 0) |^ b = (a |^ b) |^ 0
let a, b be Element of G;
thus (a |^ 0) |^ b = (1. G) |^ b by GROUP_1:43
.= 1. G by Th22
.= (a |^ b) |^ 0 by GROUP_1:43 ; :: thesis: verum
end;

Lm3: now
let n be Nat; :: thesis: ( ( for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ) implies for G being Group
for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1) )

assume A1: for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; :: thesis: for G being Group
for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)

let G be Group; :: thesis: for a, b being Element of G holds (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)
let a, b be Element of G;
thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:49
.= ((a |^ n) |^ b) * (a |^ b) by Th28
.= ((a |^ b) |^ n) * (a |^ b) by A1
.= (a |^ b) |^ (n + 1) by GROUP_1:49 ; :: thesis: verum
end;

Lm4: for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n
proof end;

theorem :: GROUP_3:33  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 Element of G
for n being Nat holds (a |^ n) |^ b = (a |^ b) |^ n by Lm4;

theorem :: GROUP_3:34  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 Element of G
for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
proof end;

theorem Th35: :: GROUP_3:35  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 Element of G st G is commutative Group holds
a |^ b = a
proof end;

theorem Th36: :: GROUP_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group st ( for a, b being Element of G holds a |^ b = a ) holds
G is commutative
proof end;

definition
let G be Group;
let A, B be Subset of G;
func A |^ B -> Subset of G equals :: GROUP_3:def 3
{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;
coherence
{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G
proof end;
end;

:: deftheorem defines |^ GROUP_3:def 3 :
for G being Group
for A, B being Subset of G holds A |^ B = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;

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

theorem Th38: :: GROUP_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for A, B being Subset of G holds
( x in A |^ B iff ex g, h being Element of G st
( x = g |^ h & g in A & h in B ) ) ;

theorem Th39: :: GROUP_3: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
for A, B being Subset of G holds
( A |^ B <> {} iff ( A <> {} & B <> {} ) )
proof end;

theorem Th40: :: GROUP_3: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 A, B being Subset of G holds A |^ B c= ((B " ) * A) * B
proof end;

theorem Th41: :: GROUP_3: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, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C)
proof end;

theorem Th42: :: GROUP_3: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, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C)
proof end;

theorem :: GROUP_3: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, B being Subset of G holds (A " ) |^ B = (A |^ B) "
proof end;

theorem Th44: :: GROUP_3: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, b being Element of G holds {a} |^ {b} = {(a |^ b)}
proof end;

theorem :: GROUP_3:45  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 {a} |^ {b,c} = {(a |^ b),(a |^ c)}
proof end;

theorem :: GROUP_3: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
for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)}
proof end;

theorem :: GROUP_3:47  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, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
proof end;

definition
let G be Group;
let A be Subset of G;
let g be Element of G;
func A |^ g -> Subset of G equals :: GROUP_3:def 4
A |^ {g};
correctness
coherence
A |^ {g} is Subset of G
;
;
func g |^ A -> Subset of G equals :: GROUP_3:def 5
{g} |^ A;
correctness
coherence
{g} |^ A is Subset of G
;
;
end;

:: deftheorem defines |^ GROUP_3:def 4 :
for G being Group
for A being Subset of G
for g being Element of G holds A |^ g = A |^ {g};

:: deftheorem defines |^ GROUP_3:def 5 :
for G being Group
for A being Subset of G
for g being Element of G holds g |^ A = {g} |^ A;

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

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

theorem Th50: :: GROUP_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for g being Element of G
for A being Subset of G holds
( x in A |^ g iff ex h being Element of G st
( x = h |^ g & h in A ) )
proof end;

theorem Th51: :: GROUP_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for g being Element of G
for A being Subset of G holds
( x in g |^ A iff ex h being Element of G st
( x = g |^ h & h in A ) )
proof end;

theorem :: GROUP_3: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 g being Element of G
for A being Subset of G holds g |^ A c= ((A " ) * g) * A
proof end;

theorem Th53: :: GROUP_3: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 g being Element of G
for A, B being Subset of G holds (A |^ B) |^ g = A |^ (B * g) by Th42;

theorem Th54: :: GROUP_3: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 g being Element of G
for A, B being Subset of G holds (A |^ g) |^ B = A |^ (g * B) by Th42;

theorem :: GROUP_3:55  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 g being Element of G
for A, B being Subset of G holds (g |^ A) |^ B = g |^ (A * B) by Th42;

theorem Th56: :: GROUP_3:56  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 Element of G
for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
proof end;

theorem :: GROUP_3: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 a, b being Element of G
for A being Subset of G holds (a |^ A) |^ b = a |^ (A * b) by Th53;

theorem :: GROUP_3: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 a, b being Element of G
for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)
proof end;

theorem Th59: :: GROUP_3: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 g being Element of G
for A being Subset of G holds A |^ g = ((g " ) * A) * g
proof end;

theorem :: GROUP_3: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 A, B being Subset of G holds (A * B) |^ a c= (A |^ a) * (B |^ a) by Th41;

theorem Th61: :: GROUP_3: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 Subset of G holds A |^ (1. G) = A
proof end;

theorem :: GROUP_3: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 st A <> {} holds
(1. G) |^ A = {(1. G)}
proof end;

theorem Th63: :: GROUP_3: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 Element of G
for A being Subset of G holds
( (A |^ a) |^ (a " ) = A & (A |^ (a " )) |^ a = A )
proof end;

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

theorem Th65: :: GROUP_3: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 holds
( G is commutative Group iff for A, B being Subset of G st B <> {} holds
A |^ B = A )
proof end;

theorem :: GROUP_3:66  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
( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )
proof end;

theorem :: GROUP_3: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 holds
( G is commutative Group iff for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} )
proof end;

definition
let G be Group;
let H be Subgroup of G;
let a be Element of G;
func H |^ a -> strict Subgroup of G means :Def6: :: GROUP_3:def 6
the carrier of it = (carr H) |^ a;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a
proof end;
correctness
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a & the carrier of b2 = (carr H) |^ a holds
b1 = b2
;
by GROUP_2:68;
end;

:: deftheorem Def6 defines |^ GROUP_3:def 6 :
for G being Group
for H being Subgroup of G
for a being Element of G
for b4 being strict Subgroup of G holds
( b4 = H |^ a iff the carrier of b4 = (carr H) |^ a );

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

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

theorem Th70: :: GROUP_3:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in H |^ a iff ex g being Element of G st
( x = g |^ a & g in H ) )
proof end;

theorem Th71: :: GROUP_3: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 a being Element of G
for H being Subgroup of G holds the carrier of (H |^ a) = ((a " ) * H) * a
proof end;

theorem Th72: :: GROUP_3: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 a, b being Element of G
for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
proof end;

theorem Th73: :: GROUP_3: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 |^ (1. G) = H
proof end;

theorem Th74: :: GROUP_3: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 a being Element of G
for H being strict Subgroup of G holds
( (H |^ a) |^ (a " ) = H & (H |^ (a " )) |^ a = H )
proof end;

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

theorem Th76: :: GROUP_3: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 a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
proof end;

theorem Th77: :: GROUP_3: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 a being Element of G
for H being Subgroup of G holds Ord H = Ord (H |^ a)
proof end;

theorem Th78: :: GROUP_3: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 a being Element of G
for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
proof end;

theorem Th79: :: GROUP_3: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 a being Element of G
for H being Subgroup of G st H is finite holds
ord H = ord (H |^ a)
proof end;

theorem Th80: :: GROUP_3: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 a being Element of G holds ((1). G) |^ a = (1). G
proof end;

theorem :: GROUP_3: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 a being Element of G
for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
proof end;

theorem Th82: :: GROUP_3: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 a being Element of G holds ((Omega). G) |^ a = (Omega). G
proof end;

theorem :: GROUP_3: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 a being Element of G
for H being strict Subgroup of G st H |^ a = G holds
H = G
proof end;

theorem Th84: :: GROUP_3: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 a being Element of G
for H being Subgroup of G holds Index H = Index (H |^ a)
proof end;

theorem :: GROUP_3: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 a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
proof end;

theorem Th86: :: GROUP_3: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 st G is commutative Group holds
for H being strict Subgroup of G
for a being Element of G holds H |^ a = H
proof end;

definition
let G be Group;
let a, b be Element of G;
pred a,b are_conjugated means :Def7: :: GROUP_3:def 7
ex g being Element of G st a = b |^ g;
end;

:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :
for G being Group
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st a = b |^ g );

notation
let G be Group;
let a, b be Element of G;
antonym a,b are_not_conjugated for a,b are_conjugated ;
end;

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

theorem Th88: :: GROUP_3:88  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 Element of G holds
( a,b are_conjugated iff ex g being Element of G st b = a |^ g )
proof end;

theorem Th89: :: GROUP_3:89  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 holds a,a are_conjugated
proof end;

theorem Th90: :: GROUP_3:90  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 Element of G st a,b are_conjugated holds
b,a are_conjugated
proof end;

definition
let G be Group;
let a, b be Element of G;
:: original: are_conjugated
redefine pred a,b are_conjugated ;
reflexivity
for a being Element of G holds a,a are_conjugated
by Th89;
symmetry
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
by Th90;
end;

theorem Th91: :: GROUP_3:91  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 st a,b are_conjugated & b,c are_conjugated holds
a,c are_conjugated
proof end;

theorem Th92: :: GROUP_3: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
for a being Element of G st ( a, 1. G are_conjugated or 1. G,a are_conjugated ) holds
a = 1. G
proof end;

theorem Th93: :: GROUP_3: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
for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
proof end;

definition
let G be Group;
let a be Element of G;
func con_class a -> Subset of G equals :: GROUP_3:def 8
a |^ (carr ((Omega). G));
correctness
coherence
a |^ (carr ((Omega). G)) is Subset of G
;
;
end;

:: deftheorem defines con_class GROUP_3:def 8 :
for G being Group
for a being Element of G holds con_class a = a |^ (carr ((Omega). G));

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

theorem Th95: :: GROUP_3:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
proof end;

theorem Th96: :: GROUP_3:96  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 Element of G holds
( a in con_class b iff a,b are_conjugated )
proof end;

theorem Th97: :: GROUP_3:97  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, g being Element of G holds a |^ g in con_class a
proof end;

theorem :: GROUP_3: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
for a being Element of G holds a in con_class a by Th96;

theorem :: GROUP_3: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
for a, b being Element of G st a in con_class b holds
b in con_class a
proof end;

theorem :: GROUP_3:100  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 Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
proof end;

theorem :: GROUP_3:101  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 holds
( con_class a = {(1. G)} iff a = 1. G )
proof end;

theorem :: GROUP_3:102  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 (con_class a) * A = A * (con_class a)
proof end;

definition
let G be Group;
let A, B be Subset of G;
pred A,B are_conjugated means :Def9: :: GROUP_3:def 9
ex g being Element of G st A = B |^ g;
end;

:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :
for G being Group
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st A = B |^ g );

notation
let G be Group;
let A, B be Subset of G;
antonym A,B are_not_conjugated for A,B are_conjugated ;
end;

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

theorem Th104: :: GROUP_3:104  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
( A,B are_conjugated iff ex g being Element of G st B = A |^ g )
proof end;

theorem Th105: :: GROUP_3:105  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 A,A are_conjugated
proof end;

theorem Th106: :: GROUP_3:106  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,B are_conjugated holds
B,A are_conjugated
proof end;

definition
let G be Group;
let A, B be Subset of G;
:: original: are_conjugated
redefine pred A,B are_conjugated ;
reflexivity
for A being Subset of G holds A,A are_conjugated
by Th105;
symmetry
for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
by Th106;
end;

theorem Th107: :: GROUP_3:107  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 Subset of G st A,B are_conjugated & B,C are_conjugated holds
A,C are_conjugated
proof end;

theorem Th108: :: GROUP_3:108  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 Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
proof end;

theorem Th109: :: GROUP_3:109  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 being Subgroup of G st A, carr H1 are_conjugated holds
ex H2 being strict Subgroup of G st the carrier of H2 = A
proof end;

definition
let G be Group;
let A be Subset of G;
func con_class A -> Subset-Family of G equals :: GROUP_3:def 10
{ B where B is Subset of G : A,B are_conjugated } ;
coherence
{ B where B is Subset of G : A,B are_conjugated } is Subset-Family of G
proof end;
end;

:: deftheorem defines con_class GROUP_3:def 10 :
for G being Group
for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;

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

theorem :: GROUP_3:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for A being Subset of G holds
( x in con_class A iff ex B being Subset of G st
( x = B & A,B are_conjugated ) ) ;

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

theorem Th113: :: GROUP_3:113  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
( A in con_class B iff A,B are_conjugated )
proof end;

theorem :: GROUP_3:114  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 g being Element of G
for A being Subset of G holds A |^ g in con_class A
proof end;

theorem :: GROUP_3:115  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 A in con_class A ;

theorem :: GROUP_3:116  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 in con_class B holds
B in con_class A
proof end;

theorem :: GROUP_3:117  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
( con_class A = con_class B iff con_class A meets con_class B )
proof end;

theorem Th118: :: GROUP_3:118  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 holds con_class {a} = { {b} where b is Element of G : b in con_class a }
proof end;

theorem :: GROUP_3:119  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 st G is finite holds
con_class A is finite
proof end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
pred H1,H2 are_conjugated means :Def11: :: GROUP_3:def 11
ex g being Element of G st HGrStr(# the carrier of H1,the mult of H1 #) = H2 |^ g;
end;

:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :
for G being Group
for H1, H2 being Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st HGrStr(# the carrier of H1,the mult of H1 #) = H2 |^ g );

notation
let G be Group;
let H1, H2 be Subgroup of G;
antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated ;
end;

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

theorem Th121: :: GROUP_3:121  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 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
proof end;

theorem Th122: :: GROUP_3:122  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 strict Subgroup of G holds H1,H1 are_conjugated
proof end;

theorem Th123: :: GROUP_3:123  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 st H1,H2 are_conjugated holds
H2,H1 are_conjugated
proof end;

definition
let G be Group;
let H1, H2 be strict Subgroup of G;
:: original: are_conjugated
redefine pred H1,H2 are_conjugated ;
reflexivity
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
by Th122;
symmetry
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
by Th123;
end;

theorem Th124: :: GROUP_3:124  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 H3 being Subgroup of G
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
proof end;

definition
let G be Group;
let H be Subgroup of G;
func con_class H -> Subset of (Subgroups G) means :Def12: :: GROUP_3:def 12
for x being set holds
( x in it iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) );
existence
ex b1 being Subset of (Subgroups G) st
for x being set holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
proof end;
uniqueness
for b1, b2 being Subset of (Subgroups G) st ( for x being set holds
( x in b1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds
( x in b2 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines con_class GROUP_3:def 12 :
for G being Group
for H being Subgroup of G
for b3 being Subset of (Subgroups G) holds
( b3 = con_class H iff for x being set holds
( x in b3 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) );

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

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

theorem Th127: :: GROUP_3:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
proof end;

theorem Th128: :: GROUP_3:128  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 in con_class H2 iff H1,H2 are_conjugated )
proof end;

theorem Th129: :: GROUP_3:129  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 g being Element of G
for H being strict Subgroup of G holds H |^ g in con_class H
proof end;

theorem Th130: :: GROUP_3:130  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 in con_class H
proof end;

theorem :: GROUP_3:131  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 st H1 in con_class H2 holds
H2 in con_class H1
proof end;

theorem :: GROUP_3:132  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
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
proof end;

theorem :: GROUP_3:133  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 st G is finite holds
con_class H is finite
proof end;

theorem Th134: :: GROUP_3:134  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,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
proof end;

definition
let G be Group;
let IT be Subgroup of G;
attr IT is normal means :Def13: :: GROUP_3:def 13
for a being Element of G holds IT |^ a = HGrStr(# the carrier of IT,the mult of IT #);
end;

:: deftheorem Def13 defines normal GROUP_3:def 13 :
for G being Group
for IT being Subgroup of G holds
( IT is normal iff for a being Element of G holds IT |^ a = HGrStr(# the carrier of IT,the mult of IT #) );

registration
let G be Group;
cluster strict normal Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is normal )
proof end;
end;

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

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

theorem Th137: :: GROUP_3:137  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
( (1). G is normal & (Omega). G is normal )
proof end;

theorem :: GROUP_3:138  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
proof end;

theorem :: GROUP_3:139  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 G is commutative Group holds
H is normal
proof end;

theorem Th140: :: GROUP_3:140  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 is normal Subgroup of G iff for a being Element of G holds a * H = H * a )
proof end;

theorem Th141: :: GROUP_3:141  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 is normal Subgroup of G iff for a being Element of G holds a * H c= H * a )
proof end;

theorem Th142: :: GROUP_3:142  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 is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
proof end;

theorem :: GROUP_3:143  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 is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )
proof end;

theorem :: GROUP_3:144  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 is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )
proof end;

theorem :: GROUP_3:145  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 is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H )
proof end;

theorem :: GROUP_3:146  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 is normal Subgroup of G iff con_class H = {H} )
proof end;

theorem :: GROUP_3:147  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 is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
proof end;

Lm5: for G being Group
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)
proof end;

theorem Th148: :: GROUP_3:148  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 (carr N1) * (carr N2) = (carr N2) * (carr N1)
proof end;

theorem :: GROUP_3:149  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 ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)
proof end;

theorem :: GROUP_3:150  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 N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
proof end;

theorem :: GROUP_3:151  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 st Left_Cosets H is finite & index H = 2 holds
H is normal Subgroup of G
proof end;

definition
let G be Group;
let A be Subset of G;
func Normalizator A -> strict Subgroup of G means :Def14: :: GROUP_3:def 14
the carrier of it = { h where h is Element of G : A |^ h = A } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } & the carrier of b2 = { h where h is Element of G : A |^ h = A } holds
b1 = b2
by GROUP_2:68;
end;

:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :
for G being Group
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = Normalizator A iff the carrier of b3 = { h where h is Element of G : A |^ h = A } );

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

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

theorem Th154: :: GROUP_3:154  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for A being Subset of G holds
( x in Normalizator A iff ex h being Element of G st
( x = h & A |^ h = A ) )
proof end;

theorem Th155: :: GROUP_3:155  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 Card (con_class A) = Index (Normalizator A)
proof end;

theorem :: GROUP_3:156  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 st ( con_class A is finite or Left_Cosets (Normalizator A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizator A) )
proof end;

theorem Th157: :: GROUP_3:157  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 holds Card (con_class a) = Index (Normalizator {a})
proof end;

theorem :: GROUP_3:158  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 ( con_class a is finite or Left_Cosets (Normalizator {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizator {a}) )
proof end;

definition
let G be Group;
let H be Subgroup of G;
func Normalizator H -> strict Subgroup of G equals :: GROUP_3:def 15
Normalizator (carr H);
correctness
coherence
Normalizator (carr H) is strict Subgroup of G
;
;
end;

:: deftheorem defines Normalizator GROUP_3:def 15 :
for G being Group
for H being Subgroup of G holds Normalizator H = Normalizator (carr H);

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

theorem Th160: :: GROUP_3:160  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Group
for H being strict Subgroup of G holds
( x in Normalizator H iff ex h being Element of G st
( x = h & H |^ h = H ) )
proof end;

theorem Th161: :: GROUP_3:161  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 Card (con_class H) = Index (Normalizator H)
proof end;

theorem :: GROUP_3:162  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 ( con_class H is finite or Left_Cosets (Normalizator H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizator H) )
proof end;

theorem Th163: :: GROUP_3:163  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 holds
( H is normal Subgroup of G iff Normalizator H = G )
proof end;

theorem :: GROUP_3:164  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 Normalizator ((1). G) = G
proof end;

theorem :: GROUP_3:165  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 Normalizator ((Omega). G) = G
proof end;