:: GROUP_3 semantic presentation
begin
theorem Th1: :: GROUP_3:1
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
let G be Group; ::_thesis: 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 )
let a, b be Element of G; ::_thesis: ( (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 )
thus A1: (a * b) * (b ") = a * (b * (b ")) by GROUP_1:def_3
.= a * (1_ G) by GROUP_1:def_5
.= a by GROUP_1:def_4 ; ::_thesis: ( (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 )
thus A2: (a * (b ")) * b = a * ((b ") * b) by GROUP_1:def_3
.= a * (1_ G) by GROUP_1:def_5
.= a by GROUP_1:def_4 ; ::_thesis: ( ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus A3: ((b ") * b) * a = (1_ G) * a by GROUP_1:def_5
.= a by GROUP_1:def_4 ; ::_thesis: ( (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus (b * (b ")) * a = (1_ G) * a by GROUP_1:def_5
.= a by GROUP_1:def_4 ; ::_thesis: ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
hence ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) by A1, A2, A3, GROUP_1:def_3; ::_thesis: verum
end;
Lm1: for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
theorem :: GROUP_3:2
for G being Group holds
( G is commutative Group iff the multF of G is commutative )
proof
let G be Group; ::_thesis: ( G is commutative Group iff the multF of G is commutative )
thus ( G is commutative Group implies the multF of G is commutative ) ::_thesis: ( the multF of G is commutative implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: the multF of G is commutative
let a be Element of G; :: according to BINOP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds the multF of G . (a,b1) = the multF of G . (b1,a)
let b be Element of G; ::_thesis: the multF of G . (a,b) = the multF of G . (b,a)
thus the multF of G . (a,b) = a * b
.= b * a by A1, Lm1
.= the multF of G . (b,a) ; ::_thesis: verum
end;
assume A2: the multF of G is commutative ; ::_thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
thus a * b = b * a by A2, BINOP_1:def_2; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
theorem :: GROUP_3:3
for G being Group holds (1). G is commutative
proof
let G be Group; ::_thesis: (1). G is commutative
let a, b be Element of ((1). G); :: according to GROUP_1:def_12 ::_thesis: a * b = b * a
a in the carrier of ((1). G) ;
then a in {(1_ G)} by GROUP_2:def_7;
then A1: a = 1_ G by TARSKI:def_1;
b in the carrier of ((1). G) ;
then b in {(1_ G)} by GROUP_2:def_7;
hence a * b = b * a by A1, TARSKI:def_1; ::_thesis: verum
end;
theorem Th4: :: GROUP_3:4
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
let G be Group; ::_thesis: for A, B, C, D being Subset of G st A c= B & C c= D holds
A * C c= B * D
let A, B, C, D be Subset of G; ::_thesis: ( A c= B & C c= D implies A * C c= B * D )
assume A1: ( A c= B & C c= D ) ; ::_thesis: A * C c= B * D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * C or x in B * D )
assume x in A * C ; ::_thesis: x in B * D
then ex a, c being Element of G st
( x = a * c & a in A & c in C ) ;
hence x in B * D by A1; ::_thesis: verum
end;
theorem :: GROUP_3:5
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
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
let G be Group; ::_thesis: 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 )
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G st H1 is Subgroup of H2 holds
( a * H1 c= a * H2 & H1 * a c= H2 * a )
let H1, H2 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies ( a * H1 c= a * H2 & H1 * a c= H2 * a ) )
assume H1 is Subgroup of H2 ; ::_thesis: ( a * H1 c= a * H2 & H1 * a c= H2 * a )
then the carrier of H1 c= the carrier of H2 by GROUP_2:def_5;
hence ( a * H1 c= a * H2 & H1 * a c= H2 * a ) by Th4; ::_thesis: verum
end;
theorem :: GROUP_3:7
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
for G being Group
for a being Element of G
for H being Subgroup of G holds H * a = H * {a} ;
theorem Th9: :: GROUP_3:9
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
let G be Group; ::_thesis: 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)
let a be Element of G; ::_thesis: for A being Subset of G
for H being Subgroup of G holds (A * a) * H = A * (a * H)
let A be Subset of G; ::_thesis: for H being Subgroup of G holds (A * a) * H = A * (a * H)
let H be Subgroup of G; ::_thesis: (A * a) * H = A * (a * H)
thus (A * a) * H = A * ({a} * H) by GROUP_2:96
.= A * (a * H) ; ::_thesis: verum
end;
theorem :: GROUP_3:10
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
let G be Group; ::_thesis: 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)
let a be Element of G; ::_thesis: for A being Subset of G
for H being Subgroup of G holds (a * H) * A = a * (H * A)
let A be Subset of G; ::_thesis: for H being Subgroup of G holds (a * H) * A = a * (H * A)
let H be Subgroup of G; ::_thesis: (a * H) * A = a * (H * A)
thus (a * H) * A = ({a} * H) * A
.= a * (H * A) by GROUP_2:97 ; ::_thesis: verum
end;
theorem :: GROUP_3:11
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
let G be Group; ::_thesis: 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)
let a be Element of G; ::_thesis: for A being Subset of G
for H being Subgroup of G holds (A * H) * a = A * (H * a)
let A be Subset of G; ::_thesis: for H being Subgroup of G holds (A * H) * a = A * (H * a)
let H be Subgroup of G; ::_thesis: (A * H) * a = A * (H * a)
thus (A * H) * a = A * (H * {a}) by GROUP_2:97
.= A * (H * a) ; ::_thesis: verum
end;
theorem :: GROUP_3:12
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
let G be Group; ::_thesis: 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)
let a be Element of G; ::_thesis: for A being Subset of G
for H being Subgroup of G holds (H * a) * A = H * (a * A)
let A be Subset of G; ::_thesis: for H being Subgroup of G holds (H * a) * A = H * (a * A)
let H be Subgroup of G; ::_thesis: (H * a) * A = H * (a * A)
thus (H * a) * A = (H * {a}) * A
.= H * (a * A) by GROUP_2:98 ; ::_thesis: verum
end;
theorem :: GROUP_3:13
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 Th9;
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
defpred S1[ set , set ] means ex H being strict Subgroup of G st
( $2 = H & $1 = the carrier of H );
defpred S2[ set ] means ex H being strict Subgroup of G st $1 = the carrier of H;
consider B being set such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of G & S2[x] ) ) from XBOOLE_0:sch_1();
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by GROUP_2:59;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
for x being set holds
( x in B iff ex y being set st [x,y] in f )
proof
let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f )
thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B )
proof
assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f
then consider H being strict Subgroup of G such that
A5: x = the carrier of H by A1;
reconsider y = H as set ;
take y ; ::_thesis: [x,y] in f
thus [x,y] in f by A3, A4, A5; ::_thesis: verum
end;
given y being set such that A6: [x,y] in f ; ::_thesis: x in B
thus x in B by A3, A6; ::_thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def_12;
for y being set holds
( y in rng f iff y is strict Subgroup of G )
proof
let y be set ; ::_thesis: ( y in rng f iff y is strict Subgroup of G )
thus ( y in rng f implies y is strict Subgroup of G ) ::_thesis: ( y is strict Subgroup of G implies y in rng f )
proof
assume y in rng f ; ::_thesis: y is strict Subgroup of G
then consider x being set such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
[x,y] in f by A8, FUNCT_1:def_2;
then ex H being strict Subgroup of G st
( y = H & x = the carrier of H ) by A3;
hence y is strict Subgroup of G ; ::_thesis: verum
end;
assume y is strict Subgroup of G ; ::_thesis: y in rng f
then reconsider H = y as strict Subgroup of G ;
reconsider x = the carrier of H as set ;
the carrier of H c= the carrier of G by GROUP_2:def_5;
then A9: x in dom f by A1, A7;
then [x,y] in f by A3, A7;
then y = f . x by A9, FUNCT_1:def_2;
hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum
end;
hence ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subgroup of G ) ; ::_thesis: verum
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
defpred S1[ set ] means $1 is strict Subgroup of G;
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff x is strict Subgroup of G ) ) & ( for x being set holds
( x in A2 iff x is strict Subgroup of G ) ) implies A1 = A2 )
assume A10: for x being set holds
( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st
( ( x in A2 implies x is strict Subgroup of G ) implies ( x is strict Subgroup of G & not x in A2 ) ) or A1 = A2 )
assume A11: for x being set holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
thus A1 = A2 from XBOOLE_0:sch_2(A10, A11); ::_thesis: verum
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
set x = the strict Subgroup of G;
the strict Subgroup of G in Subgroups G by Def1;
hence not Subgroups G is empty ; ::_thesis: verum
end;
end;
theorem :: GROUP_3:14
for G being strict Group holds G in Subgroups G
proof
let G be strict Group; ::_thesis: G in Subgroups G
G is Subgroup of G by GROUP_2:54;
hence G in Subgroups G by Def1; ::_thesis: verum
end;
theorem Th15: :: GROUP_3:15
for G being Group st G is finite holds
Subgroups G is finite
proof
let G be Group; ::_thesis: ( G is finite implies Subgroups G is finite )
defpred S1[ set , set ] means ex H being strict Subgroup of G st
( $1 = H & $2 = the carrier of H );
assume A1: G is finite ; ::_thesis: Subgroups G is finite
A2: for x being set st x in Subgroups G holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Subgroups G implies ex y being set st S1[x,y] )
assume x in Subgroups G ; ::_thesis: ex y being set st S1[x,y]
then reconsider F = x as strict Subgroup of G by Def1;
reconsider y = the carrier of F as set ;
take y ; ::_thesis: S1[x,y]
take F ; ::_thesis: ( x = F & y = the carrier of F )
thus ( x = F & y = the carrier of F ) ; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = Subgroups G and
A4: for x being set st x in Subgroups G holds
S1[x,f . x] from CLASSES1:sch_1(A2);
A5: rng f c= bool the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool the carrier of G )
assume x in rng f ; ::_thesis: x in bool the carrier of G
then consider y being set such that
A6: ( y in dom f & f . y = x ) by FUNCT_1:def_3;
consider H being strict Subgroup of G such that
y = H and
A7: x = the carrier of H by A3, A4, A6;
the carrier of H c= the carrier of G by GROUP_2:def_5;
hence x in bool the carrier of G by A7; ::_thesis: verum
end;
f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A8: ( x in dom f & y in dom f ) and
A9: f . x = f . y ; ::_thesis: x = y
( ex H1 being strict Subgroup of G st
( x = H1 & f . x = the carrier of H1 ) & ex H2 being strict Subgroup of G st
( y = H2 & f . y = the carrier of H2 ) ) by A3, A4, A8;
hence x = y by A9, GROUP_2:59; ::_thesis: verum
end;
then card (Subgroups G) c= card (bool the carrier of G) by A3, A5, CARD_1:10;
hence Subgroups G is finite by A1, CARD_2:49; ::_thesis: verum
end;
definition
let G be Group;
let a, b be Element of G;
funca |^ 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 Th16: :: GROUP_3:16
for G being Group
for a, g, b being Element of G st a |^ g = b |^ g holds
a = b
proof
let G be Group; ::_thesis: for a, g, b being Element of G st a |^ g = b |^ g holds
a = b
let a, g, b be Element of G; ::_thesis: ( a |^ g = b |^ g implies a = b )
assume a |^ g = b |^ g ; ::_thesis: a = b
then (g ") * a = (g ") * b by GROUP_1:6;
hence a = b by GROUP_1:6; ::_thesis: verum
end;
theorem Th17: :: GROUP_3:17
for G being Group
for a being Element of G holds (1_ G) |^ a = 1_ G
proof
let G be Group; ::_thesis: for a being Element of G holds (1_ G) |^ a = 1_ G
let a be Element of G; ::_thesis: (1_ G) |^ a = 1_ G
thus (1_ G) |^ a = (a ") * a by GROUP_1:def_4
.= 1_ G by GROUP_1:def_5 ; ::_thesis: verum
end;
theorem Th18: :: GROUP_3:18
for G being Group
for a, b being Element of G st a |^ b = 1_ G holds
a = 1_ G
proof
let G be Group; ::_thesis: for a, b being Element of G st a |^ b = 1_ G holds
a = 1_ G
let a, b be Element of G; ::_thesis: ( a |^ b = 1_ G implies a = 1_ G )
assume a |^ b = 1_ G ; ::_thesis: a = 1_ G
then b " = (b ") * a by GROUP_1:12;
hence a = 1_ G by GROUP_1:7; ::_thesis: verum
end;
theorem Th19: :: GROUP_3:19
for G being Group
for a being Element of G holds a |^ (1_ G) = a
proof
let G be Group; ::_thesis: for a being Element of G holds a |^ (1_ G) = a
let a be Element of G; ::_thesis: a |^ (1_ G) = a
thus a |^ (1_ G) = ((1_ G) ") * a by GROUP_1:def_4
.= (1_ G) * a by GROUP_1:8
.= a by GROUP_1:def_4 ; ::_thesis: verum
end;
theorem Th20: :: GROUP_3:20
for G being Group
for a being Element of G holds a |^ a = a
proof
let G be Group; ::_thesis: for a being Element of G holds a |^ a = a
let a be Element of G; ::_thesis: a |^ a = a
thus a |^ a = (1_ G) * a by GROUP_1:def_5
.= a by GROUP_1:def_4 ; ::_thesis: verum
end;
theorem :: GROUP_3:21
for G being Group
for a being Element of G holds
( a |^ (a ") = a & (a ") |^ a = a " ) by Th1;
theorem Th22: :: GROUP_3:22
for G being Group
for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )
let a, b be Element of G; ::_thesis: ( a |^ b = a iff a * b = b * a )
thus ( a |^ b = a implies a * b = b * a ) ::_thesis: ( a * b = b * a implies a |^ b = a )
proof
assume a |^ b = a ; ::_thesis: a * b = b * a
then a = (b ") * (a * b) by GROUP_1:def_3;
hence a * b = b * a by GROUP_1:13; ::_thesis: verum
end;
assume a * b = b * a ; ::_thesis: a |^ b = a
then a = (b ") * (a * b) by GROUP_1:13;
hence a |^ b = a by GROUP_1:def_3; ::_thesis: verum
end;
theorem Th23: :: GROUP_3:23
for G being Group
for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)
proof
let G be Group; ::_thesis: for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)
let a, b, g be Element of G; ::_thesis: (a * b) |^ g = (a |^ g) * (b |^ g)
thus (a * b) |^ g = ((g ") * ((a * (1_ G)) * b)) * g by GROUP_1:def_4
.= ((g ") * ((a * (g * (g "))) * b)) * g by GROUP_1:def_5
.= ((g ") * (((a * g) * (g ")) * b)) * g by GROUP_1:def_3
.= ((g ") * ((a * g) * ((g ") * b))) * g by GROUP_1:def_3
.= (((g ") * (a * g)) * ((g ") * b)) * g by GROUP_1:def_3
.= ((a |^ g) * ((g ") * b)) * g by GROUP_1:def_3
.= (a |^ g) * (b |^ g) by GROUP_1:def_3 ; ::_thesis: verum
end;
theorem Th24: :: GROUP_3:24
for G being Group
for a, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h)
proof
let G be Group; ::_thesis: for a, g, h being Element of G holds (a |^ g) |^ h = a |^ (g * h)
let a, g, h be Element of G; ::_thesis: (a |^ g) |^ h = a |^ (g * h)
thus (a |^ g) |^ h = (((h ") * ((g ") * a)) * g) * h by GROUP_1:def_3
.= ((((h ") * (g ")) * a) * g) * h by GROUP_1:def_3
.= ((((g * h) ") * a) * g) * h by GROUP_1:17
.= a |^ (g * h) by GROUP_1:def_3 ; ::_thesis: verum
end;
theorem Th25: :: GROUP_3:25
for G being Group
for a, b being Element of G holds
( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )
let a, b be Element of G; ::_thesis: ( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )
thus (a |^ b) |^ (b ") = a |^ (b * (b ")) by Th24
.= a |^ (1_ G) by GROUP_1:def_5
.= a by Th19 ; ::_thesis: (a |^ (b ")) |^ b = a
thus (a |^ (b ")) |^ b = a |^ ((b ") * b) by Th24
.= a |^ (1_ G) by GROUP_1:def_5
.= a by Th19 ; ::_thesis: verum
end;
theorem Th26: :: GROUP_3:26
for G being Group
for a, b being Element of G holds (a ") |^ b = (a |^ b) "
proof
let G be Group; ::_thesis: for a, b being Element of G holds (a ") |^ b = (a |^ b) "
let a, b be Element of G; ::_thesis: (a ") |^ b = (a |^ b) "
thus (a ") |^ b = ((a * b) ") * b by GROUP_1:17
.= ((a * b) ") * ((b ") ")
.= ((b ") * (a * b)) " by GROUP_1:17
.= (a |^ b) " by GROUP_1:def_3 ; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_G_being_Group
for_a,_b_being_Element_of_G_holds_(a_|^_0)_|^_b_=_(a_|^_b)_|^_0
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; ::_thesis: (a |^ 0) |^ b = (a |^ b) |^ 0
thus (a |^ 0) |^ b = (1_ G) |^ b by GROUP_1:25
.= 1_ G by Th17
.= (a |^ b) |^ 0 by GROUP_1:25 ; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_n_being_Nat_st_(_for_G_being_Group
for_a,_b_being_Element_of_G_holds_(a_|^_n)_|^_b_=_(a_|^_b)_|^_n_)_holds_
for_G_being_Group
for_a,_b_being_Element_of_G_holds_(a_|^_(n_+_1))_|^_b_=_(a_|^_b)_|^_(n_+_1)
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; ::_thesis: (a |^ (n + 1)) |^ b = (a |^ b) |^ (n + 1)
thus (a |^ (n + 1)) |^ b = ((a |^ n) * a) |^ b by GROUP_1:34
.= ((a |^ n) |^ b) * (a |^ b) by Th23
.= ((a |^ b) |^ n) * (a |^ b) by A1
.= (a |^ b) |^ (n + 1) by GROUP_1:34 ; ::_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
defpred S1[ Nat] means for G being Group
for a, b being Element of G holds (a |^ $1) |^ b = (a |^ b) |^ $1;
A1: for k being Nat st S1[k] holds
S1[k + 1] by Lm3;
A2: S1[ 0 ] by Lm2;
for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n ; ::_thesis: verum
end;
theorem :: GROUP_3:27
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:28
for G being Group
for a, b being Element of G
for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
proof
let G be Group; ::_thesis: for a, b being Element of G
for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
let a, b be Element of G; ::_thesis: for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
let i be Integer; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i
then i = abs i by ABSVALUE:def_1;
hence (a |^ i) |^ b = (a |^ b) |^ i by Lm4; ::_thesis: verum
end;
supposeA1: i < 0 ; ::_thesis: (a |^ i) |^ b = (a |^ b) |^ i
hence (a |^ i) |^ b = ((a |^ (abs i)) ") |^ b by GROUP_1:30
.= ((a |^ (abs i)) |^ b) " by Th26
.= ((a |^ b) |^ (abs i)) " by Lm4
.= (a |^ b) |^ i by A1, GROUP_1:30 ;
::_thesis: verum
end;
end;
end;
theorem Th29: :: GROUP_3:29
for G being Group
for a, b being Element of G st G is commutative Group holds
a |^ b = a
proof
let G be Group; ::_thesis: for a, b being Element of G st G is commutative Group holds
a |^ b = a
let a, b be Element of G; ::_thesis: ( G is commutative Group implies a |^ b = a )
assume G is commutative Group ; ::_thesis: a |^ b = a
hence a |^ b = (a * (b ")) * b by Lm1
.= a by Th1 ;
::_thesis: verum
end;
theorem Th30: :: GROUP_3:30
for G being Group st ( for a, b being Element of G holds a |^ b = a ) holds
G is commutative
proof
let G be Group; ::_thesis: ( ( for a, b being Element of G holds a |^ b = a ) implies G is commutative )
assume A1: for a, b being Element of G holds a |^ b = a ; ::_thesis: G is commutative
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
a |^ b = a by A1;
hence a * b = b * a by Th22; ::_thesis: verum
end;
definition
let G be Group;
let A, B be Subset of G;
funcA |^ 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
set X = { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ;
{ (g |^ h) where g, h is Element of G : ( g in A & h in B ) } c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } or x in the carrier of G )
assume x in { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } ; ::_thesis: x in the carrier of G
then ex g, h being Element of G st
( x = g |^ h & g in A & h in B ) ;
hence x in the carrier of G ; ::_thesis: verum
end;
hence { (g |^ h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G ; ::_thesis: verum
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 Th31: :: GROUP_3:31
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 Th32: :: GROUP_3:32
for G being Group
for A, B being Subset of G holds
( A |^ B <> {} iff ( A <> {} & B <> {} ) )
proof
let G be Group; ::_thesis: for A, B being Subset of G holds
( A |^ B <> {} iff ( A <> {} & B <> {} ) )
let A, B be Subset of G; ::_thesis: ( A |^ B <> {} iff ( A <> {} & B <> {} ) )
set x = the Element of A;
set y = the Element of B;
thus ( A |^ B <> {} implies ( A <> {} & B <> {} ) ) ::_thesis: ( A <> {} & B <> {} implies A |^ B <> {} )
proof
set x = the Element of A |^ B;
assume A |^ B <> {} ; ::_thesis: ( A <> {} & B <> {} )
then ex a, b being Element of G st
( the Element of A |^ B = a |^ b & a in A & b in B ) by Th31;
hence ( A <> {} & B <> {} ) ; ::_thesis: verum
end;
assume A1: A <> {} ; ::_thesis: ( not B <> {} or A |^ B <> {} )
assume A2: B <> {} ; ::_thesis: A |^ B <> {}
then reconsider x = the Element of A, y = the Element of B as Element of G by A1, TARSKI:def_3;
x |^ y in A |^ B by A1, A2;
hence A |^ B <> {} ; ::_thesis: verum
end;
theorem Th33: :: GROUP_3:33
for G being Group
for A, B being Subset of G holds A |^ B c= ((B ") * A) * B
proof
let G be Group; ::_thesis: for A, B being Subset of G holds A |^ B c= ((B ") * A) * B
let A, B be Subset of G; ::_thesis: A |^ B c= ((B ") * A) * B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ B or x in ((B ") * A) * B )
assume x in A |^ B ; ::_thesis: x in ((B ") * A) * B
then consider a, b being Element of G such that
A1: x = a |^ b and
A2: a in A and
A3: b in B ;
b " in B " by A3;
then (b ") * a in (B ") * A by A2;
hence x in ((B ") * A) * B by A1, A3; ::_thesis: verum
end;
theorem Th34: :: GROUP_3:34
for G being Group
for A, B, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C)
proof
let G be Group; ::_thesis: for A, B, C being Subset of G holds (A * B) |^ C c= (A |^ C) * (B |^ C)
let A, B, C be Subset of G; ::_thesis: (A * B) |^ C c= (A |^ C) * (B |^ C)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) |^ C or x in (A |^ C) * (B |^ C) )
assume x in (A * B) |^ C ; ::_thesis: x in (A |^ C) * (B |^ C)
then consider a, b being Element of G such that
A1: x = a |^ b and
A2: a in A * B and
A3: b in C ;
consider g, h being Element of G such that
A4: ( a = g * h & g in A ) and
A5: h in B by A2;
A6: h |^ b in B |^ C by A3, A5;
( x = (g |^ b) * (h |^ b) & g |^ b in A |^ C ) by A1, A3, A4, Th23;
hence x in (A |^ C) * (B |^ C) by A6; ::_thesis: verum
end;
theorem Th35: :: GROUP_3:35
for G being Group
for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C)
proof
let G be Group; ::_thesis: for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C)
let A, B, C be Subset of G; ::_thesis: (A |^ B) |^ C = A |^ (B * C)
thus (A |^ B) |^ C c= A |^ (B * C) :: according to XBOOLE_0:def_10 ::_thesis: A |^ (B * C) c= (A |^ B) |^ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ B) |^ C or x in A |^ (B * C) )
assume x in (A |^ B) |^ C ; ::_thesis: x in A |^ (B * C)
then consider a, c being Element of G such that
A1: x = a |^ c and
A2: a in A |^ B and
A3: c in C ;
consider g, h being Element of G such that
A4: a = g |^ h and
A5: g in A and
A6: h in B by A2;
( x = g |^ (h * c) & h * c in B * C ) by A1, A3, A4, A6, Th24;
hence x in A |^ (B * C) by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (B * C) or x in (A |^ B) |^ C )
assume x in A |^ (B * C) ; ::_thesis: x in (A |^ B) |^ C
then consider a, b being Element of G such that
A7: ( x = a |^ b & a in A ) and
A8: b in B * C ;
consider g, h being Element of G such that
A9: ( b = g * h & g in B ) and
A10: h in C by A8;
( a |^ g in A |^ B & x = (a |^ g) |^ h ) by A7, A9, Th24;
hence x in (A |^ B) |^ C by A10; ::_thesis: verum
end;
theorem :: GROUP_3:36
for G being Group
for A, B being Subset of G holds (A ") |^ B = (A |^ B) "
proof
let G be Group; ::_thesis: for A, B being Subset of G holds (A ") |^ B = (A |^ B) "
let A, B be Subset of G; ::_thesis: (A ") |^ B = (A |^ B) "
thus (A ") |^ B c= (A |^ B) " :: according to XBOOLE_0:def_10 ::_thesis: (A |^ B) " c= (A ") |^ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ") |^ B or x in (A |^ B) " )
assume x in (A ") |^ B ; ::_thesis: x in (A |^ B) "
then consider a, b being Element of G such that
A1: x = a |^ b and
A2: a in A " and
A3: b in B ;
consider c being Element of G such that
A4: ( a = c " & c in A ) by A2;
( x = (c |^ b) " & c |^ b in A |^ B ) by A1, A3, A4, Th26;
hence x in (A |^ B) " ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ B) " or x in (A ") |^ B )
assume x in (A |^ B) " ; ::_thesis: x in (A ") |^ B
then consider a being Element of G such that
A5: x = a " and
A6: a in A |^ B ;
consider b, c being Element of G such that
A7: a = b |^ c and
A8: b in A and
A9: c in B by A6;
A10: b " in A " by A8;
x = (b ") |^ c by A5, A7, Th26;
hence x in (A ") |^ B by A9, A10; ::_thesis: verum
end;
theorem Th37: :: GROUP_3:37
for G being Group
for a, b being Element of G holds {a} |^ {b} = {(a |^ b)}
proof
let G be Group; ::_thesis: for a, b being Element of G holds {a} |^ {b} = {(a |^ b)}
let a, b be Element of G; ::_thesis: {a} |^ {b} = {(a |^ b)}
A1: (({b} ") * {a}) * {b} = ({(b ")} * {a}) * {b} by GROUP_2:3
.= {((b ") * a)} * {b} by GROUP_2:18
.= {(a |^ b)} by GROUP_2:18 ;
( {a} |^ {b} c= (({b} ") * {a}) * {b} & {a} |^ {b} <> {} ) by Th32, Th33;
hence {a} |^ {b} = {(a |^ b)} by A1, ZFMISC_1:33; ::_thesis: verum
end;
theorem :: GROUP_3:38
for G being Group
for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)}
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds {a} |^ {b,c} = {(a |^ b),(a |^ c)}
let a, b, c be Element of G; ::_thesis: {a} |^ {b,c} = {(a |^ b),(a |^ c)}
thus {a} |^ {b,c} c= {(a |^ b),(a |^ c)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ b),(a |^ c)} c= {a} |^ {b,c}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} |^ {b,c} or x in {(a |^ b),(a |^ c)} )
assume x in {a} |^ {b,c} ; ::_thesis: x in {(a |^ b),(a |^ c)}
then consider g, h being Element of G such that
A1: x = g |^ h and
A2: g in {a} and
A3: h in {b,c} ;
A4: ( h = b or h = c ) by A3, TARSKI:def_2;
g = a by A2, TARSKI:def_1;
hence x in {(a |^ b),(a |^ c)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ b),(a |^ c)} or x in {a} |^ {b,c} )
A5: c in {b,c} by TARSKI:def_2;
assume x in {(a |^ b),(a |^ c)} ; ::_thesis: x in {a} |^ {b,c}
then A6: ( x = a |^ b or x = a |^ c ) by TARSKI:def_2;
( a in {a} & b in {b,c} ) by TARSKI:def_1, TARSKI:def_2;
hence x in {a} |^ {b,c} by A6, A5; ::_thesis: verum
end;
theorem :: GROUP_3:39
for G being Group
for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)}
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds {a,b} |^ {c} = {(a |^ c),(b |^ c)}
let a, b, c be Element of G; ::_thesis: {a,b} |^ {c} = {(a |^ c),(b |^ c)}
thus {a,b} |^ {c} c= {(a |^ c),(b |^ c)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ c),(b |^ c)} c= {a,b} |^ {c}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} |^ {c} or x in {(a |^ c),(b |^ c)} )
assume x in {a,b} |^ {c} ; ::_thesis: x in {(a |^ c),(b |^ c)}
then consider g, h being Element of G such that
A1: x = g |^ h and
A2: g in {a,b} and
A3: h in {c} ;
A4: ( g = b or g = a ) by A2, TARSKI:def_2;
h = c by A3, TARSKI:def_1;
hence x in {(a |^ c),(b |^ c)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ c),(b |^ c)} or x in {a,b} |^ {c} )
A5: c in {c} by TARSKI:def_1;
assume x in {(a |^ c),(b |^ c)} ; ::_thesis: x in {a,b} |^ {c}
then A6: ( x = a |^ c or x = b |^ c ) by TARSKI:def_2;
( a in {a,b} & b in {a,b} ) by TARSKI:def_2;
hence x in {a,b} |^ {c} by A6, A5; ::_thesis: verum
end;
theorem :: GROUP_3:40
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
let G be Group; ::_thesis: for a, b, c, d being Element of G holds {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
let a, b, c, d be Element of G; ::_thesis: {a,b} |^ {c,d} = {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
thus {a,b} |^ {c,d} c= {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} :: according to XBOOLE_0:def_10 ::_thesis: {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} c= {a,b} |^ {c,d}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} |^ {c,d} or x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} )
assume x in {a,b} |^ {c,d} ; ::_thesis: x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)}
then consider g, h being Element of G such that
A1: x = g |^ h and
A2: g in {a,b} and
A3: h in {c,d} ;
A4: ( h = c or h = d ) by A3, TARSKI:def_2;
( g = a or g = b ) by A2, TARSKI:def_2;
hence x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} by A1, A4, ENUMSET1:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} or x in {a,b} |^ {c,d} )
A5: ( c in {c,d} & d in {c,d} ) by TARSKI:def_2;
assume x in {(a |^ c),(a |^ d),(b |^ c),(b |^ d)} ; ::_thesis: x in {a,b} |^ {c,d}
then A6: ( x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d ) by ENUMSET1:def_2;
( a in {a,b} & b in {a,b} ) by TARSKI:def_2;
hence x in {a,b} |^ {c,d} by A6, A5; ::_thesis: verum
end;
definition
let G be Group;
let A be Subset of G;
let g be Element of G;
funcA |^ g -> Subset of G equals :: GROUP_3:def 4
A |^ {g};
correctness
coherence
A |^ {g} is Subset of G;
;
funcg |^ 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 Th41: :: GROUP_3:41
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
let x be set ; ::_thesis: 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 ) )
let G be Group; ::_thesis: 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 ) )
let g be Element of G; ::_thesis: 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 ) )
let A be Subset of G; ::_thesis: ( x in A |^ g iff ex h being Element of G st
( x = h |^ g & h in A ) )
thus ( x in A |^ g implies ex h being Element of G st
( x = h |^ g & h in A ) ) ::_thesis: ( ex h being Element of G st
( x = h |^ g & h in A ) implies x in A |^ g )
proof
assume x in A |^ g ; ::_thesis: ex h being Element of G st
( x = h |^ g & h in A )
then consider a, b being Element of G such that
A1: ( x = a |^ b & a in A ) and
A2: b in {g} ;
b = g by A2, TARSKI:def_1;
hence ex h being Element of G st
( x = h |^ g & h in A ) by A1; ::_thesis: verum
end;
given h being Element of G such that A3: ( x = h |^ g & h in A ) ; ::_thesis: x in A |^ g
g in {g} by TARSKI:def_1;
hence x in A |^ g by A3; ::_thesis: verum
end;
theorem Th42: :: GROUP_3:42
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
let x be set ; ::_thesis: 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 ) )
let G be Group; ::_thesis: 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 ) )
let g be Element of G; ::_thesis: 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 ) )
let A be Subset of G; ::_thesis: ( x in g |^ A iff ex h being Element of G st
( x = g |^ h & h in A ) )
thus ( x in g |^ A implies ex h being Element of G st
( x = g |^ h & h in A ) ) ::_thesis: ( ex h being Element of G st
( x = g |^ h & h in A ) implies x in g |^ A )
proof
assume x in g |^ A ; ::_thesis: ex h being Element of G st
( x = g |^ h & h in A )
then consider a, b being Element of G such that
A1: x = a |^ b and
A2: a in {g} and
A3: b in A ;
a = g by A2, TARSKI:def_1;
hence ex h being Element of G st
( x = g |^ h & h in A ) by A1, A3; ::_thesis: verum
end;
given h being Element of G such that A4: ( x = g |^ h & h in A ) ; ::_thesis: x in g |^ A
g in {g} by TARSKI:def_1;
hence x in g |^ A by A4; ::_thesis: verum
end;
theorem :: GROUP_3:43
for G being Group
for g being Element of G
for A being Subset of G holds g |^ A c= ((A ") * g) * A
proof
let G be Group; ::_thesis: for g being Element of G
for A being Subset of G holds g |^ A c= ((A ") * g) * A
let g be Element of G; ::_thesis: for A being Subset of G holds g |^ A c= ((A ") * g) * A
let A be Subset of G; ::_thesis: g |^ A c= ((A ") * g) * A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g |^ A or x in ((A ") * g) * A )
assume x in g |^ A ; ::_thesis: x in ((A ") * g) * A
then consider a being Element of G such that
A1: x = g |^ a and
A2: a in A by Th42;
a " in A " by A2;
then (a ") * g in (A ") * g by GROUP_2:28;
hence x in ((A ") * g) * A by A1, A2; ::_thesis: verum
end;
theorem :: GROUP_3:44
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 Th35;
theorem :: GROUP_3:45
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 Th35;
theorem :: GROUP_3:46
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 Th35;
theorem Th47: :: GROUP_3:47
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
let G be Group; ::_thesis: for a, b being Element of G
for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
let a, b be Element of G; ::_thesis: for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
let A be Subset of G; ::_thesis: (A |^ a) |^ b = A |^ (a * b)
thus (A |^ a) |^ b = A |^ (a * {b}) by Th35
.= A |^ (a * b) by GROUP_2:18 ; ::_thesis: verum
end;
theorem :: GROUP_3:48
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 Th35;
theorem :: GROUP_3:49
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
let G be Group; ::_thesis: for a, b being Element of G
for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)
let a, b be Element of G; ::_thesis: for A being Subset of G holds (a |^ b) |^ A = a |^ (b * A)
let A be Subset of G; ::_thesis: (a |^ b) |^ A = a |^ (b * A)
thus (a |^ b) |^ A = ({a} |^ {b}) |^ A by Th37
.= a |^ (b * A) by Th35 ; ::_thesis: verum
end;
theorem Th50: :: GROUP_3:50
for G being Group
for g being Element of G
for A being Subset of G holds A |^ g = ((g ") * A) * g
proof
let G be Group; ::_thesis: for g being Element of G
for A being Subset of G holds A |^ g = ((g ") * A) * g
let g be Element of G; ::_thesis: for A being Subset of G holds A |^ g = ((g ") * A) * g
let A be Subset of G; ::_thesis: A |^ g = ((g ") * A) * g
A |^ g c= (({g} ") * A) * {g} by Th33;
hence A |^ g c= ((g ") * A) * g by GROUP_2:3; :: according to XBOOLE_0:def_10 ::_thesis: ((g ") * A) * g c= A |^ g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((g ") * A) * g or x in A |^ g )
assume x in ((g ") * A) * g ; ::_thesis: x in A |^ g
then consider a being Element of G such that
A1: x = a * g and
A2: a in (g ") * A by GROUP_2:28;
consider b being Element of G such that
A3: a = (g ") * b and
A4: b in A by A2, GROUP_2:27;
x = b |^ g by A1, A3;
hence x in A |^ g by A4, Th41; ::_thesis: verum
end;
theorem :: GROUP_3:51
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 Th34;
theorem Th52: :: GROUP_3:52
for G being Group
for A being Subset of G holds A |^ (1_ G) = A
proof
let G be Group; ::_thesis: for A being Subset of G holds A |^ (1_ G) = A
let A be Subset of G; ::_thesis: A |^ (1_ G) = A
thus A |^ (1_ G) = (((1_ G) ") * A) * (1_ G) by Th50
.= ((1_ G) ") * A by GROUP_2:37
.= (1_ G) * A by GROUP_1:8
.= A by GROUP_2:37 ; ::_thesis: verum
end;
theorem :: GROUP_3:53
for G being Group
for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}
proof
let G be Group; ::_thesis: for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}
let A be Subset of G; ::_thesis: ( A <> {} implies (1_ G) |^ A = {(1_ G)} )
set y = the Element of A;
assume A1: A <> {} ; ::_thesis: (1_ G) |^ A = {(1_ G)}
then reconsider y = the Element of A as Element of G by TARSKI:def_3;
thus (1_ G) |^ A c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= (1_ G) |^ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (1_ G) |^ A or x in {(1_ G)} )
assume x in (1_ G) |^ A ; ::_thesis: x in {(1_ G)}
then ex a being Element of G st
( x = (1_ G) |^ a & a in A ) by Th42;
then x = 1_ G by Th17;
hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(1_ G)} or x in (1_ G) |^ A )
assume x in {(1_ G)} ; ::_thesis: x in (1_ G) |^ A
then x = 1_ G by TARSKI:def_1;
then (1_ G) |^ y = x by Th17;
hence x in (1_ G) |^ A by A1, Th42; ::_thesis: verum
end;
theorem Th54: :: GROUP_3:54
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
let G be Group; ::_thesis: for a being Element of G
for A being Subset of G holds
( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
let a be Element of G; ::_thesis: for A being Subset of G holds
( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
let A be Subset of G; ::_thesis: ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
thus (A |^ a) |^ (a ") = A |^ (a * (a ")) by Th47
.= A |^ (1_ G) by GROUP_1:def_5
.= A by Th52 ; ::_thesis: (A |^ (a ")) |^ a = A
thus (A |^ (a ")) |^ a = A |^ ((a ") * a) by Th47
.= A |^ (1_ G) by GROUP_1:def_5
.= A by Th52 ; ::_thesis: verum
end;
theorem Th55: :: GROUP_3:55
for G being Group holds
( G is commutative Group iff for A, B being Subset of G st B <> {} holds
A |^ B = A )
proof
let G be Group; ::_thesis: ( G is commutative Group iff for A, B being Subset of G st B <> {} holds
A |^ B = A )
thus ( G is commutative Group implies for A, B being Subset of G st B <> {} holds
A |^ B = A ) ::_thesis: ( ( for A, B being Subset of G st B <> {} holds
A |^ B = A ) implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: for A, B being Subset of G st B <> {} holds
A |^ B = A
let A, B be Subset of G; ::_thesis: ( B <> {} implies A |^ B = A )
set y = the Element of B;
assume A2: B <> {} ; ::_thesis: A |^ B = A
then reconsider y = the Element of B as Element of G by TARSKI:def_3;
thus A |^ B c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A |^ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ B or x in A )
assume x in A |^ B ; ::_thesis: x in A
then ex a, b being Element of G st
( x = a |^ b & a in A & b in B ) ;
hence x in A by A1, Th29; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A |^ B )
assume A3: x in A ; ::_thesis: x in A |^ B
then reconsider a = x as Element of G ;
a |^ y = x by A1, Th29;
hence x in A |^ B by A2, A3; ::_thesis: verum
end;
assume A4: for A, B being Subset of G st B <> {} holds
A |^ B = A ; ::_thesis: G is commutative Group
now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b
let a, b be Element of G; ::_thesis: a = a |^ b
{a} = {a} |^ {b} by A4
.= {(a |^ b)} by Th37 ;
hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum
end;
hence G is commutative Group by Th30; ::_thesis: verum
end;
theorem :: GROUP_3:56
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
let G be Group; ::_thesis: ( G is commutative Group iff for A being Subset of G
for g being Element of G holds A |^ g = A )
thus ( G is commutative Group implies for A being Subset of G
for g being Element of G holds A |^ g = A ) by Th55; ::_thesis: ( ( for A being Subset of G
for g being Element of G holds A |^ g = A ) implies G is commutative Group )
assume A1: for A being Subset of G
for g being Element of G holds A |^ g = A ; ::_thesis: G is commutative Group
now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b
let a, b be Element of G; ::_thesis: a = a |^ b
{a} = {a} |^ b by A1
.= {(a |^ b)} by Th37 ;
hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum
end;
hence G is commutative Group by Th30; ::_thesis: verum
end;
theorem :: GROUP_3:57
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
let G be Group; ::_thesis: ( G is commutative Group iff for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} )
thus ( G is commutative Group implies for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} ) by Th55; ::_thesis: ( ( for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} ) implies G is commutative Group )
assume A1: for A being Subset of G
for g being Element of G st A <> {} holds
g |^ A = {g} ; ::_thesis: G is commutative Group
now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_a_|^_b
let a, b be Element of G; ::_thesis: a = a |^ b
{a} = a |^ {b} by A1
.= {(a |^ b)} by Th37 ;
hence a = a |^ b by ZFMISC_1:3; ::_thesis: verum
end;
hence G is commutative Group by Th30; ::_thesis: verum
end;
definition
let G be Group;
let H be Subgroup of G;
let a be Element of G;
funcH |^ 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
consider H1 being strict Subgroup of G such that
A1: the carrier of H1 = ((a ") * H) * ((a ") ") by GROUP_2:127;
the carrier of H1 = ((a ") * (carr H)) * a by A1
.= (carr H) |^ a by Th50 ;
hence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H) |^ a ; ::_thesis: verum
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:59;
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 Th58: :: GROUP_3:58
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
let x be set ; ::_thesis: 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 ) )
let G be Group; ::_thesis: 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 ) )
let a be Element of G; ::_thesis: 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 ) )
let H be Subgroup of G; ::_thesis: ( x in H |^ a iff ex g being Element of G st
( x = g |^ a & g in H ) )
thus ( x in H |^ a implies ex g being Element of G st
( x = g |^ a & g in H ) ) ::_thesis: ( ex g being Element of G st
( x = g |^ a & g in H ) implies x in H |^ a )
proof
assume x in H |^ a ; ::_thesis: ex g being Element of G st
( x = g |^ a & g in H )
then x in the carrier of (H |^ a) by STRUCT_0:def_5;
then x in (carr H) |^ a by Def6;
then consider b being Element of G such that
A1: ( x = b |^ a & b in carr H ) by Th41;
take b ; ::_thesis: ( x = b |^ a & b in H )
thus ( x = b |^ a & b in H ) by A1, STRUCT_0:def_5; ::_thesis: verum
end;
given g being Element of G such that A2: x = g |^ a and
A3: g in H ; ::_thesis: x in H |^ a
g in carr H by A3, STRUCT_0:def_5;
then x in (carr H) |^ a by A2, Th41;
then x in the carrier of (H |^ a) by Def6;
hence x in H |^ a by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th59: :: GROUP_3:59
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
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a
let a be Element of G; ::_thesis: for H being Subgroup of G holds the carrier of (H |^ a) = ((a ") * H) * a
let H be Subgroup of G; ::_thesis: the carrier of (H |^ a) = ((a ") * H) * a
thus the carrier of (H |^ a) = (carr H) |^ a by Def6
.= ((a ") * H) * a by Th50 ; ::_thesis: verum
end;
theorem Th60: :: GROUP_3:60
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
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
let H be Subgroup of G; ::_thesis: (H |^ a) |^ b = H |^ (a * b)
the carrier of ((H |^ a) |^ b) = (carr (H |^ a)) |^ b by Def6
.= ((carr H) |^ a) |^ b by Def6
.= (carr H) |^ (a * b) by Th47
.= the carrier of (H |^ (a * b)) by Def6 ;
hence (H |^ a) |^ b = H |^ (a * b) by GROUP_2:59; ::_thesis: verum
end;
theorem Th61: :: GROUP_3:61
for G being Group
for H being strict Subgroup of G holds H |^ (1_ G) = H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds H |^ (1_ G) = H
let H be strict Subgroup of G; ::_thesis: H |^ (1_ G) = H
the carrier of (H |^ (1_ G)) = (carr H) |^ (1_ G) by Def6
.= the carrier of H by Th52 ;
hence H |^ (1_ G) = H by GROUP_2:59; ::_thesis: verum
end;
theorem Th62: :: GROUP_3:62
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
let G be Group; ::_thesis: for a being Element of G
for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
let a be Element of G; ::_thesis: for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
let H be strict Subgroup of G; ::_thesis: ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
thus (H |^ a) |^ (a ") = H |^ (a * (a ")) by Th60
.= H |^ (1_ G) by GROUP_1:def_5
.= H by Th61 ; ::_thesis: (H |^ (a ")) |^ a = H
thus (H |^ (a ")) |^ a = H |^ ((a ") * a) by Th60
.= H |^ (1_ G) by GROUP_1:def_5
.= H by Th61 ; ::_thesis: verum
end;
theorem Th63: :: GROUP_3:63
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
let G be Group; ::_thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let H1, H2 be Subgroup of G; ::_thesis: (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
let g be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not g in (H1 /\ H2) |^ a or g in (H1 |^ a) /\ (H2 |^ a) ) & ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a ) )
thus ( g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a) ) ::_thesis: ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a )
proof
assume g in (H1 /\ H2) |^ a ; ::_thesis: g in (H1 |^ a) /\ (H2 |^ a)
then consider h being Element of G such that
A1: g = h |^ a and
A2: h in H1 /\ H2 by Th58;
h in H2 by A2, GROUP_2:82;
then A3: g in H2 |^ a by A1, Th58;
h in H1 by A2, GROUP_2:82;
then g in H1 |^ a by A1, Th58;
hence g in (H1 |^ a) /\ (H2 |^ a) by A3, GROUP_2:82; ::_thesis: verum
end;
assume A4: g in (H1 |^ a) /\ (H2 |^ a) ; ::_thesis: g in (H1 /\ H2) |^ a
then g in H1 |^ a by GROUP_2:82;
then consider b being Element of G such that
A5: g = b |^ a and
A6: b in H1 by Th58;
g in H2 |^ a by A4, GROUP_2:82;
then consider c being Element of G such that
A7: g = c |^ a and
A8: c in H2 by Th58;
b = c by A5, A7, Th16;
then b in H1 /\ H2 by A6, A8, GROUP_2:82;
hence g in (H1 /\ H2) |^ a by A5, Th58; ::_thesis: verum
end;
theorem Th64: :: GROUP_3:64
for G being Group
for a being Element of G
for H being Subgroup of G holds card H = card (H |^ a)
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds card H = card (H |^ a)
let a be Element of G; ::_thesis: for H being Subgroup of G holds card H = card (H |^ a)
let H be Subgroup of G; ::_thesis: card H = card (H |^ a)
deffunc H1( Element of G) -> Element of G = $1 |^ a;
consider f being Function of the carrier of G, the carrier of G such that
A1: for g being Element of G holds f . g = H1(g) from FUNCT_2:sch_4();
set g = f | the carrier of H;
A2: ( dom f = the carrier of G & the carrier of H c= the carrier of G ) by FUNCT_2:def_1, GROUP_2:def_5;
then A3: dom (f | the carrier of H) = the carrier of H by RELAT_1:62;
A4: rng (f | the carrier of H) = the carrier of (H |^ a)
proof
thus rng (f | the carrier of H) c= the carrier of (H |^ a) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (H |^ a) c= rng (f | the carrier of H)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | the carrier of H) or x in the carrier of (H |^ a) )
assume x in rng (f | the carrier of H) ; ::_thesis: x in the carrier of (H |^ a)
then consider y being set such that
A5: y in dom (f | the carrier of H) and
A6: (f | the carrier of H) . y = x by FUNCT_1:def_3;
reconsider y = y as Element of H by A2, A5, RELAT_1:62;
reconsider y = y as Element of G by GROUP_2:42;
A7: f . y = (f | the carrier of H) . y by A5, FUNCT_1:47;
f . y = y |^ a by A1;
then x in (carr H) |^ a by A6, A7, Th41;
hence x in the carrier of (H |^ a) by Def6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (H |^ a) or x in rng (f | the carrier of H) )
assume x in the carrier of (H |^ a) ; ::_thesis: x in rng (f | the carrier of H)
then x in (carr H) |^ a by Def6;
then consider b being Element of G such that
A8: x = b |^ a and
A9: b in carr H by Th41;
A10: f . b = b |^ a by A1;
(f | the carrier of H) . b = f . b by A3, A9, FUNCT_1:47;
hence x in rng (f | the carrier of H) by A3, A8, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
f | the carrier of H is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (f | the carrier of H) or not b1 in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (f | the carrier of H) or not y in dom (f | the carrier of H) or not (f | the carrier of H) . x = (f | the carrier of H) . y or x = y )
assume that
A11: x in dom (f | the carrier of H) and
A12: y in dom (f | the carrier of H) and
A13: (f | the carrier of H) . x = (f | the carrier of H) . y ; ::_thesis: x = y
reconsider b = x, c = y as Element of H by A2, A11, A12, RELAT_1:62;
reconsider b = b, c = c as Element of G by GROUP_2:42;
A14: ( f . x = b |^ a & f . y = c |^ a ) by A1;
f . x = (f | the carrier of H) . x by A11, FUNCT_1:47;
hence x = y by A12, A13, A14, Th16, FUNCT_1:47; ::_thesis: verum
end;
then the carrier of H, the carrier of (H |^ a) are_equipotent by A3, A4, WELLORD2:def_4;
hence card H = card (H |^ a) by CARD_1:5; ::_thesis: verum
end;
theorem Th65: :: GROUP_3:65
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
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
let H be Subgroup of G; ::_thesis: ( H is finite iff H |^ a is finite )
card H = card (H |^ a) by Th64;
then the carrier of H, the carrier of (H |^ a) are_equipotent by CARD_1:5;
hence ( H is finite iff H |^ a is finite ) by CARD_1:38; ::_thesis: verum
end;
registration
let G be Group;
let a be Element of G;
let H be finite Subgroup of G;
clusterH |^ a -> finite strict ;
coherence
H |^ a is finite by Th65;
end;
theorem :: GROUP_3:66
for G being Group
for a being Element of G
for H being finite Subgroup of G holds card H = card (H |^ a) by Th64;
theorem Th67: :: GROUP_3:67
for G being Group
for a being Element of G holds ((1). G) |^ a = (1). G
proof
let G be Group; ::_thesis: for a being Element of G holds ((1). G) |^ a = (1). G
let a be Element of G; ::_thesis: ((1). G) |^ a = (1). G
A1: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7;
the carrier of (((1). G) |^ a) = (carr ((1). G)) |^ a by Def6
.= {((1_ G) |^ a)} by A1, Th37
.= {(1_ G)} by Th17 ;
hence ((1). G) |^ a = (1). G by GROUP_2:def_7; ::_thesis: verum
end;
theorem :: GROUP_3:68
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
let G be Group; ::_thesis: for a being Element of G
for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
let a be Element of G; ::_thesis: for H being strict Subgroup of G st H |^ a = (1). G holds
H = (1). G
let H be strict Subgroup of G; ::_thesis: ( H |^ a = (1). G implies H = (1). G )
assume A1: H |^ a = (1). G ; ::_thesis: H = (1). G
then reconsider H = H as finite Subgroup of G by Th65;
card ((1). G) = 1 by GROUP_2:69;
then card H = 1 by A1, Th64;
hence H = (1). G by GROUP_2:70; ::_thesis: verum
end;
theorem Th69: :: GROUP_3:69
for G being Group
for a being Element of G holds ((Omega). G) |^ a = (Omega). G
proof
let G be Group; ::_thesis: for a being Element of G holds ((Omega). G) |^ a = (Omega). G
let a be Element of G; ::_thesis: ((Omega). G) |^ a = (Omega). G
let h be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) )
(h |^ (a ")) |^ a = h |^ ((a ") * a) by Th24
.= h |^ (1_ G) by GROUP_1:def_5
.= h by Th19 ;
hence ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) ) by Th58, STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: GROUP_3:70
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
let G be Group; ::_thesis: for a being Element of G
for H being strict Subgroup of G st H |^ a = G holds
H = G
let a be Element of G; ::_thesis: for H being strict Subgroup of G st H |^ a = G holds
H = G
let H be strict Subgroup of G; ::_thesis: ( H |^ a = G implies H = G )
assume A1: H |^ a = G ; ::_thesis: H = G
now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H
let g be Element of G; ::_thesis: g in H
assume A2: not g in H ; ::_thesis: contradiction
now__::_thesis:_not_g_|^_a_in_H_|^_a
assume g |^ a in H |^ a ; ::_thesis: contradiction
then ex h being Element of G st
( g |^ a = h |^ a & h in H ) by Th58;
hence contradiction by A2, Th16; ::_thesis: verum
end;
hence contradiction by A1, STRUCT_0:def_5; ::_thesis: verum
end;
hence H = G by A1, GROUP_2:62; ::_thesis: verum
end;
theorem Th71: :: GROUP_3:71
for G being Group
for a being Element of G
for H being Subgroup of G holds Index H = Index (H |^ a)
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds Index H = Index (H |^ a)
let a be Element of G; ::_thesis: for H being Subgroup of G holds Index H = Index (H |^ a)
let H be Subgroup of G; ::_thesis: Index H = Index (H |^ a)
defpred S1[ set , set ] means ex b being Element of G st
( $1 = b * H & $2 = (b |^ a) * (H |^ a) );
A1: for x being set st x in Left_Cosets H holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Left_Cosets H implies ex y being set st S1[x,y] )
assume x in Left_Cosets H ; ::_thesis: ex y being set st S1[x,y]
then consider b being Element of G such that
A2: x = b * H by GROUP_2:def_15;
reconsider y = (b |^ a) * (H |^ a) as set ;
take y ; ::_thesis: S1[x,y]
take b ; ::_thesis: ( x = b * H & y = (b |^ a) * (H |^ a) )
thus ( x = b * H & y = (b |^ a) * (H |^ a) ) by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being set st x in Left_Cosets H holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A5: for x, y1, y2 being set st x in Left_Cosets H & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
set A = carr H;
let x, y1, y2 be set ; ::_thesis: ( x in Left_Cosets H & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume x in Left_Cosets H ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 )
given b being Element of G such that A6: x = b * H and
A7: y1 = (b |^ a) * (H |^ a) ; ::_thesis: ( not S1[x,y2] or y1 = y2 )
given c being Element of G such that A8: x = c * H and
A9: y2 = (c |^ a) * (H |^ a) ; ::_thesis: y1 = y2
thus y1 = (((a ") * b) * a) * (((a ") * H) * a) by A7, Th59
.= ((((a ") * b) * a) * ((a ") * (carr H))) * a by GROUP_2:33
.= (((a ") * b) * (a * ((a ") * (carr H)))) * a by GROUP_2:32
.= (((a ") * b) * ((a * (a ")) * (carr H))) * a by GROUP_2:32
.= (((a ") * b) * ((1_ G) * (carr H))) * a by GROUP_1:def_5
.= (((a ") * b) * (carr H)) * a by GROUP_2:37
.= ((a ") * (c * H)) * a by A6, A8, GROUP_2:32
.= (((a ") * c) * (carr H)) * a by GROUP_2:32
.= (((a ") * c) * ((1_ G) * (carr H))) * a by GROUP_2:37
.= (((a ") * c) * ((a * (a ")) * (carr H))) * a by GROUP_1:def_5
.= (((a ") * c) * (a * ((a ") * (carr H)))) * a by GROUP_2:32
.= ((((a ") * c) * a) * ((a ") * (carr H))) * a by GROUP_2:32
.= (((a ") * c) * a) * (((a ") * H) * a) by GROUP_2:33
.= y2 by A9, Th59 ; ::_thesis: verum
end;
A10: rng f = Left_Cosets (H |^ a)
proof
thus rng f c= Left_Cosets (H |^ a) :: according to XBOOLE_0:def_10 ::_thesis: Left_Cosets (H |^ a) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Left_Cosets (H |^ a) )
assume x in rng f ; ::_thesis: x in Left_Cosets (H |^ a)
then consider y being set such that
A11: ( y in dom f & f . y = x ) by FUNCT_1:def_3;
ex b being Element of G st
( y = b * H & x = (b |^ a) * (H |^ a) ) by A3, A4, A11;
hence x in Left_Cosets (H |^ a) by GROUP_2:def_15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets (H |^ a) or x in rng f )
assume x in Left_Cosets (H |^ a) ; ::_thesis: x in rng f
then consider b being Element of G such that
A12: x = b * (H |^ a) by GROUP_2:def_15;
set c = b |^ (a ");
A13: x = ((b |^ (a ")) |^ a) * (H |^ a) by A12, Th25;
A14: (b |^ (a ")) * H in Left_Cosets H by GROUP_2:def_15;
then consider d being Element of G such that
A15: (b |^ (a ")) * H = d * H and
A16: f . ((b |^ (a ")) * H) = (d |^ a) * (H |^ a) by A4;
((b |^ (a ")) |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A5, A14, A15;
hence x in rng f by A3, A13, A14, A16, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A17: x in dom f and
A18: y in dom f and
A19: f . x = f . y ; ::_thesis: x = y
consider c being Element of G such that
A20: y = c * H and
A21: f . y = (c |^ a) * (H |^ a) by A3, A4, A18;
consider b being Element of G such that
A22: x = b * H and
A23: f . x = (b |^ a) * (H |^ a) by A3, A4, A17;
A24: ((c |^ a) ") * (b |^ a) = ((c ") |^ a) * (b |^ a) by Th26
.= ((c ") * b) |^ a by Th23 ;
((c |^ a) ") * (b |^ a) in H |^ a by A19, A23, A21, GROUP_2:114;
then consider d being Element of G such that
A25: ((c ") * b) |^ a = d |^ a and
A26: d in H by A24, Th58;
(c ") * b = d by A25, Th16;
hence x = y by A22, A20, A26, GROUP_2:114; ::_thesis: verum
end;
then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by A3, A10, WELLORD2:def_4;
hence Index H = Index (H |^ a) by CARD_1:5; ::_thesis: verum
end;
theorem :: GROUP_3:72
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
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
let a be Element of G; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite holds
index H = index (H |^ a)
let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite implies index H = index (H |^ a) )
assume A1: Left_Cosets H is finite ; ::_thesis: index H = index (H |^ a)
then A2: ex B being finite set st
( B = Left_Cosets H & index H = card B ) by GROUP_2:def_18;
A3: Index H = Index (H |^ a) by Th71;
then Left_Cosets H, Left_Cosets (H |^ a) are_equipotent by CARD_1:5;
then Left_Cosets (H |^ a) is finite by A1, CARD_1:38;
hence index H = index (H |^ a) by A2, A3, GROUP_2:def_18; ::_thesis: verum
end;
theorem Th73: :: GROUP_3:73
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
let G be Group; ::_thesis: ( G is commutative Group implies for H being strict Subgroup of G
for a being Element of G holds H |^ a = H )
assume A1: G is commutative Group ; ::_thesis: for H being strict Subgroup of G
for a being Element of G holds H |^ a = H
let H be strict Subgroup of G; ::_thesis: for a being Element of G holds H |^ a = H
let a be Element of G; ::_thesis: H |^ a = H
the carrier of (H |^ a) = ((a ") * H) * a by Th59
.= (H * (a ")) * a by A1, GROUP_2:112
.= H * ((a ") * a) by GROUP_2:107
.= H * (1_ G) by GROUP_1:def_5
.= the carrier of H by GROUP_2:109 ;
hence H |^ a = H by GROUP_2:59; ::_thesis: verum
end;
definition
let G be Group;
let a, b be Element of G;
preda,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 Th74: :: GROUP_3:74
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
let G be Group; ::_thesis: for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st b = a |^ g )
let a, b be Element of G; ::_thesis: ( a,b are_conjugated iff ex g being Element of G st b = a |^ g )
thus ( a,b are_conjugated implies ex g being Element of G st b = a |^ g ) ::_thesis: ( ex g being Element of G st b = a |^ g implies a,b are_conjugated )
proof
given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: ex g being Element of G st b = a |^ g
a |^ (g ") = b by A1, Th25;
hence ex g being Element of G st b = a |^ g ; ::_thesis: verum
end;
given g being Element of G such that A2: b = a |^ g ; ::_thesis: a,b are_conjugated
a = b |^ (g ") by A2, Th25;
hence a,b are_conjugated by Def7; ::_thesis: verum
end;
theorem Th75: :: GROUP_3:75
for G being Group
for a being Element of G holds a,a are_conjugated
proof
let G be Group; ::_thesis: for a being Element of G holds a,a are_conjugated
let a be Element of G; ::_thesis: a,a are_conjugated
take 1_ G ; :: according to GROUP_3:def_7 ::_thesis: a = a |^ (1_ G)
thus a = a |^ (1_ G) by Th19; ::_thesis: verum
end;
theorem Th76: :: GROUP_3:76
for G being Group
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
proof
let G be Group; ::_thesis: for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
let a, b be Element of G; ::_thesis: ( a,b are_conjugated implies b,a are_conjugated )
given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: b,a are_conjugated
b = a |^ (g ") by A1, Th25;
hence b,a are_conjugated by Def7; ::_thesis: verum
end;
definition
let G be Group;
let a, b be Element of G;
:: original: are_conjugated
redefine preda,b are_conjugated ;
reflexivity
for a being Element of G holds (G,b1,b1) by Th75;
symmetry
for a, b being Element of G st (G,b1,b2) holds
(G,b2,b1) by Th76;
end;
theorem Th77: :: GROUP_3:77
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
let G be Group; ::_thesis: for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds
a,c are_conjugated
let a, b, c be Element of G; ::_thesis: ( a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated )
given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def_7 ::_thesis: ( not b,c are_conjugated or a,c are_conjugated )
given h being Element of G such that A2: b = c |^ h ; :: according to GROUP_3:def_7 ::_thesis: a,c are_conjugated
a = c |^ (h * g) by A1, A2, Th24;
hence a,c are_conjugated by Def7; ::_thesis: verum
end;
theorem Th78: :: GROUP_3:78
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
let G be Group; ::_thesis: for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds
a = 1_ G
let a be Element of G; ::_thesis: ( ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) implies a = 1_ G )
assume A1: ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) ; ::_thesis: a = 1_ G
now__::_thesis:_a_=_1__G
percases ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) by A1;
suppose a, 1_ G are_conjugated ; ::_thesis: a = 1_ G
then ex g being Element of G st 1_ G = a |^ g by Th74;
hence a = 1_ G by Th18; ::_thesis: verum
end;
suppose 1_ G,a are_conjugated ; ::_thesis: a = 1_ G
then ex g being Element of G st 1_ G = a |^ g by Def7;
hence a = 1_ G by Th18; ::_thesis: verum
end;
end;
end;
hence a = 1_ G ; ::_thesis: verum
end;
theorem Th79: :: GROUP_3:79
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
let G be Group; ::_thesis: for a being Element of G holds a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
let a be Element of G; ::_thesis: a |^ (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }
set A = a |^ (carr ((Omega). G));
set B = { b where b is Element of G : a,b are_conjugated } ;
thus a |^ (carr ((Omega). G)) c= { b where b is Element of G : a,b are_conjugated } :: according to XBOOLE_0:def_10 ::_thesis: { b where b is Element of G : a,b are_conjugated } c= a |^ (carr ((Omega). G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a |^ (carr ((Omega). G)) or x in { b where b is Element of G : a,b are_conjugated } )
assume A1: x in a |^ (carr ((Omega). G)) ; ::_thesis: x in { b where b is Element of G : a,b are_conjugated }
then reconsider b = x as Element of G ;
ex g being Element of G st
( x = a |^ g & g in carr ((Omega). G) ) by A1, Th42;
then b,a are_conjugated by Def7;
hence x in { b where b is Element of G : a,b are_conjugated } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of G : a,b are_conjugated } or x in a |^ (carr ((Omega). G)) )
assume x in { b where b is Element of G : a,b are_conjugated } ; ::_thesis: x in a |^ (carr ((Omega). G))
then consider b being Element of G such that
A2: x = b and
A3: a,b are_conjugated ;
ex g being Element of G st b = a |^ g by A3, Def7;
hence x in a |^ (carr ((Omega). G)) by A2, Th42; ::_thesis: verum
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 Th80: :: GROUP_3:80
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
let x be set ; ::_thesis: 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 ) )
let G be Group; ::_thesis: 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 ) )
let a be Element of G; ::_thesis: ( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
thus ( x in con_class a implies ex b being Element of G st
( b = x & a,b are_conjugated ) ) ::_thesis: ( ex b being Element of G st
( b = x & a,b are_conjugated ) implies x in con_class a )
proof
assume x in con_class a ; ::_thesis: ex b being Element of G st
( b = x & a,b are_conjugated )
then x in { b where b is Element of G : a,b are_conjugated } by Th79;
hence ex b being Element of G st
( b = x & a,b are_conjugated ) ; ::_thesis: verum
end;
given b being Element of G such that A1: ( b = x & a,b are_conjugated ) ; ::_thesis: x in con_class a
x in { c where c is Element of G : a,c are_conjugated } by A1;
hence x in con_class a by Th79; ::_thesis: verum
end;
theorem Th81: :: GROUP_3:81
for G being Group
for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )
let a, b be Element of G; ::_thesis: ( a in con_class b iff a,b are_conjugated )
thus ( a in con_class b implies a,b are_conjugated ) ::_thesis: ( a,b are_conjugated implies a in con_class b )
proof
assume a in con_class b ; ::_thesis: a,b are_conjugated
then ex c being Element of G st
( a = c & b,c are_conjugated ) by Th80;
hence a,b are_conjugated ; ::_thesis: verum
end;
assume a,b are_conjugated ; ::_thesis: a in con_class b
hence a in con_class b by Th80; ::_thesis: verum
end;
theorem Th82: :: GROUP_3:82
for G being Group
for a, g being Element of G holds a |^ g in con_class a
proof
let G be Group; ::_thesis: for a, g being Element of G holds a |^ g in con_class a
let a, g be Element of G; ::_thesis: a |^ g in con_class a
a,a |^ g are_conjugated by Th74;
hence a |^ g in con_class a by Th80; ::_thesis: verum
end;
theorem :: GROUP_3:83
for G being Group
for a being Element of G holds a in con_class a by Th81;
theorem :: GROUP_3:84
for G being Group
for a, b being Element of G st a in con_class b holds
b in con_class a
proof
let G be Group; ::_thesis: for a, b being Element of G st a in con_class b holds
b in con_class a
let a, b be Element of G; ::_thesis: ( a in con_class b implies b in con_class a )
assume a in con_class b ; ::_thesis: b in con_class a
then a,b are_conjugated by Th81;
hence b in con_class a by Th81; ::_thesis: verum
end;
theorem :: GROUP_3:85
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
let G be Group; ::_thesis: for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
let a, b be Element of G; ::_thesis: ( con_class a = con_class b iff con_class a meets con_class b )
thus ( con_class a = con_class b implies con_class a meets con_class b ) ::_thesis: ( con_class a meets con_class b implies con_class a = con_class b )
proof
assume A1: con_class a = con_class b ; ::_thesis: con_class a meets con_class b
a in con_class a by Th81;
hence con_class a meets con_class b by A1, XBOOLE_0:3; ::_thesis: verum
end;
assume con_class a meets con_class b ; ::_thesis: con_class a = con_class b
then consider x being set such that
A2: x in con_class a and
A3: x in con_class b by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
A4: a,x are_conjugated by A2, Th81;
thus con_class a c= con_class b :: according to XBOOLE_0:def_10 ::_thesis: con_class b c= con_class a
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class a or y in con_class b )
assume y in con_class a ; ::_thesis: y in con_class b
then consider g being Element of G such that
A5: g = y and
A6: a,g are_conjugated by Th80;
A7: b,x are_conjugated by A3, Th81;
x,a are_conjugated by A2, Th81;
then x,g are_conjugated by A6, Th77;
then b,g are_conjugated by A7, Th77;
hence y in con_class b by A5, Th80; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class b or y in con_class a )
assume y in con_class b ; ::_thesis: y in con_class a
then consider g being Element of G such that
A8: g = y and
A9: b,g are_conjugated by Th80;
x,b are_conjugated by A3, Th81;
then x,g are_conjugated by A9, Th77;
then a,g are_conjugated by A4, Th77;
hence y in con_class a by A8, Th80; ::_thesis: verum
end;
theorem :: GROUP_3:86
for G being Group
for a being Element of G holds
( con_class a = {(1_ G)} iff a = 1_ G )
proof
let G be Group; ::_thesis: for a being Element of G holds
( con_class a = {(1_ G)} iff a = 1_ G )
let a be Element of G; ::_thesis: ( con_class a = {(1_ G)} iff a = 1_ G )
thus ( con_class a = {(1_ G)} implies a = 1_ G ) ::_thesis: ( a = 1_ G implies con_class a = {(1_ G)} )
proof
assume A1: con_class a = {(1_ G)} ; ::_thesis: a = 1_ G
a in con_class a by Th81;
hence a = 1_ G by A1, TARSKI:def_1; ::_thesis: verum
end;
assume A2: a = 1_ G ; ::_thesis: con_class a = {(1_ G)}
thus con_class a c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= con_class a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class a or x in {(1_ G)} )
assume x in con_class a ; ::_thesis: x in {(1_ G)}
then consider b being Element of G such that
A3: b = x and
A4: a,b are_conjugated by Th80;
b = 1_ G by A2, A4, Th78;
hence x in {(1_ G)} by A3, TARSKI:def_1; ::_thesis: verum
end;
1_ G in con_class a by A2, Th81;
hence {(1_ G)} c= con_class a by ZFMISC_1:31; ::_thesis: verum
end;
theorem :: GROUP_3:87
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
let G be Group; ::_thesis: for a being Element of G
for A being Subset of G holds (con_class a) * A = A * (con_class a)
let a be Element of G; ::_thesis: for A being Subset of G holds (con_class a) * A = A * (con_class a)
let A be Subset of G; ::_thesis: (con_class a) * A = A * (con_class a)
thus (con_class a) * A c= A * (con_class a) :: according to XBOOLE_0:def_10 ::_thesis: A * (con_class a) c= (con_class a) * A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (con_class a) * A or x in A * (con_class a) )
assume x in (con_class a) * A ; ::_thesis: x in A * (con_class a)
then consider b, c being Element of G such that
A1: x = b * c and
A2: b in con_class a and
A3: c in A ;
reconsider h = x as Element of G by A1;
b,a are_conjugated by A2, Th81;
then consider g being Element of G such that
A4: b = a |^ g by Def7;
h |^ (c ") = (c * ((a |^ g) * c)) * (c ") by A1, A4
.= c * (((a |^ g) * c) * (c ")) by GROUP_1:def_3
.= c * (a |^ g) by Th1 ;
then A5: x = (c * (a |^ g)) |^ c by Th25
.= (c |^ c) * ((a |^ g) |^ c) by Th23
.= c * ((a |^ g) |^ c) by Th20
.= c * (a |^ (g * c)) by Th24 ;
a |^ (g * c) in con_class a by Th82;
hence x in A * (con_class a) by A3, A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (con_class a) or x in (con_class a) * A )
assume x in A * (con_class a) ; ::_thesis: x in (con_class a) * A
then consider b, c being Element of G such that
A6: x = b * c and
A7: b in A and
A8: c in con_class a ;
reconsider h = x as Element of G by A6;
c,a are_conjugated by A8, Th81;
then consider g being Element of G such that
A9: c = a |^ g by Def7;
h |^ b = (a |^ g) * b by A6, A9, Th1;
then A10: x = ((a |^ g) * b) |^ (b ") by Th25
.= ((a |^ g) |^ (b ")) * (b |^ (b ")) by Th23
.= (a |^ (g * (b "))) * (b |^ (b ")) by Th24
.= (a |^ (g * (b "))) * b by Th1 ;
a |^ (g * (b ")) in con_class a by Th82;
hence x in (con_class a) * A by A7, A10; ::_thesis: verum
end;
definition
let G be Group;
let A, B be Subset of G;
predA,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 Th88: :: GROUP_3:88
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
let G be Group; ::_thesis: for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st B = A |^ g )
let A, B be Subset of G; ::_thesis: ( A,B are_conjugated iff ex g being Element of G st B = A |^ g )
thus ( A,B are_conjugated implies ex g being Element of G st B = A |^ g ) ::_thesis: ( ex g being Element of G st B = A |^ g implies A,B are_conjugated )
proof
given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: ex g being Element of G st B = A |^ g
A |^ (g ") = B by A1, Th54;
hence ex g being Element of G st B = A |^ g ; ::_thesis: verum
end;
given g being Element of G such that A2: B = A |^ g ; ::_thesis: A,B are_conjugated
A = B |^ (g ") by A2, Th54;
hence A,B are_conjugated by Def9; ::_thesis: verum
end;
theorem Th89: :: GROUP_3:89
for G being Group
for A being Subset of G holds A,A are_conjugated
proof
let G be Group; ::_thesis: for A being Subset of G holds A,A are_conjugated
let A be Subset of G; ::_thesis: A,A are_conjugated
take 1_ G ; :: according to GROUP_3:def_9 ::_thesis: A = A |^ (1_ G)
thus A = A |^ (1_ G) by Th52; ::_thesis: verum
end;
theorem Th90: :: GROUP_3:90
for G being Group
for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
proof
let G be Group; ::_thesis: for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
let A, B be Subset of G; ::_thesis: ( A,B are_conjugated implies B,A are_conjugated )
given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: B,A are_conjugated
B = A |^ (g ") by A1, Th54;
hence B,A are_conjugated by Def9; ::_thesis: verum
end;
definition
let G be Group;
let A, B be Subset of G;
:: original: are_conjugated
redefine predA,B are_conjugated ;
reflexivity
for A being Subset of G holds (G,b1,b1) by Th89;
symmetry
for A, B being Subset of G st (G,b1,b2) holds
(G,b2,b1) by Th90;
end;
theorem Th91: :: GROUP_3:91
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
let G be Group; ::_thesis: for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds
A,C are_conjugated
let A, B, C be Subset of G; ::_thesis: ( A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated )
given g being Element of G such that A1: A = B |^ g ; :: according to GROUP_3:def_9 ::_thesis: ( not B,C are_conjugated or A,C are_conjugated )
given h being Element of G such that A2: B = C |^ h ; :: according to GROUP_3:def_9 ::_thesis: A,C are_conjugated
A = C |^ (h * g) by A1, A2, Th47;
hence A,C are_conjugated by Def9; ::_thesis: verum
end;
theorem Th92: :: GROUP_3:92
for G being Group
for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
let a, b be Element of G; ::_thesis: ( {a},{b} are_conjugated iff a,b are_conjugated )
thus ( {a},{b} are_conjugated implies a,b are_conjugated ) ::_thesis: ( a,b are_conjugated implies {a},{b} are_conjugated )
proof
assume {a},{b} are_conjugated ; ::_thesis: a,b are_conjugated
then consider g being Element of G such that
A1: {a} |^ g = {b} by Th88;
{b} = {(a |^ g)} by A1, Th37;
then b = a |^ g by ZFMISC_1:3;
hence a,b are_conjugated by Th74; ::_thesis: verum
end;
assume a,b are_conjugated ; ::_thesis: {a},{b} are_conjugated
then consider g being Element of G such that
A2: a |^ g = b by Th74;
{b} = {a} |^ g by A2, Th37;
hence {a},{b} are_conjugated by Th88; ::_thesis: verum
end;
theorem Th93: :: GROUP_3:93
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
let G be Group; ::_thesis: 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
let A be Subset of G; ::_thesis: 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
let H1 be Subgroup of G; ::_thesis: ( A, carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A )
assume A, carr H1 are_conjugated ; ::_thesis: ex H2 being strict Subgroup of G st the carrier of H2 = A
then consider g being Element of G such that
A1: A = (carr H1) |^ g by Def9;
A = the carrier of (H1 |^ g) by A1, Def6;
hence ex H2 being strict Subgroup of G st the carrier of H2 = A ; ::_thesis: verum
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
set X = { B where B is Subset of G : A,B are_conjugated } ;
{ B where B is Subset of G : A,B are_conjugated } c= bool the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of G : A,B are_conjugated } or x in bool the carrier of G )
assume x in { B where B is Subset of G : A,B are_conjugated } ; ::_thesis: x in bool the carrier of G
then ex B being Subset of G st
( x = B & A,B are_conjugated ) ;
hence x in bool the carrier of G ; ::_thesis: verum
end;
hence { B where B is Subset of G : A,B are_conjugated } is Subset-Family of G ; ::_thesis: verum
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:94
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 Th95: :: GROUP_3:95
for G being Group
for A, B being Subset of G holds
( A in con_class B iff A,B are_conjugated )
proof
let G be Group; ::_thesis: for A, B being Subset of G holds
( A in con_class B iff A,B are_conjugated )
let A, B be Subset of G; ::_thesis: ( A in con_class B iff A,B are_conjugated )
thus ( A in con_class B implies A,B are_conjugated ) ::_thesis: ( A,B are_conjugated implies A in con_class B )
proof
assume A in con_class B ; ::_thesis: A,B are_conjugated
then ex C being Subset of G st
( A = C & B,C are_conjugated ) ;
hence A,B are_conjugated ; ::_thesis: verum
end;
assume A,B are_conjugated ; ::_thesis: A in con_class B
hence A in con_class B ; ::_thesis: verum
end;
theorem :: GROUP_3:96
for G being Group
for g being Element of G
for A being Subset of G holds A |^ g in con_class A
proof
let G be Group; ::_thesis: for g being Element of G
for A being Subset of G holds A |^ g in con_class A
let g be Element of G; ::_thesis: for A being Subset of G holds A |^ g in con_class A
let A be Subset of G; ::_thesis: A |^ g in con_class A
A,A |^ g are_conjugated by Th88;
hence A |^ g in con_class A ; ::_thesis: verum
end;
theorem :: GROUP_3:97
for G being Group
for A being Subset of G holds A in con_class A ;
theorem :: GROUP_3:98
for G being Group
for A, B being Subset of G st A in con_class B holds
B in con_class A
proof
let G be Group; ::_thesis: for A, B being Subset of G st A in con_class B holds
B in con_class A
let A, B be Subset of G; ::_thesis: ( A in con_class B implies B in con_class A )
assume A in con_class B ; ::_thesis: B in con_class A
then A,B are_conjugated by Th95;
hence B in con_class A ; ::_thesis: verum
end;
theorem :: GROUP_3:99
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
let G be Group; ::_thesis: for A, B being Subset of G holds
( con_class A = con_class B iff con_class A meets con_class B )
let A, B be Subset of G; ::_thesis: ( con_class A = con_class B iff con_class A meets con_class B )
thus ( con_class A = con_class B implies con_class A meets con_class B ) ::_thesis: ( con_class A meets con_class B implies con_class A = con_class B )
proof
A1: A in con_class A ;
assume con_class A = con_class B ; ::_thesis: con_class A meets con_class B
hence con_class A meets con_class B by A1, XBOOLE_0:3; ::_thesis: verum
end;
assume con_class A meets con_class B ; ::_thesis: con_class A = con_class B
then consider x being set such that
A2: x in con_class A and
A3: x in con_class B by XBOOLE_0:3;
reconsider x = x as Subset of G by A2;
A4: A,x are_conjugated by A2, Th95;
thus con_class A c= con_class B :: according to XBOOLE_0:def_10 ::_thesis: con_class B c= con_class A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class A or y in con_class B )
assume y in con_class A ; ::_thesis: y in con_class B
then consider C being Subset of G such that
A5: C = y and
A6: A,C are_conjugated ;
A7: B,x are_conjugated by A3, Th95;
x,A are_conjugated by A2, Th95;
then x,C are_conjugated by A6, Th91;
then B,C are_conjugated by A7, Th91;
hence y in con_class B by A5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class B or y in con_class A )
assume y in con_class B ; ::_thesis: y in con_class A
then consider C being Subset of G such that
A8: C = y and
A9: B,C are_conjugated ;
x,B are_conjugated by A3, Th95;
then x,C are_conjugated by A9, Th91;
then A,C are_conjugated by A4, Th91;
hence y in con_class A by A8; ::_thesis: verum
end;
theorem Th100: :: GROUP_3:100
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
let G be Group; ::_thesis: for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }
let a be Element of G; ::_thesis: con_class {a} = { {b} where b is Element of G : b in con_class a }
set A = { {b} where b is Element of G : b in con_class a } ;
thus con_class {a} c= { {b} where b is Element of G : b in con_class a } :: according to XBOOLE_0:def_10 ::_thesis: { {b} where b is Element of G : b in con_class a } c= con_class {a}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class {a} or x in { {b} where b is Element of G : b in con_class a } )
assume x in con_class {a} ; ::_thesis: x in { {b} where b is Element of G : b in con_class a }
then consider B being Subset of G such that
A1: x = B and
A2: {a},B are_conjugated ;
consider b being Element of G such that
A3: {a} |^ b = B by A2, Th88;
a,a |^ b are_conjugated by Th74;
then A4: a |^ b in con_class a by Th81;
B = {(a |^ b)} by A3, Th37;
hence x in { {b} where b is Element of G : b in con_class a } by A1, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {b} where b is Element of G : b in con_class a } or x in con_class {a} )
assume x in { {b} where b is Element of G : b in con_class a } ; ::_thesis: x in con_class {a}
then consider b being Element of G such that
A5: x = {b} and
A6: b in con_class a ;
b,a are_conjugated by A6, Th81;
then {b},{a} are_conjugated by Th92;
hence x in con_class {a} by A5; ::_thesis: verum
end;
theorem :: GROUP_3:101
for G being Group
for A being Subset of G st G is finite holds
con_class A is finite ;
definition
let G be Group;
let H1, H2 be Subgroup of G;
predH1,H2 are_conjugated means :Def11: :: GROUP_3:def 11
ex g being Element of G st multMagma(# the carrier of H1, the multF 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 multMagma(# the carrier of H1, the multF 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 Th102: :: GROUP_3:102
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
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
thus ( H1,H2 are_conjugated implies ex g being Element of G st H2 = H1 |^ g ) ::_thesis: ( ex g being Element of G st H2 = H1 |^ g implies H1,H2 are_conjugated )
proof
given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: ex g being Element of G st H2 = H1 |^ g
H1 |^ (g ") = H2 by A1, Th62;
hence ex g being Element of G st H2 = H1 |^ g ; ::_thesis: verum
end;
given g being Element of G such that A2: H2 = H1 |^ g ; ::_thesis: H1,H2 are_conjugated
H1 = H2 |^ (g ") by A2, Th62;
hence H1,H2 are_conjugated by Def11; ::_thesis: verum
end;
theorem Th103: :: GROUP_3:103
for G being Group
for H1 being strict Subgroup of G holds H1,H1 are_conjugated
proof
let G be Group; ::_thesis: for H1 being strict Subgroup of G holds H1,H1 are_conjugated
let H1 be strict Subgroup of G; ::_thesis: H1,H1 are_conjugated
take 1_ G ; :: according to GROUP_3:def_11 ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G)
thus multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G) by Th61; ::_thesis: verum
end;
theorem Th104: :: GROUP_3:104
for G being Group
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
proof
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated implies H2,H1 are_conjugated )
given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: H2,H1 are_conjugated
H2 = H1 |^ (g ") by A1, Th62;
hence H2,H1 are_conjugated by Def11; ::_thesis: verum
end;
definition
let G be Group;
let H1, H2 be strict Subgroup of G;
:: original: are_conjugated
redefine predH1,H2 are_conjugated ;
reflexivity
for H1 being strict Subgroup of G holds (G,b1,b1) by Th103;
symmetry
for H1, H2 being strict Subgroup of G st (G,b1,b2) holds
(G,b2,b1) by Th104;
end;
theorem Th105: :: GROUP_3:105
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
let G be Group; ::_thesis: 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
let H3 be Subgroup of G; ::_thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated )
given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def_11 ::_thesis: ( not H2,H3 are_conjugated or H1,H3 are_conjugated )
given h being Element of G such that A2: multMagma(# the carrier of H2, the multF of H2 #) = H3 |^ h ; :: according to GROUP_3:def_11 ::_thesis: H1,H3 are_conjugated
H1 = H3 |^ (h * g) by A1, A2, Th60;
hence H1,H3 are_conjugated by Def11; ::_thesis: verum
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
defpred S1[ set ] means ex H1 being strict Subgroup of G st
( $1 = H1 & H,H1 are_conjugated );
consider L being Subset of (Subgroups G) such that
A1: for x being set holds
( x in L iff ( x in Subgroups G & S1[x] ) ) from SUBSET_1:sch_1();
take L ; ::_thesis: for x being set holds
( x in L iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
let x be set ; ::_thesis: ( x in L iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
thus ( x in L implies ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) by A1; ::_thesis: ( ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) implies x in L )
given H1 being strict Subgroup of G such that A2: x = H1 and
A3: H,H1 are_conjugated ; ::_thesis: x in L
x in Subgroups G by A2, Def1;
hence x in L by A1, A2, A3; ::_thesis: verum
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
defpred S1[ set ] means ex H3 being strict Subgroup of G st
( $1 = H3 & H,H3 are_conjugated );
let A1, A2 be Subset of (Subgroups G); ::_thesis: ( ( for x being set holds
( x in A1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being set holds
( x in A2 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) implies A1 = A2 )
assume A4: for x being set holds
( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st
( ( x in A2 implies ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) implies ( ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) & not x in A2 ) ) or A1 = A2 )
assume A5: for x being set holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
thus A1 = A2 from XBOOLE_0:sch_2(A4, A5); ::_thesis: verum
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 Th106: :: GROUP_3:106
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
let x be set ; ::_thesis: for G being Group
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
let G be Group; ::_thesis: for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
let H be Subgroup of G; ::_thesis: ( x in con_class H implies x is strict Subgroup of G )
assume x in con_class H ; ::_thesis: x is strict Subgroup of G
then ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) by Def12;
hence x is strict Subgroup of G ; ::_thesis: verum
end;
theorem Th107: :: GROUP_3:107
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 in con_class H2 iff H1,H2 are_conjugated )
proof
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds
( H1 in con_class H2 iff H1,H2 are_conjugated )
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1 in con_class H2 iff H1,H2 are_conjugated )
thus ( H1 in con_class H2 implies H1,H2 are_conjugated ) ::_thesis: ( H1,H2 are_conjugated implies H1 in con_class H2 )
proof
assume H1 in con_class H2 ; ::_thesis: H1,H2 are_conjugated
then ex H3 being strict Subgroup of G st
( H1 = H3 & H2,H3 are_conjugated ) by Def12;
hence H1,H2 are_conjugated ; ::_thesis: verum
end;
assume H1,H2 are_conjugated ; ::_thesis: H1 in con_class H2
hence H1 in con_class H2 by Def12; ::_thesis: verum
end;
theorem Th108: :: GROUP_3:108
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
let G be Group; ::_thesis: for g being Element of G
for H being strict Subgroup of G holds H |^ g in con_class H
let g be Element of G; ::_thesis: for H being strict Subgroup of G holds H |^ g in con_class H
let H be strict Subgroup of G; ::_thesis: H |^ g in con_class H
H,H |^ g are_conjugated by Th102;
hence H |^ g in con_class H by Def12; ::_thesis: verum
end;
theorem Th109: :: GROUP_3:109
for G being Group
for H being strict Subgroup of G holds H in con_class H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds H in con_class H
let H be strict Subgroup of G; ::_thesis: H in con_class H
H,H are_conjugated ;
hence H in con_class H by Def12; ::_thesis: verum
end;
theorem :: GROUP_3:110
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
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds
H2 in con_class H1
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1 in con_class H2 implies H2 in con_class H1 )
assume H1 in con_class H2 ; ::_thesis: H2 in con_class H1
then H1,H2 are_conjugated by Th107;
hence H2 in con_class H1 by Th107; ::_thesis: verum
end;
theorem :: GROUP_3:111
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
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
let H1, H2 be strict Subgroup of G; ::_thesis: ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
thus ( con_class H1 = con_class H2 implies con_class H1 meets con_class H2 ) ::_thesis: ( con_class H1 meets con_class H2 implies con_class H1 = con_class H2 )
proof
assume A1: con_class H1 = con_class H2 ; ::_thesis: con_class H1 meets con_class H2
H1 in con_class H1 by Th109;
hence con_class H1 meets con_class H2 by A1, XBOOLE_0:3; ::_thesis: verum
end;
assume con_class H1 meets con_class H2 ; ::_thesis: con_class H1 = con_class H2
then consider x being set such that
A2: x in con_class H1 and
A3: x in con_class H2 by XBOOLE_0:3;
reconsider x = x as strict Subgroup of G by A2, Th106;
A4: H1,x are_conjugated by A2, Th107;
thus con_class H1 c= con_class H2 :: according to XBOOLE_0:def_10 ::_thesis: con_class H2 c= con_class H1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class H1 or y in con_class H2 )
assume y in con_class H1 ; ::_thesis: y in con_class H2
then consider H3 being strict Subgroup of G such that
A5: H3 = y and
A6: H1,H3 are_conjugated by Def12;
A7: H2,x are_conjugated by A3, Th107;
x,H1 are_conjugated by A2, Th107;
then x,H3 are_conjugated by A6, Th105;
then H2,H3 are_conjugated by A7, Th105;
hence y in con_class H2 by A5, Def12; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in con_class H2 or y in con_class H1 )
assume y in con_class H2 ; ::_thesis: y in con_class H1
then consider H3 being strict Subgroup of G such that
A8: H3 = y and
A9: H2,H3 are_conjugated by Def12;
x,H2 are_conjugated by A3, Th107;
then x,H3 are_conjugated by A9, Th105;
then H1,H3 are_conjugated by A4, Th105;
hence y in con_class H1 by A8, Def12; ::_thesis: verum
end;
theorem :: GROUP_3:112
for G being Group
for H being Subgroup of G st G is finite holds
con_class H is finite by Th15, FINSET_1:1;
theorem Th113: :: GROUP_3:113
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
let G be Group; ::_thesis: 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 )
let H2 be Subgroup of G; ::_thesis: for H1 being strict Subgroup of G holds
( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
let H1 be strict Subgroup of G; ::_thesis: ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
thus ( H1,H2 are_conjugated implies carr H1, carr H2 are_conjugated ) ::_thesis: ( carr H1, carr H2 are_conjugated implies H1,H2 are_conjugated )
proof
given a being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ a ; :: according to GROUP_3:def_11 ::_thesis: carr H1, carr H2 are_conjugated
carr H1 = (carr H2) |^ a by A1, Def6;
hence carr H1, carr H2 are_conjugated by Def9; ::_thesis: verum
end;
given a being Element of G such that A2: carr H1 = (carr H2) |^ a ; :: according to GROUP_3:def_9 ::_thesis: H1,H2 are_conjugated
H1 = H2 |^ a by A2, Def6;
hence H1,H2 are_conjugated by Def11; ::_thesis: verum
end;
definition
let G be Group;
let IT be Subgroup of G;
attrIT is normal means :Def13: :: GROUP_3:def 13
for a being Element of G holds IT |^ a = multMagma(# the carrier of IT, the multF 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 = multMagma(# the carrier of IT, the multF of IT #) );
registration
let G be Group;
cluster non empty strict unital Group-like associative normal for Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is strict & b1 is normal )
proof
for a being Element of G holds ((1). G) |^ a = (1). G by Th67;
then (1). G is normal by Def13;
hence ex b1 being Subgroup of G st
( b1 is strict & b1 is normal ) ; ::_thesis: verum
end;
end;
theorem Th114: :: GROUP_3:114
for G being Group holds
( (1). G is normal & (Omega). G is normal )
proof
let G be Group; ::_thesis: ( (1). G is normal & (Omega). G is normal )
thus for a being Element of G holds ((1). G) |^ a = multMagma(# the carrier of ((1). G), the multF of ((1). G) #) by Th67; :: according to GROUP_3:def_13 ::_thesis: (Omega). G is normal
thus for a being Element of G holds ((Omega). G) |^ a = multMagma(# the carrier of ((Omega). G), the multF of ((Omega). G) #) by Th69; :: according to GROUP_3:def_13 ::_thesis: verum
end;
theorem :: GROUP_3:115
for G being Group
for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
proof
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds N1 /\ N2 is normal
let N1, N2 be strict normal Subgroup of G; ::_thesis: N1 /\ N2 is normal
let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: (N1 /\ N2) |^ a = multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #)
thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th63
.= N1 /\ (N2 |^ a) by Def13
.= multMagma(# the carrier of (N1 /\ N2), the multF of (N1 /\ N2) #) by Def13 ; ::_thesis: verum
end;
theorem :: GROUP_3:116
for G being Group
for H being strict Subgroup of G st G is commutative Group holds
H is normal
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st G is commutative Group holds
H is normal
let H be strict Subgroup of G; ::_thesis: ( G is commutative Group implies H is normal )
assume G is commutative Group ; ::_thesis: H is normal
hence for a being Element of G holds H |^ a = multMagma(# the carrier of H, the multF of H #) by Th73; :: according to GROUP_3:def_13 ::_thesis: verum
end;
theorem Th117: :: GROUP_3:117
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
let G be Group; ::_thesis: 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 )
let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds a * H = H * a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a * H = H * a ) ::_thesis: ( ( for a being Element of G holds a * H = H * a ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds a * H = H * a
let a be Element of G; ::_thesis: a * H = H * a
A2: carr (H |^ a) = ((a ") * H) * a by Th59;
carr (H |^ a) = the carrier of multMagma(# the carrier of H, the multF of H #) by A1, Def13
.= carr H ;
hence a * H = (a * ((a ") * H)) * a by A2, GROUP_2:33
.= ((a * (a ")) * H) * a by GROUP_2:105
.= ((1_ G) * H) * a by GROUP_1:def_5
.= H * a by GROUP_2:37 ;
::_thesis: verum
end;
assume A3: for a being Element of G holds a * H = H * a ; ::_thesis: H is normal Subgroup of G
H is normal
proof
let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
the carrier of (H |^ a) = ((a ") * H) * a by Th59
.= (H * (a ")) * a by A3
.= H * ((a ") * a) by GROUP_2:107
.= H * (1_ G) by GROUP_1:def_5
.= the carrier of H by GROUP_2:109 ;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) by GROUP_2:59; ::_thesis: verum
end;
hence H is normal Subgroup of G ; ::_thesis: verum
end;
theorem Th118: :: GROUP_3:118
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
let G be Group; ::_thesis: 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 )
let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds a * H c= H * a )
thus ( H is normal Subgroup of G implies for a being Element of G holds a * H c= H * a ) by Th117; ::_thesis: ( ( for a being Element of G holds a * H c= H * a ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds a * H c= H * a ; ::_thesis: H is normal Subgroup of G
A2: now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H
let a be Element of G; ::_thesis: H * a c= a * H
(a ") * H c= H * (a ") by A1;
then a * ((a ") * H) c= a * (H * (a ")) by Th4;
then (a * (a ")) * H c= a * (H * (a ")) by GROUP_2:105;
then (1_ G) * H c= a * (H * (a ")) by GROUP_1:def_5;
then carr H c= a * (H * (a ")) by GROUP_2:109;
then carr H c= (a * H) * (a ") by GROUP_2:106;
then (carr H) * a c= ((a * H) * (a ")) * a by Th4;
then H * a c= (a * H) * ((a ") * a) by GROUP_2:34;
then H * a c= (a * H) * (1_ G) by GROUP_1:def_5;
hence H * a c= a * H by GROUP_2:37; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a
let a be Element of G; ::_thesis: a * H = H * a
( a * H c= H * a & H * a c= a * H ) by A1, A2;
hence a * H = H * a by XBOOLE_0:def_10; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th117; ::_thesis: verum
end;
theorem Th119: :: GROUP_3:119
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
let G be Group; ::_thesis: 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 )
let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
thus ( H is normal Subgroup of G implies for a being Element of G holds H * a c= a * H ) by Th117; ::_thesis: ( ( for a being Element of G holds H * a c= a * H ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds H * a c= a * H ; ::_thesis: H is normal Subgroup of G
A2: now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_c=_H_*_a
let a be Element of G; ::_thesis: a * H c= H * a
H * (a ") c= (a ") * H by A1;
then a * (H * (a ")) c= a * ((a ") * H) by Th4;
then a * (H * (a ")) c= (a * (a ")) * H by GROUP_2:105;
then a * (H * (a ")) c= (1_ G) * H by GROUP_1:def_5;
then a * (H * (a ")) c= carr H by GROUP_2:109;
then (a * H) * (a ") c= carr H by GROUP_2:106;
then ((a * H) * (a ")) * a c= (carr H) * a by Th4;
then (a * H) * ((a ") * a) c= H * a by GROUP_2:34;
then (a * H) * (1_ G) c= H * a by GROUP_1:def_5;
hence a * H c= H * a by GROUP_2:37; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a
let a be Element of G; ::_thesis: a * H = H * a
( a * H c= H * a & H * a c= a * H ) by A1, A2;
hence a * H = H * a by XBOOLE_0:def_10; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th117; ::_thesis: verum
end;
theorem :: GROUP_3:120
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
let G be Group; ::_thesis: 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 )
let H be Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for A being Subset of G holds A * H = H * A )
thus ( H is normal Subgroup of G implies for A being Subset of G holds A * H = H * A ) ::_thesis: ( ( for A being Subset of G holds A * H = H * A ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: for A being Subset of G holds A * H = H * A
let A be Subset of G; ::_thesis: A * H = H * A
thus A * H c= H * A :: according to XBOOLE_0:def_10 ::_thesis: H * A c= A * H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * H or x in H * A )
assume x in A * H ; ::_thesis: x in H * A
then consider a, h being Element of G such that
A2: x = a * h and
A3: a in A and
A4: h in H by GROUP_2:94;
x in a * H by A2, A4, GROUP_2:103;
then x in H * a by A1, Th117;
then ex g being Element of G st
( x = g * a & g in H ) by GROUP_2:104;
hence x in H * A by A3, GROUP_2:95; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * A or x in A * H )
assume x in H * A ; ::_thesis: x in A * H
then consider h, a being Element of G such that
A5: ( x = h * a & h in H ) and
A6: a in A by GROUP_2:95;
x in H * a by A5, GROUP_2:104;
then x in a * H by A1, Th117;
then ex g being Element of G st
( x = a * g & g in H ) by GROUP_2:103;
hence x in A * H by A6, GROUP_2:94; ::_thesis: verum
end;
assume A7: for A being Subset of G holds A * H = H * A ; ::_thesis: H is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a
let a be Element of G; ::_thesis: a * H = H * a
thus a * H = {a} * H
.= H * {a} by A7
.= H * a ; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th117; ::_thesis: verum
end;
theorem :: GROUP_3:121
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
let G be Group; ::_thesis: 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 )
let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H |^ a )
thus ( H is normal Subgroup of G implies for a being Element of G holds H is Subgroup of H |^ a ) ::_thesis: ( ( for a being Element of G holds H is Subgroup of H |^ a ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds H is Subgroup of H |^ a
let a be Element of G; ::_thesis: H is Subgroup of H |^ a
H |^ a = multMagma(# the carrier of H, the multF of H #) by A1, Def13;
hence H is Subgroup of H |^ a by GROUP_2:54; ::_thesis: verum
end;
assume A2: for a being Element of G holds H is Subgroup of H |^ a ; ::_thesis: H is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H
let a be Element of G; ::_thesis: H * a c= a * H
A3: (H |^ (a ")) * a = ((((a ") ") * H) * (a ")) * a by Th59
.= (((a ") ") * H) * ((a ") * a) by GROUP_2:34
.= (((a ") ") * H) * (1_ G) by GROUP_1:def_5
.= ((a ") ") * H by GROUP_2:37
.= a * H ;
H is Subgroup of H |^ (a ") by A2;
hence H * a c= a * H by A3, Th6; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th119; ::_thesis: verum
end;
theorem :: GROUP_3:122
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
let G be Group; ::_thesis: 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 )
let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G holds H |^ a is Subgroup of H )
thus ( H is normal Subgroup of G implies for a being Element of G holds H |^ a is Subgroup of H ) ::_thesis: ( ( for a being Element of G holds H |^ a is Subgroup of H ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G holds H |^ a is Subgroup of H
let a be Element of G; ::_thesis: H |^ a is Subgroup of H
H |^ a = multMagma(# the carrier of H, the multF of H #) by A1, Def13;
hence H |^ a is Subgroup of H by GROUP_2:54; ::_thesis: verum
end;
assume A2: for a being Element of G holds H |^ a is Subgroup of H ; ::_thesis: H is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_c=_H_*_a
let a be Element of G; ::_thesis: a * H c= H * a
A3: (H |^ (a ")) * a = ((((a ") ") * H) * (a ")) * a by Th59
.= (((a ") ") * H) * ((a ") * a) by GROUP_2:34
.= (((a ") ") * H) * (1_ G) by GROUP_1:def_5
.= ((a ") ") * H by GROUP_2:37
.= a * H ;
H |^ (a ") is Subgroup of H by A2;
hence a * H c= H * a by A3, Th6; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th118; ::_thesis: verum
end;
theorem :: GROUP_3:123
for G being Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff con_class H = {H} )
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff con_class H = {H} )
let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff con_class H = {H} )
thus ( H is normal Subgroup of G implies con_class H = {H} ) ::_thesis: ( con_class H = {H} implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: con_class H = {H}
thus con_class H c= {H} :: according to XBOOLE_0:def_10 ::_thesis: {H} c= con_class H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class H or x in {H} )
assume x in con_class H ; ::_thesis: x in {H}
then consider H1 being strict Subgroup of G such that
A2: x = H1 and
A3: H,H1 are_conjugated by Def12;
ex g being Element of G st H1 = H |^ g by A3, Th102;
then x = H by A1, A2, Def13;
hence x in {H} by TARSKI:def_1; ::_thesis: verum
end;
H in con_class H by Th109;
hence {H} c= con_class H by ZFMISC_1:31; ::_thesis: verum
end;
assume A4: con_class H = {H} ; ::_thesis: H is normal Subgroup of G
H is normal
proof
let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
H |^ a in con_class H by Th108;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) by A4, TARSKI:def_1; ::_thesis: verum
end;
hence H is normal Subgroup of G ; ::_thesis: verum
end;
theorem :: GROUP_3:124
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
let G be Group; ::_thesis: 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 )
let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff for a being Element of G st a in H holds
con_class a c= carr H )
thus ( H is normal Subgroup of G implies for a being Element of G st a in H holds
con_class a c= carr H ) ::_thesis: ( ( for a being Element of G st a in H holds
con_class a c= carr H ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: for a being Element of G st a in H holds
con_class a c= carr H
let a be Element of G; ::_thesis: ( a in H implies con_class a c= carr H )
assume A2: a in H ; ::_thesis: con_class a c= carr H
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class a or x in carr H )
assume x in con_class a ; ::_thesis: x in carr H
then consider b being Element of G such that
A3: x = b and
A4: a,b are_conjugated by Th80;
consider c being Element of G such that
A5: b = a |^ c by A4, Th74;
x in H |^ c by A2, A3, A5, Th58;
then x in H by A1, Def13;
hence x in carr H by STRUCT_0:def_5; ::_thesis: verum
end;
assume A6: for a being Element of G st a in H holds
con_class a c= carr H ; ::_thesis: H is normal Subgroup of G
H is normal
proof
let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
H |^ a = H
proof
let b be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not b in H |^ a or b in H ) & ( not b in H or b in H |^ a ) )
thus ( b in H |^ a implies b in H ) ::_thesis: ( not b in H or b in H |^ a )
proof
assume b in H |^ a ; ::_thesis: b in H
then consider c being Element of G such that
A7: ( b = c |^ a & c in H ) by Th58;
( b in con_class c & con_class c c= carr H ) by A6, A7, Th82;
hence b in H by STRUCT_0:def_5; ::_thesis: verum
end;
assume b in H ; ::_thesis: b in H |^ a
then A8: con_class b c= carr H by A6;
b |^ (a ") in con_class b by Th82;
then b |^ (a ") in H by A8, STRUCT_0:def_5;
then (b |^ (a ")) |^ a in H |^ a by Th58;
hence b in H |^ a by Th25; ::_thesis: verum
end;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; ::_thesis: verum
end;
hence H is normal Subgroup of G ; ::_thesis: verum
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
let G be Group; ::_thesis: 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)
let N2 be normal Subgroup of G; ::_thesis: for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)
let N1 be strict normal Subgroup of G; ::_thesis: (carr N1) * (carr N2) c= (carr N2) * (carr N1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr N1) * (carr N2) or x in (carr N2) * (carr N1) )
assume x in (carr N1) * (carr N2) ; ::_thesis: x in (carr N2) * (carr N1)
then consider a, b being Element of G such that
A1: x = a * b and
A2: a in carr N1 and
A3: b in carr N2 ;
a in N1 by A2, STRUCT_0:def_5;
then a |^ b in N1 |^ b by Th58;
then a |^ b in multMagma(# the carrier of N1, the multF of N1 #) by Def13;
then A4: a |^ b in carr N1 by STRUCT_0:def_5;
b * (a |^ b) = b * ((b ") * (a * b)) by GROUP_1:def_3
.= a * b by Th1 ;
hence x in (carr N2) * (carr N1) by A1, A3, A4; ::_thesis: verum
end;
theorem Th125: :: GROUP_3:125
for G being Group
for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)
proof
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds (carr N1) * (carr N2) = (carr N2) * (carr N1)
let N1, N2 be strict normal Subgroup of G; ::_thesis: (carr N1) * (carr N2) = (carr N2) * (carr N1)
( (carr N1) * (carr N2) c= (carr N2) * (carr N1) & (carr N2) * (carr N1) c= (carr N1) * (carr N2) ) by Lm5;
hence (carr N1) * (carr N2) = (carr N2) * (carr N1) by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: GROUP_3:126
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
let G be Group; ::_thesis: 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)
let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2)
set A = (carr N1) * (carr N2);
set B = carr N1;
set C = carr N2;
(carr N1) * (carr N2) = (carr N2) * (carr N1) by Th125;
then consider H being strict Subgroup of G such that
A1: the carrier of H = (carr N1) * (carr N2) by GROUP_2:78;
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_H_=_H_*_a
let a be Element of G; ::_thesis: a * H = H * a
thus a * H = (a * N1) * (carr N2) by A1, GROUP_2:29
.= (N1 * a) * (carr N2) by Th117
.= (carr N1) * (a * N2) by GROUP_2:30
.= (carr N1) * (N2 * a) by Th117
.= H * a by A1, GROUP_2:31 ; ::_thesis: verum
end;
then H is normal Subgroup of G by Th117;
hence ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) by A1; ::_thesis: verum
end;
theorem :: GROUP_3:127
for G being Group
for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
proof
let G be Group; ::_thesis: for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N
let N be normal Subgroup of G; ::_thesis: Left_Cosets N = Right_Cosets N
thus Left_Cosets N c= Right_Cosets N :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets N c= Left_Cosets N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets N or x in Right_Cosets N )
assume x in Left_Cosets N ; ::_thesis: x in Right_Cosets N
then consider a being Element of G such that
A1: x = a * N by GROUP_2:def_15;
x = N * a by A1, Th117;
hence x in Right_Cosets N by GROUP_2:def_16; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets N or x in Left_Cosets N )
assume x in Right_Cosets N ; ::_thesis: x in Left_Cosets N
then consider a being Element of G such that
A2: x = N * a by GROUP_2:def_16;
x = a * N by A2, Th117;
hence x in Left_Cosets N by GROUP_2:def_15; ::_thesis: verum
end;
theorem :: GROUP_3:128
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
let G be Group; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds
H is normal Subgroup of G
let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G )
assume that
A1: Left_Cosets H is finite and
A2: index H = 2 ; ::_thesis: H is normal Subgroup of G
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:146;
then consider x, y being set such that
A3: x <> y and
A4: Left_Cosets H = {x,y} by A2, CARD_2:60;
carr H in Left_Cosets H by GROUP_2:135;
then ( {x,y} = {x,(carr H)} or {x,y} = {(carr H),y} ) by A4, TARSKI:def_2;
then consider z3 being set such that
A5: {x,y} = {(carr H),z3} ;
A6: carr H misses z3
proof
z3 in Left_Cosets H by A4, A5, TARSKI:def_2;
then A7: ex a being Element of G st z3 = a * H by GROUP_2:def_15;
A8: carr H = (1_ G) * H by GROUP_2:109;
assume not carr H misses z3 ; ::_thesis: contradiction
then carr H = z3 by A7, A8, GROUP_2:115;
then A9: {x,y} = {(carr H)} by A5, ENUMSET1:29;
then x = carr H by ZFMISC_1:4;
hence contradiction by A3, A9, ZFMISC_1:4; ::_thesis: verum
end;
( union (Left_Cosets H) = the carrier of G & union (Left_Cosets H) = (carr H) \/ z3 ) by A4, A5, GROUP_2:137, ZFMISC_1:75;
then A10: ( union (Right_Cosets H) = the carrier of G & z3 = the carrier of G \ (carr H) ) by A6, GROUP_2:137, XBOOLE_1:88;
ex C being finite set st
( C = Right_Cosets H & index H = card C ) by A1, GROUP_2:146;
then consider z1, z2 being set such that
A11: z1 <> z2 and
A12: Right_Cosets H = {z1,z2} by A2, CARD_2:60;
carr H in Right_Cosets H by GROUP_2:135;
then ( {z1,z2} = {z1,(carr H)} or {z1,z2} = {(carr H),z2} ) by A12, TARSKI:def_2;
then consider z4 being set such that
A13: {z1,z2} = {(carr H),z4} ;
A14: carr H misses z4
proof
z4 in Right_Cosets H by A12, A13, TARSKI:def_2;
then A15: ex a being Element of G st z4 = H * a by GROUP_2:def_16;
A16: carr H = H * (1_ G) by GROUP_2:109;
assume not carr H misses z4 ; ::_thesis: contradiction
then carr H = z4 by A15, A16, GROUP_2:121;
then A17: {z1,z2} = {(carr H)} by A13, ENUMSET1:29;
then z1 = carr H by ZFMISC_1:4;
hence contradiction by A11, A17, ZFMISC_1:4; ::_thesis: verum
end;
A18: union (Right_Cosets H) = (carr H) \/ z4 by A12, A13, ZFMISC_1:75;
now__::_thesis:_for_c_being_Element_of_G_holds_c_*_H_=_H_*_c
let c be Element of G; ::_thesis: c * H = H * c
now__::_thesis:_c_*_H_=_H_*_c
percases ( c * H = carr H or c * H <> carr H ) ;
supposeA19: c * H = carr H ; ::_thesis: c * H = H * c
then c in H by GROUP_2:113;
hence c * H = H * c by A19, GROUP_2:119; ::_thesis: verum
end;
supposeA20: c * H <> carr H ; ::_thesis: c * H = H * c
then not c in H by GROUP_2:113;
then A21: H * c <> carr H by GROUP_2:119;
c * H in Left_Cosets H by GROUP_2:def_15;
then A22: c * H = z3 by A4, A5, A20, TARSKI:def_2;
H * c in Right_Cosets H by GROUP_2:def_16;
then H * c = z4 by A12, A13, A21, TARSKI:def_2;
hence c * H = H * c by A10, A18, A14, A22, XBOOLE_1:88; ::_thesis: verum
end;
end;
end;
hence c * H = H * c ; ::_thesis: verum
end;
hence H is normal Subgroup of G by Th117; ::_thesis: verum
end;
definition
let G be Group;
let A be Subset of G;
func Normalizer 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
set X = { h where h is Element of G : A |^ h = A } ;
{ h where h is Element of G : A |^ h = A } c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { h where h is Element of G : A |^ h = A } or x in the carrier of G )
assume x in { h where h is Element of G : A |^ h = A } ; ::_thesis: x in the carrier of G
then ex h being Element of G st
( x = h & A |^ h = A ) ;
hence x in the carrier of G ; ::_thesis: verum
end;
then reconsider X = { h where h is Element of G : A |^ h = A } as Subset of G ;
A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_X_&_b_in_X_holds_
a_*_b_in_X
let a, b be Element of G; ::_thesis: ( a in X & b in X implies a * b in X )
assume ( a in X & b in X ) ; ::_thesis: a * b in X
then ( ex g being Element of G st
( a = g & A |^ g = A ) & ex h being Element of G st
( b = h & A |^ h = A ) ) ;
then A |^ (a * b) = A by Th47;
hence a * b in X ; ::_thesis: verum
end;
A2: now__::_thesis:_for_a_being_Element_of_G_st_a_in_X_holds_
a_"_in_X
let a be Element of G; ::_thesis: ( a in X implies a " in X )
assume a in X ; ::_thesis: a " in X
then ex b being Element of G st
( a = b & A |^ b = A ) ;
then A = A |^ (a ") by Th54;
hence a " in X ; ::_thesis: verum
end;
A |^ (1_ G) = A by Th52;
then 1_ G in X ;
hence ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } by A1, A2, GROUP_2:52; ::_thesis: verum
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:59;
end;
:: deftheorem Def14 defines Normalizer GROUP_3:def_14_:_
for G being Group
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = Normalizer A iff the carrier of b3 = { h where h is Element of G : A |^ h = A } );
theorem Th129: :: GROUP_3:129
for x being set
for G being Group
for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A |^ h = A ) )
proof
let x be set ; ::_thesis: for G being Group
for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A |^ h = A ) )
let G be Group; ::_thesis: for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A |^ h = A ) )
let A be Subset of G; ::_thesis: ( x in Normalizer A iff ex h being Element of G st
( x = h & A |^ h = A ) )
thus ( x in Normalizer A implies ex h being Element of G st
( x = h & A |^ h = A ) ) ::_thesis: ( ex h being Element of G st
( x = h & A |^ h = A ) implies x in Normalizer A )
proof
assume x in Normalizer A ; ::_thesis: ex h being Element of G st
( x = h & A |^ h = A )
then x in the carrier of (Normalizer A) by STRUCT_0:def_5;
then x in { h where h is Element of G : A |^ h = A } by Def14;
hence ex h being Element of G st
( x = h & A |^ h = A ) ; ::_thesis: verum
end;
given h being Element of G such that A1: ( x = h & A |^ h = A ) ; ::_thesis: x in Normalizer A
x in { b where b is Element of G : A |^ b = A } by A1;
then x in the carrier of (Normalizer A) by Def14;
hence x in Normalizer A by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th130: :: GROUP_3:130
for G being Group
for A being Subset of G holds card (con_class A) = Index (Normalizer A)
proof
let G be Group; ::_thesis: for A being Subset of G holds card (con_class A) = Index (Normalizer A)
let A be Subset of G; ::_thesis: card (con_class A) = Index (Normalizer A)
defpred S1[ set , set ] means ex a being Element of G st
( $1 = A |^ a & $2 = (Normalizer A) * a );
A1: for x being set st x in con_class A holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in con_class A implies ex y being set st S1[x,y] )
assume x in con_class A ; ::_thesis: ex y being set st S1[x,y]
then consider B being Subset of G such that
A2: x = B and
A3: A,B are_conjugated ;
consider g being Element of G such that
A4: B = A |^ g by A3, Th88;
reconsider y = (Normalizer A) * g as set ;
take y ; ::_thesis: S1[x,y]
take g ; ::_thesis: ( x = A |^ g & y = (Normalizer A) * g )
thus ( x = A |^ g & y = (Normalizer A) * g ) by A2, A4; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = con_class A and
A6: for x being set st x in con_class A holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A7: for x, y1, y2 being set st x in con_class A & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( x in con_class A & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume x in con_class A ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 )
given a being Element of G such that A8: x = A |^ a and
A9: y1 = (Normalizer A) * a ; ::_thesis: ( not S1[x,y2] or y1 = y2 )
given b being Element of G such that A10: x = A |^ b and
A11: y2 = (Normalizer A) * b ; ::_thesis: y1 = y2
A = (A |^ b) |^ (a ") by A8, A10, Th54
.= A |^ (b * (a ")) by Th47 ;
then b * (a ") in Normalizer A by Th129;
hence y1 = y2 by A9, A11, GROUP_2:120; ::_thesis: verum
end;
A12: rng f = Right_Cosets (Normalizer A)
proof
thus rng f c= Right_Cosets (Normalizer A) :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets (Normalizer A) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Right_Cosets (Normalizer A) )
assume x in rng f ; ::_thesis: x in Right_Cosets (Normalizer A)
then consider y being set such that
A13: ( y in dom f & f . y = x ) by FUNCT_1:def_3;
ex a being Element of G st
( y = A |^ a & x = (Normalizer A) * a ) by A5, A6, A13;
hence x in Right_Cosets (Normalizer A) by GROUP_2:def_16; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets (Normalizer A) or x in rng f )
assume x in Right_Cosets (Normalizer A) ; ::_thesis: x in rng f
then consider a being Element of G such that
A14: x = (Normalizer A) * a by GROUP_2:def_16;
set y = A |^ a;
A,A |^ a are_conjugated by Th88;
then A15: A |^ a in con_class A ;
then ex b being Element of G st
( A |^ a = A |^ b & f . (A |^ a) = (Normalizer A) * b ) by A6;
then x = f . (A |^ a) by A7, A14, A15;
hence x in rng f by A5, A15, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A16: x in dom f and
A17: y in dom f and
A18: f . x = f . y ; ::_thesis: x = y
consider b being Element of G such that
A19: y = A |^ b and
A20: f . y = (Normalizer A) * b by A5, A6, A17;
consider a being Element of G such that
A21: x = A |^ a and
A22: f . x = (Normalizer A) * a by A5, A6, A16;
b * (a ") in Normalizer A by A18, A22, A20, GROUP_2:120;
then ex h being Element of G st
( b * (a ") = h & A |^ h = A ) by Th129;
then A = (A |^ b) |^ (a ") by Th47;
hence x = y by A21, A19, Th54; ::_thesis: verum
end;
then con_class A, Right_Cosets (Normalizer A) are_equipotent by A5, A12, WELLORD2:def_4;
hence card (con_class A) = card (Right_Cosets (Normalizer A)) by CARD_1:5
.= Index (Normalizer A) by GROUP_2:145 ;
::_thesis: verum
end;
theorem :: GROUP_3:131
for G being Group
for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
proof
let G be Group; ::_thesis: for A being Subset of G st ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) holds
ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
let A be Subset of G; ::_thesis: ( ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) implies ex C being finite set st
( C = con_class A & card C = index (Normalizer A) ) )
A1: card (con_class A) = Index (Normalizer A) by Th130
.= card (Left_Cosets (Normalizer A)) ;
then A2: con_class A, Left_Cosets (Normalizer A) are_equipotent by CARD_1:5;
assume A3: ( con_class A is finite or Left_Cosets (Normalizer A) is finite ) ; ::_thesis: ex C being finite set st
( C = con_class A & card C = index (Normalizer A) )
then reconsider C = con_class A as finite set by A2, CARD_1:38;
take C ; ::_thesis: ( C = con_class A & card C = index (Normalizer A) )
thus C = con_class A ; ::_thesis: card C = index (Normalizer A)
Left_Cosets (Normalizer A) is finite by A3, A2, CARD_1:38;
hence card C = index (Normalizer A) by A1, GROUP_2:def_18; ::_thesis: verum
end;
theorem Th132: :: GROUP_3:132
for G being Group
for a being Element of G holds card (con_class a) = Index (Normalizer {a})
proof
let G be Group; ::_thesis: for a being Element of G holds card (con_class a) = Index (Normalizer {a})
let a be Element of G; ::_thesis: card (con_class a) = Index (Normalizer {a})
deffunc H1( set ) -> set = {$1};
consider f being Function such that
A1: dom f = con_class a and
A2: for x being set st x in con_class a holds
f . x = H1(x) from FUNCT_1:sch_3();
A3: rng f = con_class {a}
proof
thus rng f c= con_class {a} :: according to XBOOLE_0:def_10 ::_thesis: con_class {a} c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in con_class {a} )
assume x in rng f ; ::_thesis: x in con_class {a}
then consider y being set such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def_3;
reconsider y = y as Element of G by A1, A4;
f . y = {y} by A1, A2, A4;
then x in { {d} where d is Element of G : d in con_class a } by A1, A4, A5;
hence x in con_class {a} by Th100; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class {a} or x in rng f )
assume x in con_class {a} ; ::_thesis: x in rng f
then x in { {b} where b is Element of G : b in con_class a } by Th100;
then consider b being Element of G such that
A6: x = {b} and
A7: b in con_class a ;
f . b = {b} by A2, A7;
hence x in rng f by A1, A6, A7, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A8: ( x in dom f & y in dom f ) and
A9: f . x = f . y ; ::_thesis: x = y
( f . x = {x} & f . y = {y} ) by A1, A2, A8;
hence x = y by A9, ZFMISC_1:3; ::_thesis: verum
end;
then con_class a, con_class {a} are_equipotent by A1, A3, WELLORD2:def_4;
hence card (con_class a) = card (con_class {a}) by CARD_1:5
.= Index (Normalizer {a}) by Th130 ;
::_thesis: verum
end;
theorem :: GROUP_3:133
for G being Group
for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizer {a}) )
proof
let G be Group; ::_thesis: for a being Element of G st ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) holds
ex C being finite set st
( C = con_class a & card C = index (Normalizer {a}) )
let a be Element of G; ::_thesis: ( ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) implies ex C being finite set st
( C = con_class a & card C = index (Normalizer {a}) ) )
A1: card (con_class a) = Index (Normalizer {a}) by Th132
.= card (Left_Cosets (Normalizer {a})) ;
then A2: con_class a, Left_Cosets (Normalizer {a}) are_equipotent by CARD_1:5;
assume A3: ( con_class a is finite or Left_Cosets (Normalizer {a}) is finite ) ; ::_thesis: ex C being finite set st
( C = con_class a & card C = index (Normalizer {a}) )
then reconsider C = con_class a as finite set by A2, CARD_1:38;
take C ; ::_thesis: ( C = con_class a & card C = index (Normalizer {a}) )
thus C = con_class a ; ::_thesis: card C = index (Normalizer {a})
Left_Cosets (Normalizer {a}) is finite by A3, A2, CARD_1:38;
hence card C = index (Normalizer {a}) by A1, GROUP_2:def_18; ::_thesis: verum
end;
definition
let G be Group;
let H be Subgroup of G;
func Normalizer H -> strict Subgroup of G equals :: GROUP_3:def 15
Normalizer (carr H);
correctness
coherence
Normalizer (carr H) is strict Subgroup of G;
;
end;
:: deftheorem defines Normalizer GROUP_3:def_15_:_
for G being Group
for H being Subgroup of G holds Normalizer H = Normalizer (carr H);
theorem Th134: :: GROUP_3:134
for x being set
for G being Group
for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H |^ h = H ) )
proof
let x be set ; ::_thesis: for G being Group
for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H |^ h = H ) )
let G be Group; ::_thesis: for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H |^ h = H ) )
let H be strict Subgroup of G; ::_thesis: ( x in Normalizer H iff ex h being Element of G st
( x = h & H |^ h = H ) )
thus ( x in Normalizer H implies ex h being Element of G st
( x = h & H |^ h = H ) ) ::_thesis: ( ex h being Element of G st
( x = h & H |^ h = H ) implies x in Normalizer H )
proof
assume x in Normalizer H ; ::_thesis: ex h being Element of G st
( x = h & H |^ h = H )
then consider a being Element of G such that
A1: x = a and
A2: (carr H) |^ a = carr H by Th129;
H |^ a = H by A2, Def6;
hence ex h being Element of G st
( x = h & H |^ h = H ) by A1; ::_thesis: verum
end;
given h being Element of G such that A3: x = h and
A4: H |^ h = H ; ::_thesis: x in Normalizer H
(carr H) |^ h = carr H by A4, Def6;
hence x in Normalizer H by A3, Th129; ::_thesis: verum
end;
theorem Th135: :: GROUP_3:135
for G being Group
for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H)
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H)
let H be strict Subgroup of G; ::_thesis: card (con_class H) = Index (Normalizer H)
defpred S1[ set , set ] means ex H1 being strict Subgroup of G st
( $1 = H1 & $2 = carr H1 );
A1: for x being set st x in con_class H holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in con_class H implies ex y being set st S1[x,y] )
assume x in con_class H ; ::_thesis: ex y being set st S1[x,y]
then reconsider H = x as strict Subgroup of G by Def1;
reconsider y = carr H as set ;
take y ; ::_thesis: S1[x,y]
take H ; ::_thesis: ( x = H & y = carr H )
thus ( x = H & y = carr H ) ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = con_class H and
A3: for x being set st x in con_class H holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f = con_class (carr H)
proof
thus rng f c= con_class (carr H) :: according to XBOOLE_0:def_10 ::_thesis: con_class (carr H) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in con_class (carr H) )
assume x in rng f ; ::_thesis: x in con_class (carr H)
then consider y being set such that
A5: y in dom f and
A6: f . y = x by FUNCT_1:def_3;
consider H1 being strict Subgroup of G such that
A7: y = H1 and
A8: x = carr H1 by A2, A3, A5, A6;
H1,H are_conjugated by A2, A5, A7, Th107;
then carr H1, carr H are_conjugated by Th113;
hence x in con_class (carr H) by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class (carr H) or x in rng f )
assume x in con_class (carr H) ; ::_thesis: x in rng f
then consider B being Subset of G such that
A9: B = x and
A10: carr H,B are_conjugated ;
consider H1 being strict Subgroup of G such that
A11: the carrier of H1 = B by A10, Th93;
B = carr H1 by A11;
then H1,H are_conjugated by A10, Th113;
then A12: H1 in con_class H by Th107;
then ex H2 being strict Subgroup of G st
( H1 = H2 & f . H1 = carr H2 ) by A3;
hence x in rng f by A2, A9, A11, A12, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A13: ( x in dom f & y in dom f ) and
A14: f . x = f . y ; ::_thesis: x = y
( ex H1 being strict Subgroup of G st
( x = H1 & f . x = carr H1 ) & ex H2 being strict Subgroup of G st
( y = H2 & f . y = carr H2 ) ) by A2, A3, A13;
hence x = y by A14, GROUP_2:59; ::_thesis: verum
end;
then con_class H, con_class (carr H) are_equipotent by A2, A4, WELLORD2:def_4;
hence card (con_class H) = card (con_class (carr H)) by CARD_1:5
.= Index (Normalizer H) by Th130 ;
::_thesis: verum
end;
theorem :: GROUP_3:136
for G being Group
for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) holds
ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
let H be strict Subgroup of G; ::_thesis: ( ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) implies ex C being finite set st
( C = con_class H & card C = index (Normalizer H) ) )
A1: card (con_class H) = Index (Normalizer H) by Th135
.= card (Left_Cosets (Normalizer H)) ;
then A2: con_class H, Left_Cosets (Normalizer H) are_equipotent by CARD_1:5;
assume A3: ( con_class H is finite or Left_Cosets (Normalizer H) is finite ) ; ::_thesis: ex C being finite set st
( C = con_class H & card C = index (Normalizer H) )
then reconsider C = con_class H as finite set by A2, CARD_1:38;
take C ; ::_thesis: ( C = con_class H & card C = index (Normalizer H) )
thus C = con_class H ; ::_thesis: card C = index (Normalizer H)
Left_Cosets (Normalizer H) is finite by A3, A2, CARD_1:38;
hence card C = index (Normalizer H) by A1, GROUP_2:def_18; ::_thesis: verum
end;
theorem Th137: :: GROUP_3:137
for G being strict Group
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizer H = G )
proof
let G be strict Group; ::_thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizer H = G )
let H be strict Subgroup of G; ::_thesis: ( H is normal Subgroup of G iff Normalizer H = G )
thus ( H is normal Subgroup of G implies Normalizer H = G ) ::_thesis: ( Normalizer H = G implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; ::_thesis: Normalizer H = G
now__::_thesis:_for_a_being_Element_of_G_holds_a_in_Normalizer_H
let a be Element of G; ::_thesis: a in Normalizer H
H |^ a = H by A1, Def13;
hence a in Normalizer H by Th134; ::_thesis: verum
end;
hence Normalizer H = G by GROUP_2:62; ::_thesis: verum
end;
assume A2: Normalizer H = G ; ::_thesis: H is normal Subgroup of G
H is normal
proof
let a be Element of G; :: according to GROUP_3:def_13 ::_thesis: H |^ a = multMagma(# the carrier of H, the multF of H #)
a in Normalizer H by A2, STRUCT_0:def_5;
then ex b being Element of G st
( b = a & H |^ b = H ) by Th134;
hence H |^ a = multMagma(# the carrier of H, the multF of H #) ; ::_thesis: verum
end;
hence H is normal Subgroup of G ; ::_thesis: verum
end;
theorem :: GROUP_3:138
for G being strict Group holds Normalizer ((1). G) = G
proof
let G be strict Group; ::_thesis: Normalizer ((1). G) = G
(1). G is normal Subgroup of G by Th114;
hence Normalizer ((1). G) = G by Th137; ::_thesis: verum
end;
theorem :: GROUP_3:139
for G being strict Group holds Normalizer ((Omega). G) = G
proof
let G be strict Group; ::_thesis: Normalizer ((Omega). G) = G
(Omega). G is normal Subgroup of G by Th114;
hence Normalizer ((Omega). G) = G by Th137; ::_thesis: verum
end;