:: GROUP_6 semantic presentation
begin
theorem Th1: :: GROUP_6:1
for A, B being non empty set
for f being Function of A,B holds
( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
proof
let A, B be non empty set ; ::_thesis: for f being Function of A,B holds
( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
let f be Function of A,B; ::_thesis: ( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
thus ( f is one-to-one implies for a, b being Element of A st f . a = f . b holds
a = b ) by FUNCT_2:19; ::_thesis: ( ( for a, b being Element of A st f . a = f . b holds
a = b ) implies f is one-to-one )
assume for a, b being Element of A st f . a = f . b holds
a = b ; ::_thesis: f is one-to-one
then for a, b being set st a in A & b in A & f . a = f . b holds
a = b ;
hence f is one-to-one by FUNCT_2:19; ::_thesis: verum
end;
definition
let G be Group;
let A be Subgroup of G;
:: original: Subgroup
redefine mode Subgroup of A -> Subgroup of G;
coherence
for b1 being Subgroup of A holds b1 is Subgroup of G by GROUP_2:56;
end;
registration
let G be Group;
cluster (1). G -> normal ;
coherence
(1). G is normal by GROUP_3:114;
cluster (Omega). G -> normal ;
coherence
(Omega). G is normal by GROUP_3:114;
end;
theorem Th2: :: GROUP_6:2
for G being Group
for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
proof
let G be Group; ::_thesis: for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let A be Subgroup of G; ::_thesis: for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let a be Element of G; ::_thesis: for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let X be Subgroup of A; ::_thesis: for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
let x be Element of A; ::_thesis: ( x = a implies ( x * X = a * X & X * x = X * a ) )
set I = X;
assume A1: x = a ; ::_thesis: ( x * X = a * X & X * x = X * a )
thus x * X c= a * X :: according to XBOOLE_0:def_10 ::_thesis: ( a * X c= x * X & X * x = X * a )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * X or y in a * X )
assume y in x * X ; ::_thesis: y in a * X
then consider g being Element of A such that
A2: ( y = x * g & g in X ) by GROUP_2:103;
reconsider h = g as Element of G by GROUP_2:42;
a * h = x * g by A1, GROUP_2:43;
hence y in a * X by A2, GROUP_2:103; ::_thesis: verum
end;
thus a * X c= x * X ::_thesis: X * x = X * a
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a * X or y in x * X )
assume y in a * X ; ::_thesis: y in x * X
then consider b being Element of G such that
A3: y = a * b and
A4: b in X by GROUP_2:103;
reconsider c = b as Element of X by A4, STRUCT_0:def_5;
reconsider c = c as Element of A by GROUP_2:42;
a * b = x * c by A1, GROUP_2:43;
hence y in x * X by A3, A4, GROUP_2:103; ::_thesis: verum
end;
thus X * x c= X * a :: according to XBOOLE_0:def_10 ::_thesis: X * a c= X * x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X * x or y in X * a )
assume y in X * x ; ::_thesis: y in X * a
then consider g being Element of A such that
A5: ( y = g * x & g in X ) by GROUP_2:104;
reconsider h = g as Element of G by GROUP_2:42;
h * a = g * x by A1, GROUP_2:43;
hence y in X * a by A5, GROUP_2:104; ::_thesis: verum
end;
thus X * a c= X * x ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X * a or y in X * x )
assume y in X * a ; ::_thesis: y in X * x
then consider b being Element of G such that
A6: y = b * a and
A7: b in X by GROUP_2:104;
reconsider c = b as Element of X by A7, STRUCT_0:def_5;
reconsider c = c as Element of A by GROUP_2:42;
b * a = c * x by A1, GROUP_2:43;
hence y in X * x by A6, A7, GROUP_2:104; ::_thesis: verum
end;
end;
theorem :: GROUP_6:3
for G being Group
for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y
proof
let G be Group; ::_thesis: for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y
let A be Subgroup of G; ::_thesis: for X, Y being Subgroup of A holds X /\ Y = X /\ Y
let X, Y be Subgroup of A; ::_thesis: X /\ Y = X /\ Y
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:56;
the carrier of (X /\ Y) = (carr X) /\ (carr Y) by GROUP_2:def_10;
then X /\ Y = Z by GROUP_2:80;
hence X /\ Y = X /\ Y ; ::_thesis: verum
end;
theorem Th4: :: GROUP_6:4
for G being Group
for a, b being Element of G holds
( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )
let a, b be Element of G; ::_thesis: ( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )
thus (a * b) * (a ") = (((a ") ") * b) * (a ")
.= b |^ (a ") by GROUP_3:def_2 ; ::_thesis: a * (b * (a ")) = b |^ (a ")
hence a * (b * (a ")) = b |^ (a ") by GROUP_1:def_3; ::_thesis: verum
end;
theorem Th5: :: GROUP_6:5
for G being Group
for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
proof
let G be Group; ::_thesis: for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
let A be Subgroup of G; ::_thesis: for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
let a be Element of G; ::_thesis: ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
thus (a * A) * A = a * (A * A) by GROUP_4:45
.= a * A by GROUP_2:76 ; ::_thesis: ( a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
hence a * (A * A) = a * A by GROUP_4:45; ::_thesis: ( (A * A) * a = A * a & A * (A * a) = A * a )
thus (A * A) * a = A * a by GROUP_2:76; ::_thesis: A * (A * a) = A * a
hence A * (A * a) = A * a by GROUP_4:46; ::_thesis: verum
end;
theorem Th6: :: GROUP_6:6
for G being Group
for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds
G ` = gr A1
proof
let G be Group; ::_thesis: for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds
G ` = gr A1
let A1 be Subset of G; ::_thesis: ( A1 = { [.a,b.] where a, b is Element of G : verum } implies G ` = gr A1 )
assume A1: A1 = { [.a,b.] where a, b is Element of G : verum } ; ::_thesis: G ` = gr A1
A1 = commutators G
proof
thus A1 c= commutators G :: according to XBOOLE_0:def_10 ::_thesis: commutators G c= A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in commutators G )
assume x in A1 ; ::_thesis: x in commutators G
then ex a, b being Element of G st x = [.a,b.] by A1;
hence x in commutators G by GROUP_5:58; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators G or x in A1 )
assume x in commutators G ; ::_thesis: x in A1
then ex a, b being Element of G st x = [.a,b.] by GROUP_5:58;
hence x in A1 by A1; ::_thesis: verum
end;
hence G ` = gr A1 by GROUP_5:72; ::_thesis: verum
end;
theorem Th7: :: GROUP_6:7
for G being strict Group
for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
proof
defpred S1[ set , set ] means verum;
let G be strict Group; ::_thesis: for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
let B be strict Subgroup of G; ::_thesis: ( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )
thus ( G ` is Subgroup of B implies for a, b being Element of G holds [.a,b.] in B ) by GROUP_2:40, GROUP_5:74; ::_thesis: ( ( for a, b being Element of G holds [.a,b.] in B ) implies G ` is Subgroup of B )
deffunc H1( Element of G, Element of G) -> Element of the carrier of G = [.$1,$2.];
reconsider X = { H1(a,b) where a, b is Element of G : S1[a,b] } as Subset of G from DOMAIN_1:sch_9();
assume A1: for a, b being Element of G holds [.a,b.] in B ; ::_thesis: G ` is Subgroup of B
X c= the carrier of B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of B )
assume x in X ; ::_thesis: x in the carrier of B
then ex a, b being Element of G st x = [.a,b.] ;
then x in B by A1;
hence x in the carrier of B by STRUCT_0:def_5; ::_thesis: verum
end;
then gr X is Subgroup of B by GROUP_4:def_4;
hence G ` is Subgroup of B by Th6; ::_thesis: verum
end;
theorem Th8: :: GROUP_6:8
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
proof
let G be Group; ::_thesis: for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
let B be Subgroup of G; ::_thesis: for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
let N be normal Subgroup of G; ::_thesis: ( N is Subgroup of B implies N is normal Subgroup of B )
assume N is Subgroup of B ; ::_thesis: N is normal Subgroup of B
then reconsider N9 = N as Subgroup of B ;
now__::_thesis:_for_n_being_Element_of_B_holds_n_*_N9_c=_N9_*_n
let n be Element of B; ::_thesis: n * N9 c= N9 * n
thus n * N9 c= N9 * n ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n * N9 or x in N9 * n )
assume x in n * N9 ; ::_thesis: x in N9 * n
then consider a being Element of B such that
A1: x = n * a and
A2: a in N9 by GROUP_2:103;
reconsider a9 = a, n9 = n as Element of G by GROUP_2:42;
x = n9 * a9 by A1, GROUP_2:43;
then A3: x in n9 * N by A2, GROUP_2:103;
n9 * N c= N * n9 by GROUP_3:118;
then consider a1 being Element of G such that
A4: x = a1 * n9 and
A5: a1 in N by A3, GROUP_2:104;
a1 in N9 by A5;
then a1 in B by GROUP_2:40;
then reconsider a19 = a1 as Element of B by STRUCT_0:def_5;
x = a19 * n by A4, GROUP_2:43;
hence x in N9 * n by A5, GROUP_2:104; ::_thesis: verum
end;
end;
hence N is normal Subgroup of B by GROUP_3:118; ::_thesis: verum
end;
definition
let G be Group;
let B be Subgroup of G;
let M be normal Subgroup of G;
assume A1: multMagma(# the carrier of M, the multF of M #) is Subgroup of B ;
func(B,M) `*` -> strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1
multMagma(# the carrier of M, the multF of M #);
coherence
multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B
proof
reconsider x = multMagma(# the carrier of M, the multF of M #) as Subgroup of G by A1;
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_x_=_x_*_a
let a be Element of G; ::_thesis: a * x = x * a
thus a * x = a * M
.= M * a by GROUP_3:117
.= x * a ; ::_thesis: verum
end;
then x is normal Subgroup of G by GROUP_3:117;
hence multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B by A1, Th8; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def1 defines `*` GROUP_6:def_1_:_
for G being Group
for B being Subgroup of G
for M being normal Subgroup of G st multMagma(# the carrier of M, the multF of M #) is Subgroup of B holds
(B,M) `*` = multMagma(# the carrier of M, the multF of M #);
theorem Th9: :: GROUP_6:9
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
proof
let G be Group; ::_thesis: for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
let B be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
let N be normal Subgroup of G; ::_thesis: ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
thus B /\ N is normal Subgroup of B ::_thesis: N /\ B is normal Subgroup of B
proof
reconsider A = B /\ N as Subgroup of B by GROUP_2:88;
now__::_thesis:_for_b_being_Element_of_B_holds_b_*_A_c=_A_*_b
let b be Element of B; ::_thesis: b * A c= A * b
thus b * A c= A * b ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * A or x in A * b )
assume x in b * A ; ::_thesis: x in A * b
then consider a being Element of B such that
A1: x = b * a and
A2: a in A by GROUP_2:103;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
( a in N & x = b9 * a9 ) by A1, A2, GROUP_2:43, GROUP_2:82;
then A3: x in b9 * N by GROUP_2:103;
reconsider x9 = x as Element of B by A1;
A4: b9 " = b " by GROUP_2:48;
b9 * N c= N * b9 by GROUP_3:118;
then consider b1 being Element of G such that
A5: x = b1 * b9 and
A6: b1 in N by A3, GROUP_2:104;
reconsider x99 = x as Element of G by A5;
b1 = x99 * (b9 ") by A5, GROUP_1:14;
then A7: b1 = x9 * (b ") by A4, GROUP_2:43;
then reconsider b19 = b1 as Element of B ;
b1 in B by A7, STRUCT_0:def_5;
then A8: b19 in A by A6, GROUP_2:82;
b19 * b = x by A5, GROUP_2:43;
hence x in A * b by A8, GROUP_2:104; ::_thesis: verum
end;
end;
hence B /\ N is normal Subgroup of B by GROUP_3:118; ::_thesis: verum
end;
hence N /\ B is normal Subgroup of B ; ::_thesis: verum
end;
definition
let G be Group;
let B be Subgroup of G;
let N be normal Subgroup of G;
:: original: /\
redefine funcB /\ N -> strict normal Subgroup of B;
coherence
B /\ N is strict normal Subgroup of B by Th9;
end;
definition
let G be Group;
let N be normal Subgroup of G;
let B be Subgroup of G;
:: original: /\
redefine funcN /\ B -> strict normal Subgroup of B;
coherence
N /\ B is strict normal Subgroup of B by Th9;
end;
definition
let G be non empty 1-sorted ;
redefine attr G is trivial means :Def2: :: GROUP_6:def 2
ex x being set st the carrier of G = {x};
compatibility
( G is trivial iff ex x being set st the carrier of G = {x} )
proof
hereby ::_thesis: ( ex x being set st the carrier of G = {x} implies G is trivial )
set y = the Element of G;
assume G is trivial ; ::_thesis: ex x being set st the carrier of G = {x}
then for x being set holds
( x in the carrier of G iff x = the Element of G ) by STRUCT_0:def_10;
then the carrier of G = { the Element of G} by TARSKI:def_1;
hence ex x being set st the carrier of G = {x} ; ::_thesis: verum
end;
given x being set such that A1: the carrier of G = {x} ; ::_thesis: G is trivial
now__::_thesis:_for_a,_b_being_Element_of_G_holds_a_=_b
let a, b be Element of G; ::_thesis: a = b
thus a = x by A1, TARSKI:def_1
.= b by A1, TARSKI:def_1 ; ::_thesis: verum
end;
hence G is trivial by STRUCT_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines trivial GROUP_6:def_2_:_
for G being non empty 1-sorted holds
( G is trivial iff ex x being set st the carrier of G = {x} );
theorem Th10: :: GROUP_6:10
for G being Group holds (1). G is trivial
proof
let G be Group; ::_thesis: (1). G is trivial
the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7;
hence (1). G is trivial by Def2; ::_thesis: verum
end;
registration
let G be Group;
cluster (1). G -> trivial ;
coherence
(1). G is trivial by Th10;
end;
registration
cluster non empty trivial strict unital Group-like associative for multMagma ;
existence
ex b1 being Group st
( b1 is strict & b1 is trivial )
proof
set G = the Group;
take (1). the Group ; ::_thesis: ( (1). the Group is strict & (1). the Group is trivial )
thus ( (1). the Group is strict & (1). the Group is trivial ) ; ::_thesis: verum
end;
end;
theorem Th11: :: GROUP_6:11
( ( for G being trivial Group holds
( card G = 1 & G is finite ) ) & ( for G being finite Group st card G = 1 holds
G is trivial ) )
proof
thus for G being trivial Group holds
( card G = 1 & G is finite ) ::_thesis: for G being finite Group st card G = 1 holds
G is trivial
proof
let G be trivial Group; ::_thesis: ( card G = 1 & G is finite )
ex x being set st the carrier of G = {x} by Def2;
hence ( card G = 1 & G is finite ) by CARD_1:30; ::_thesis: verum
end;
let G be finite Group; ::_thesis: ( card G = 1 implies G is trivial )
assume card G = 1 ; ::_thesis: G is trivial
hence ex x being set st the carrier of G = {x} by CARD_2:42; :: according to GROUP_6:def_2 ::_thesis: verum
end;
theorem Th12: :: GROUP_6:12
for G being trivial strict Group holds (1). G = G
proof
let G be trivial strict Group; ::_thesis: (1). G = G
card G = 1 by Th11;
then card G = card ((1). G) by GROUP_2:69;
hence (1). G = G by GROUP_2:73; ::_thesis: verum
end;
notation
let G be Group;
let N be normal Subgroup of G;
synonym Cosets N for Left_Cosets N;
end;
registration
let G be Group;
let N be normal Subgroup of G;
cluster Cosets N -> non empty ;
coherence
not Cosets N is empty by GROUP_2:135;
end;
theorem Th13: :: GROUP_6:13
for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
proof
let G be Group; ::_thesis: for x being set
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
let x be set ; ::_thesis: for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
let N be normal Subgroup of G; ::_thesis: ( x in Cosets N implies ex a being Element of G st
( x = a * N & x = N * a ) )
assume x in Cosets N ; ::_thesis: ex a being Element of G st
( x = a * N & x = N * a )
then consider a being Element of G such that
A1: x = a * N by GROUP_2:def_15;
x = N * a by A1, GROUP_3:117;
hence ex a being Element of G st
( x = a * N & x = N * a ) by A1; ::_thesis: verum
end;
theorem Th14: :: GROUP_6:14
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
proof
let G be Group; ::_thesis: for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
let a be Element of G; ::_thesis: for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
let N be normal Subgroup of G; ::_thesis: ( a * N in Cosets N & N * a in Cosets N )
N * a in Right_Cosets N by GROUP_2:def_16;
hence ( a * N in Cosets N & N * a in Cosets N ) by GROUP_2:def_15, GROUP_3:127; ::_thesis: verum
end;
theorem Th15: :: GROUP_6:15
for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
x is Subset of G ;
theorem Th16: :: GROUP_6:16
for G being Group
for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
proof
let G be Group; ::_thesis: for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
let A1, A2 be Subset of G; ::_thesis: for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
let N be normal Subgroup of G; ::_thesis: ( A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N )
assume that
A1: A1 in Cosets N and
A2: A2 in Cosets N ; ::_thesis: A1 * A2 in Cosets N
consider a being Element of G such that
A3: A1 = a * N and
A1 = N * a by A1, Th13;
consider b being Element of G such that
A4: A2 = b * N and
A5: A2 = N * b by A2, Th13;
A1 * A2 = a * (N * (b * N)) by A3, A4, GROUP_3:10
.= a * ((b * N) * N) by A4, A5, GROUP_3:13
.= a * (b * (N * N)) by GROUP_4:45
.= a * (b * N) by GROUP_2:76
.= (a * b) * N by GROUP_2:105 ;
hence A1 * A2 in Cosets N by GROUP_2:def_15; ::_thesis: verum
end;
definition
let G be Group;
let N be normal Subgroup of G;
func CosOp N -> BinOp of (Cosets N) means :Def3: :: GROUP_6:def 3
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
it . (W1,W2) = A1 * A2;
existence
ex b1 being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2
proof
defpred S1[ Element of Cosets N, Element of Cosets N, set ] means for A1, A2 being Subset of G st $1 = A1 & $2 = A2 holds
$3 = A1 * A2;
A1: for W1, W2 being Element of Cosets N ex V being Element of Cosets N st S1[W1,W2,V]
proof
let W1, W2 be Element of Cosets N; ::_thesis: ex V being Element of Cosets N st S1[W1,W2,V]
reconsider A1 = W1, A2 = W2 as Subset of G by Th15;
reconsider C = A1 * A2 as Element of Cosets N by Th16;
take C ; ::_thesis: S1[W1,W2,C]
thus S1[W1,W2,C] ; ::_thesis: verum
end;
thus ex B being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N holds S1[W1,W2,B . (W1,W2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Cosets N) st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b2 . (W1,W2) = A1 * A2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Cosets N); ::_thesis: ( ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o2 . (W1,W2) = A1 * A2 ) implies o1 = o2 )
assume A2: for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o1 . (W1,W2) = A1 * A2 ; ::_thesis: ( ex W1, W2 being Element of Cosets N ex A1, A2 being Subset of G st
( W1 = A1 & W2 = A2 & not o2 . (W1,W2) = A1 * A2 ) or o1 = o2 )
assume A3: for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
o2 . (W1,W2) = A1 * A2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Cosets_N_&_y_in_Cosets_N_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Cosets N & y in Cosets N implies o1 . (x,y) = o2 . (x,y) )
assume A4: ( x in Cosets N & y in Cosets N ) ; ::_thesis: o1 . (x,y) = o2 . (x,y)
then reconsider W = x, V = y as Element of Cosets N ;
reconsider A1 = x, A2 = y as Subset of G by A4;
o1 . (W,V) = A1 * A2 by A2;
hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines CosOp GROUP_6:def_3_:_
for G being Group
for N being normal Subgroup of G
for b3 being BinOp of (Cosets N) holds
( b3 = CosOp N iff for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b3 . (W1,W2) = A1 * A2 );
definition
let G be Group;
let N be normal Subgroup of G;
funcG ./. N -> multMagma equals :: GROUP_6:def 4
multMagma(# (Cosets N),(CosOp N) #);
correctness
coherence
multMagma(# (Cosets N),(CosOp N) #) is multMagma ;
;
end;
:: deftheorem defines ./. GROUP_6:def_4_:_
for G being Group
for N being normal Subgroup of G holds G ./. N = multMagma(# (Cosets N),(CosOp N) #);
registration
let G be Group;
let N be normal Subgroup of G;
clusterG ./. N -> non empty strict ;
coherence
( G ./. N is strict & not G ./. N is empty ) ;
end;
theorem :: GROUP_6:17
for G being Group
for N being normal Subgroup of G holds the carrier of (G ./. N) = Cosets N ;
theorem :: GROUP_6:18
for G being Group
for N being normal Subgroup of G holds the multF of (G ./. N) = CosOp N ;
definition
let G be Group;
let N be normal Subgroup of G;
let S be Element of (G ./. N);
func @ S -> Subset of G equals :: GROUP_6:def 5
S;
coherence
S is Subset of G by Th15;
end;
:: deftheorem defines @ GROUP_6:def_5_:_
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) holds @ S = S;
theorem :: GROUP_6:19
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def3;
theorem :: GROUP_6:20
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def3;
registration
let G be Group;
let N be normal Subgroup of G;
clusterG ./. N -> Group-like associative ;
coherence
( G ./. N is associative & G ./. N is Group-like )
proof
thus for f, g, h being Element of (G ./. N) holds f * (g * h) = (f * g) * h :: according to GROUP_1:def_3 ::_thesis: G ./. N is Group-like
proof
let f, g, h be Element of (G ./. N); ::_thesis: f * (g * h) = (f * g) * h
consider a being Element of G such that
A1: f = a * N and
f = N * a by Th13;
consider c being Element of G such that
A2: h = c * N and
h = N * c by Th13;
thus f * (g * h) = (@ f) * (@ (g * h)) by Def3
.= (a * N) * ((@ g) * (@ h)) by A1, Def3
.= ((@ f) * (@ g)) * (c * N) by A1, A2, GROUP_2:10
.= (@ (f * g)) * (@ h) by A2, Def3
.= (f * g) * h by Def3 ; ::_thesis: verum
end;
reconsider e = carr N as Element of (G ./. N) by GROUP_2:135;
take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (G ./. N) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (G ./. N) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (G ./. N); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (G ./. N) st
( h * b1 = e & b1 * h = e ) )
consider a being Element of G such that
A3: h = a * N and
A4: h = N * a by Th13;
thus h * e = (a * N) * N by A3, Def3
.= a * (N * N) by GROUP_4:45
.= h by A3, GROUP_2:76 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (G ./. N) st
( h * b1 = e & b1 * h = e ) )
thus e * h = N * (N * a) by A4, Def3
.= (N * N) * a by GROUP_4:46
.= h by A4, GROUP_2:76 ; ::_thesis: ex b1 being Element of the carrier of (G ./. N) st
( h * b1 = e & b1 * h = e )
reconsider g = (a ") * N as Element of (G ./. N) by GROUP_2:def_15;
take g ; ::_thesis: ( h * g = e & g * h = e )
thus h * g = (N * a) * ((a ") * N) by A4, Def3
.= ((N * a) * (a ")) * N by GROUP_3:9
.= (N * (a * (a "))) * N by GROUP_2:107
.= (N * (1_ G)) * N by GROUP_1:def_5
.= (carr N) * (carr N) by GROUP_2:109
.= e by GROUP_2:76 ; ::_thesis: g * h = e
thus g * h = (@ g) * (@ h) by Def3
.= (((a ") * N) * a) * N by A3, GROUP_3:9
.= ((a ") * (N * a)) * N by GROUP_2:106
.= ((a ") * (a * N)) * N by GROUP_3:117
.= (((a ") * a) * N) * N by GROUP_2:105
.= ((1_ G) * N) * N by GROUP_1:def_5
.= (1_ G) * (N * N) by GROUP_4:45
.= (1_ G) * (carr N) by GROUP_2:76
.= e by GROUP_2:37 ; ::_thesis: verum
end;
end;
theorem :: GROUP_6:21
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) ex a being Element of G st
( S = a * N & S = N * a ) by Th13;
theorem :: GROUP_6:22
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by Th14, GROUP_2:135;
theorem Th23: :: GROUP_6:23
for G being Group
for x being set
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
proof
let G be Group; ::_thesis: for x being set
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
let x be set ; ::_thesis: for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
let N be normal Subgroup of G; ::_thesis: ( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )
thus ( x in G ./. N implies ex a being Element of G st
( x = a * N & x = N * a ) ) ::_thesis: ( ex a being Element of G st
( x = a * N & x = N * a ) implies x in G ./. N )
proof
assume x in G ./. N ; ::_thesis: ex a being Element of G st
( x = a * N & x = N * a )
then x is Element of (G ./. N) by STRUCT_0:def_5;
hence ex a being Element of G st
( x = a * N & x = N * a ) by Th13; ::_thesis: verum
end;
given a being Element of G such that A1: x = a * N and
x = N * a ; ::_thesis: x in G ./. N
x is Element of (G ./. N) by A1, Th14;
hence x in G ./. N by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th24: :: GROUP_6:24
for G being Group
for N being normal Subgroup of G holds 1_ (G ./. N) = carr N
proof
let G be Group; ::_thesis: for N being normal Subgroup of G holds 1_ (G ./. N) = carr N
let N be normal Subgroup of G; ::_thesis: 1_ (G ./. N) = carr N
reconsider e = carr N as Element of (G ./. N) by GROUP_2:135;
now__::_thesis:_for_h_being_Element_of_(G_./._N)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (G ./. N); ::_thesis: ( h * e = h & e * h = h )
consider a being Element of G such that
A1: h = a * N and
A2: h = N * a by Th13;
thus h * e = (a * N) * N by A1, Def3
.= a * (N * N) by GROUP_4:45
.= h by A1, GROUP_2:76 ; ::_thesis: e * h = h
thus e * h = N * (N * a) by A2, Def3
.= (N * N) * a by GROUP_4:46
.= h by A2, GROUP_2:76 ; ::_thesis: verum
end;
hence 1_ (G ./. N) = carr N by GROUP_1:4; ::_thesis: verum
end;
theorem Th25: :: GROUP_6:25
for G being Group
for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
proof
let G be Group; ::_thesis: for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
let a be Element of G; ::_thesis: for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
let N be normal Subgroup of G; ::_thesis: for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
let S be Element of (G ./. N); ::_thesis: ( S = a * N implies S " = (a ") * N )
reconsider g = (a ") * N as Element of (G ./. N) by Th14;
assume A1: S = a * N ; ::_thesis: S " = (a ") * N
A2: g * S = (@ g) * (@ S) by Def3
.= (((a ") * N) * a) * N by A1, GROUP_3:9
.= ((a ") * (N * a)) * N by GROUP_2:106
.= ((a ") * (a * N)) * N by GROUP_3:117
.= (((a ") * a) * N) * N by GROUP_2:105
.= ((1_ G) * N) * N by GROUP_1:def_5
.= (1_ G) * (N * N) by GROUP_4:45
.= (1_ G) * (carr N) by GROUP_2:76
.= carr N by GROUP_2:37 ;
A3: 1_ (G ./. N) = carr N by Th24;
S * g = (@ S) * (@ g) by Def3
.= (N * a) * ((a ") * N) by A1, GROUP_3:117
.= ((N * a) * (a ")) * N by GROUP_3:9
.= (N * (a * (a "))) * N by GROUP_2:107
.= (N * (1_ G)) * N by GROUP_1:def_5
.= (carr N) * (carr N) by GROUP_2:109
.= carr N by GROUP_2:76 ;
hence S " = (a ") * N by A2, A3, GROUP_1:def_5; ::_thesis: verum
end;
theorem :: GROUP_6:26
for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;
theorem :: GROUP_6:27
for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N
proof
let G be Group; ::_thesis: for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N
let N be normal Subgroup of G; ::_thesis: ( Left_Cosets N is finite implies card (G ./. N) = index N )
assume Left_Cosets N is finite ; ::_thesis: card (G ./. N) = index N
then reconsider LC = Left_Cosets N as finite set ;
thus card (G ./. N) = card LC
.= index N by GROUP_2:def_18 ; ::_thesis: verum
end;
theorem Th28: :: GROUP_6:28
for G being Group
for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) `*`) is Subgroup of G ./. M
proof
let G be Group; ::_thesis: for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) `*`) is Subgroup of G ./. M
let B be Subgroup of G; ::_thesis: for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) `*`) is Subgroup of G ./. M
let M be strict normal Subgroup of G; ::_thesis: ( M is Subgroup of B implies B ./. ((B,M) `*`) is Subgroup of G ./. M )
set I = B ./. ((B,M) `*`);
set J = (B,M) `*` ;
set g = the multF of (B ./. ((B,M) `*`));
set f = the multF of (G ./. M);
set X = [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):];
assume A1: M is Subgroup of B ; ::_thesis: B ./. ((B,M) `*`) is Subgroup of G ./. M
A2: the carrier of (B ./. ((B,M) `*`)) c= the carrier of (G ./. M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (B ./. ((B,M) `*`)) or x in the carrier of (G ./. M) )
assume x in the carrier of (B ./. ((B,M) `*`)) ; ::_thesis: x in the carrier of (G ./. M)
then consider a being Element of B such that
A3: x = a * ((B,M) `*`) and
x = ((B,M) `*`) * a by Th13;
reconsider b = a as Element of G by GROUP_2:42;
(B,M) `*` = M by A1, Def1;
then a * ((B,M) `*`) = b * M by Th2;
hence x in the carrier of (G ./. M) by A3, Th14; ::_thesis: verum
end;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_the_multF_of_(B_./._((B,M)_`*`))_holds_
the_multF_of_(B_./._((B,M)_`*`))_._x_=_the_multF_of_(G_./._M)_._x
let x be set ; ::_thesis: ( x in dom the multF of (B ./. ((B,M) `*`)) implies the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x )
assume A5: x in dom the multF of (B ./. ((B,M) `*`)) ; ::_thesis: the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x
then consider y, z being set such that
A6: [y,z] = x by RELAT_1:def_1;
z in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87;
then consider b being Element of B such that
A7: z = b * ((B,M) `*`) and
A8: z = ((B,M) `*`) * b by Th13;
y in the carrier of (B ./. ((B,M) `*`)) by A5, A6, ZFMISC_1:87;
then consider a being Element of B such that
A9: y = a * ((B,M) `*`) and
y = ((B,M) `*`) * a by Th13;
reconsider W1 = y, W2 = z as Element of Cosets ((B,M) `*`) by A9, A7, Th14;
A10: the multF of (B ./. ((B,M) `*`)) . x = the multF of (B ./. ((B,M) `*`)) . (W1,W2) by A6
.= (a * ((B,M) `*`)) * (((B,M) `*`) * b) by A9, A8, Def3
.= ((a * ((B,M) `*`)) * ((B,M) `*`)) * b by GROUP_3:11
.= (a * (((B,M) `*`) * ((B,M) `*`))) * b by GROUP_4:45
.= (a * ((B,M) `*`)) * b by GROUP_2:76
.= a * (((B,M) `*`) * b) by GROUP_2:106
.= a * (b * ((B,M) `*`)) by GROUP_3:117
.= (a * b) * ((B,M) `*`) by GROUP_2:105 ;
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
A11: (B,M) `*` = M by A1, Def1;
then A12: y = a9 * M by A9, Th2;
z = b9 * M by A7, A11, Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by A12, Th14;
A13: a9 * b9 = a * b by GROUP_2:43;
A14: z = M * b9 by A8, A11, Th2;
the multF of (G ./. M) . x = the multF of (G ./. M) . (V1,V2) by A6
.= (a9 * M) * (M * b9) by A12, A14, Def3
.= ((a9 * M) * M) * b9 by GROUP_3:11
.= (a9 * (M * M)) * b9 by GROUP_4:45
.= (a9 * M) * b9 by GROUP_2:76
.= a9 * (M * b9) by GROUP_2:106
.= a9 * (b9 * M) by GROUP_3:117
.= (a9 * b9) * M by GROUP_2:105 ;
hence the multF of (B ./. ((B,M) `*`)) . x = the multF of (G ./. M) . x by A10, A11, A13, Th2; ::_thesis: verum
end;
( dom the multF of (B ./. ((B,M) `*`)) = [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):] & dom the multF of (G ./. M) = [: the carrier of (G ./. M), the carrier of (G ./. M):] ) by FUNCT_2:def_1;
then dom the multF of (B ./. ((B,M) `*`)) = (dom the multF of (G ./. M)) /\ [: the carrier of (B ./. ((B,M) `*`)), the carrier of (B ./. ((B,M) `*`)):] by A2, XBOOLE_1:28, ZFMISC_1:96;
then the multF of (B ./. ((B,M) `*`)) = the multF of (G ./. M) || the carrier of (B ./. ((B,M) `*`)) by A4, FUNCT_1:46;
hence B ./. ((B,M) `*`) is Subgroup of G ./. M by A2, GROUP_2:def_5; ::_thesis: verum
end;
theorem :: GROUP_6:29
for G being Group
for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) `*`) is normal Subgroup of G ./. M
proof
let G be Group; ::_thesis: for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) `*`) is normal Subgroup of G ./. M
let N, M be strict normal Subgroup of G; ::_thesis: ( M is Subgroup of N implies N ./. ((N,M) `*`) is normal Subgroup of G ./. M )
assume A1: M is Subgroup of N ; ::_thesis: N ./. ((N,M) `*`) is normal Subgroup of G ./. M
then A2: (N,M) `*` = M by Def1;
then reconsider I = M as normal Subgroup of N ;
reconsider J = N ./. ((N,M) `*`) as Subgroup of G ./. M by A1, Th28;
now__::_thesis:_for_S_being_Element_of_(G_./._M)_holds_S_*_J_c=_J_*_S
let S be Element of (G ./. M); ::_thesis: S * J c= J * S
thus S * J c= J * S ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S * J or x in J * S )
assume x in S * J ; ::_thesis: x in J * S
then consider T being Element of (G ./. M) such that
A3: x = S * T and
A4: T in J by GROUP_2:103;
consider c being Element of N such that
T = c * I and
A5: T = I * c by A2, A4, Th23;
reconsider d = c as Element of G by GROUP_2:42;
consider a being Element of G such that
S = a * M and
A6: S = M * a by Th13;
set e = a * (d * (a "));
( c in N & a * (d * (a ")) = d |^ (a ") ) by Th4, STRUCT_0:def_5;
then a * (d * (a ")) in N by GROUP_5:3;
then reconsider f = a * (d * (a ")) as Element of N by STRUCT_0:def_5;
A7: M * (a * (d * (a "))) = I * f by Th2;
reconsider V = I * f as Element of J by A2, Th14;
A8: V in J by STRUCT_0:def_5;
reconsider V = V as Element of (G ./. M) by GROUP_2:42;
M * d = I * c by Th2;
then x = (M * a) * (M * d) by A3, A6, A5, Def3
.= (M * a) * ((M * d) * (1_ G)) by GROUP_2:37
.= (M * a) * ((M * d) * ((a ") * a)) by GROUP_1:def_5
.= (M * a) * (M * (d * ((a ") * a))) by GROUP_2:107
.= ((M * a) * M) * (d * ((a ") * a)) by GROUP_3:11
.= (M * (a * M)) * (d * ((a ") * a)) by GROUP_3:13
.= (M * (M * a)) * (d * ((a ") * a)) by GROUP_3:117
.= M * ((M * a) * (d * ((a ") * a))) by GROUP_2:98
.= M * (M * (a * (d * ((a ") * a)))) by GROUP_2:107
.= M * (M * (a * ((d * (a ")) * a))) by GROUP_1:def_3
.= M * (M * ((a * (d * (a "))) * a)) by GROUP_1:def_3
.= M * ((M * (a * (d * (a ")))) * a) by GROUP_2:107
.= M * (((a * (d * (a "))) * M) * a) by GROUP_3:117
.= M * ((a * (d * (a "))) * (M * a)) by GROUP_2:106
.= (M * (a * (d * (a ")))) * (M * a) by GROUP_3:12
.= V * S by A6, A7, Def3 ;
hence x in J * S by A8, GROUP_2:104; ::_thesis: verum
end;
end;
hence N ./. ((N,M) `*`) is normal Subgroup of G ./. M by GROUP_3:118; ::_thesis: verum
end;
theorem :: GROUP_6:30
for G being strict Group
for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G ` is Subgroup of N )
proof
let G be strict Group; ::_thesis: for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G ` is Subgroup of N )
let N be strict normal Subgroup of G; ::_thesis: ( G ./. N is commutative Group iff G ` is Subgroup of N )
thus ( G ./. N is commutative Group implies G ` is Subgroup of N ) ::_thesis: ( G ` is Subgroup of N implies G ./. N is commutative Group )
proof
assume A1: G ./. N is commutative Group ; ::_thesis: G ` is Subgroup of N
now__::_thesis:_for_a,_b_being_Element_of_G_holds_[.a,b.]_in_N
let a, b be Element of G; ::_thesis: [.a,b.] in N
reconsider S = a * N, T = b * N as Element of (G ./. N) by Th14;
A2: ( [.S,T.] = 1_ (G ./. N) & 1_ (G ./. N) = carr N ) by A1, Th24, GROUP_5:37;
( S " = (a ") * N & T " = (b ") * N ) by Th25;
then A3: (S ") * (T ") = ((a ") * N) * ((b ") * N) by Def3;
( S * T = (a * N) * (b * N) & [.S,T.] = ((S ") * (T ")) * (S * T) ) by Def3, GROUP_5:16;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A3, Def3;
then carr N = (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by A2, GROUP_3:10
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by GROUP_3:117
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by Th5
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:10
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:13
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by GROUP_3:117
.= ((a ") * ((b ") * N)) * ((a * b) * N) by Th5
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:10
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:13
.= ((a ") * (b ")) * (((a * b) * N) * N) by GROUP_3:117
.= ((a ") * (b ")) * ((a * b) * N) by Th5
.= (((a ") * (b ")) * (a * b)) * N by GROUP_2:105
.= [.a,b.] * N by GROUP_5:16 ;
hence [.a,b.] in N by GROUP_2:113; ::_thesis: verum
end;
hence G ` is Subgroup of N by Th7; ::_thesis: verum
end;
assume A4: G ` is Subgroup of N ; ::_thesis: G ./. N is commutative Group
now__::_thesis:_for_S,_T_being_Element_of_(G_./._N)_holds_[.S,T.]_=_1__(G_./._N)
let S, T be Element of (G ./. N); ::_thesis: [.S,T.] = 1_ (G ./. N)
A5: [.S,T.] = ((S ") * (T ")) * (S * T) by GROUP_5:16;
consider b being Element of G such that
A6: T = b * N and
T = N * b by Th13;
A7: T " = (b ") * N by A6, Th25;
consider a being Element of G such that
A8: S = a * N and
S = N * a by Th13;
S " = (a ") * N by A8, Th25;
then A9: (S ") * (T ") = ((a ") * N) * ((b ") * N) by A7, Def3;
[.a,b.] in N by A4, Th7;
then A10: carr N = [.a,b.] * N by GROUP_2:113
.= (((a ") * (b ")) * (a * b)) * N by GROUP_5:16
.= ((a ") * (b ")) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (b ")) * (((a * b) * N) * N) by Th5
.= ((a ") * (b ")) * ((N * (a * b)) * N) by GROUP_3:117
.= ((a ") * (b ")) * (N * ((a * b) * N)) by GROUP_3:13
.= (((a ") * (b ")) * N) * ((a * b) * N) by GROUP_3:10
.= ((a ") * ((b ") * N)) * ((a * b) * N) by GROUP_2:105
.= ((a ") * (((b ") * N) * N)) * ((a * b) * N) by Th5
.= ((a ") * ((N * (b ")) * N)) * ((a * b) * N) by GROUP_3:117
.= ((a ") * (N * ((b ") * N))) * ((a * b) * N) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * ((a * b) * N) by GROUP_3:10
.= (((a ") * N) * ((b ") * N)) * (a * (b * N)) by GROUP_2:105
.= (((a ") * N) * ((b ") * N)) * (a * ((b * N) * N)) by Th5
.= (((a ") * N) * ((b ") * N)) * (a * ((N * b) * N)) by GROUP_3:117
.= (((a ") * N) * ((b ") * N)) * (a * (N * (b * N))) by GROUP_3:13
.= (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by GROUP_3:10 ;
S * T = (a * N) * (b * N) by A8, A6, Def3;
then [.S,T.] = (((a ") * N) * ((b ") * N)) * ((a * N) * (b * N)) by A9, A5, Def3;
hence [.S,T.] = 1_ (G ./. N) by A10, Th24; ::_thesis: verum
end;
hence G ./. N is commutative Group by GROUP_5:37; ::_thesis: verum
end;
Lm1: for G, H being Group
for a, b being Element of G
for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
proof
let G, H be Group; ::_thesis: for a, b being Element of G
for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
let a, b be Element of G; ::_thesis: for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
let f be Function of the carrier of G, the carrier of H; ::_thesis: ( ( for a being Element of G holds f . a = 1_ H ) implies f . (a * b) = (f . a) * (f . b) )
assume A1: for a being Element of G holds f . a = 1_ H ; ::_thesis: f . (a * b) = (f . a) * (f . b)
hence f . (a * b) = 1_ H
.= (1_ H) * (1_ H) by GROUP_1:def_4
.= (f . a) * (1_ H) by A1
.= (f . a) * (f . b) by A1 ;
::_thesis: verum
end;
definition
let G, H be non empty multMagma ;
let f be Function of G,H;
attrf is multiplicative means :Def6: :: GROUP_6:def 6
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);
end;
:: deftheorem Def6 defines multiplicative GROUP_6:def_6_:_
for G, H being non empty multMagma
for f being Function of G,H holds
( f is multiplicative iff for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) );
registration
let G, H be Group;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V22( the carrier of G) quasi_total multiplicative for Element of bool [: the carrier of G, the carrier of H:];
existence
ex b1 being Function of G,H st b1 is multiplicative
proof
take f = the carrier of G --> (1_ H); ::_thesis: f is multiplicative
for a being Element of G holds f . a = 1_ H by FUNCOP_1:7;
hence for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) by Lm1; :: according to GROUP_6:def_6 ::_thesis: verum
end;
end;
definition
let G, H be Group;
mode Homomorphism of G,H is multiplicative Function of G,H;
end;
theorem Th31: :: GROUP_6:31
for G, H being Group
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H
proof
let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds g . (1_ G) = 1_ H
let g be Homomorphism of G,H; ::_thesis: g . (1_ G) = 1_ H
g . (1_ G) = g . ((1_ G) * (1_ G)) by GROUP_1:def_4
.= (g . (1_ G)) * (g . (1_ G)) by Def6 ;
hence g . (1_ G) = 1_ H by GROUP_1:7; ::_thesis: verum
end;
registration
let G, H be Group;
cluster Function-like quasi_total multiplicative -> unity-preserving for Element of bool [: the carrier of G, the carrier of H:];
coherence
for b1 being Homomorphism of G,H holds b1 is unity-preserving
proof
let g be Homomorphism of G,H; ::_thesis: g is unity-preserving
thus g . (1_ G) = 1_ H by Th31; :: according to GROUP_1:def_13 ::_thesis: verum
end;
end;
theorem Th32: :: GROUP_6:32
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "
proof
let G, H be Group; ::_thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "
let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a ") = (g . a) "
let g be Homomorphism of G,H; ::_thesis: g . (a ") = (g . a) "
(g . (a ")) * (g . a) = g . ((a ") * a) by Def6
.= g . (1_ G) by GROUP_1:def_5
.= 1_ H by Th31 ;
hence g . (a ") = (g . a) " by GROUP_1:12; ::_thesis: verum
end;
theorem Th33: :: GROUP_6:33
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
proof
let G, H be Group; ::_thesis: for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
let a, b be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
let g be Homomorphism of G,H; ::_thesis: g . (a |^ b) = (g . a) |^ (g . b)
thus g . (a |^ b) = g . (((b ") * a) * b) by GROUP_3:def_2
.= (g . ((b ") * a)) * (g . b) by Def6
.= ((g . (b ")) * (g . a)) * (g . b) by Def6
.= (((g . b) ") * (g . a)) * (g . b) by Th32
.= (g . a) |^ (g . b) by GROUP_3:def_2 ; ::_thesis: verum
end;
theorem Th34: :: GROUP_6:34
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
proof
let G, H be Group; ::_thesis: for a, b being Element of G
for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
let a, b be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
let g be Homomorphism of G,H; ::_thesis: g . [.a,b.] = [.(g . a),(g . b).]
thus g . [.a,b.] = g . ((((a ") * (b ")) * a) * b) by GROUP_5:16
.= (g . (((a ") * (b ")) * a)) * (g . b) by Def6
.= ((g . ((a ") * (b "))) * (g . a)) * (g . b) by Def6
.= (((g . (a ")) * (g . (b "))) * (g . a)) * (g . b) by Def6
.= ((((g . a) ") * (g . (b "))) * (g . a)) * (g . b) by Th32
.= ((((g . a) ") * ((g . b) ")) * (g . a)) * (g . b) by Th32
.= [.(g . a),(g . b).] by GROUP_5:16 ; ::_thesis: verum
end;
theorem :: GROUP_6:35
for G, H being Group
for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
proof
let G, H be Group; ::_thesis: for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
let a1, a2, a3 be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
let g be Homomorphism of G,H; ::_thesis: g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
thus g . [.a1,a2,a3.] = g . [.[.a1,a2.],a3.] by GROUP_5:def_3
.= [.(g . [.a1,a2.]),(g . a3).] by Th34
.= [.[.(g . a1),(g . a2).],(g . a3).] by Th34
.= [.(g . a1),(g . a2),(g . a3).] by GROUP_5:def_3 ; ::_thesis: verum
end;
theorem Th36: :: GROUP_6:36
for n being Element of NAT
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
proof
let n be Element of NAT ; ::_thesis: for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let G, H be Group; ::_thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let g be Homomorphism of G,H; ::_thesis: g . (a |^ n) = (g . a) |^ n
defpred S1[ Element of NAT ] means g . (a |^ $1) = (g . a) |^ $1;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus g . (a |^ (n + 1)) = g . ((a |^ n) * a) by GROUP_1:34
.= ((g . a) |^ n) * (g . a) by A2, Def6
.= (g . a) |^ (n + 1) by GROUP_1:34 ; ::_thesis: verum
end;
g . (a |^ 0) = g . (1_ G) by GROUP_1:25
.= 1_ H by Th31
.= (g . a) |^ 0 by GROUP_1:25 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence g . (a |^ n) = (g . a) |^ n ; ::_thesis: verum
end;
theorem :: GROUP_6:37
for i being Integer
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
proof
let i be Integer; ::_thesis: for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let G, H be Group; ::_thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let a be Element of G; ::_thesis: for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let g be Homomorphism of G,H; ::_thesis: g . (a |^ i) = (g . a) |^ i
percases ( i >= 0 or i < 0 ) ;
supposeA1: i >= 0 ; ::_thesis: g . (a |^ i) = (g . a) |^ i
hence g . (a |^ i) = g . (a |^ (abs i)) by ABSVALUE:def_1
.= (g . a) |^ (abs i) by Th36
.= (g . a) |^ i by A1, ABSVALUE:def_1 ;
::_thesis: verum
end;
supposeA2: i < 0 ; ::_thesis: g . (a |^ i) = (g . a) |^ i
hence g . (a |^ i) = g . ((a |^ (abs i)) ") by GROUP_1:30
.= (g . (a |^ (abs i))) " by Th32
.= ((g . a) |^ (abs i)) " by Th36
.= (g . a) |^ i by A2, GROUP_1:30 ;
::_thesis: verum
end;
end;
end;
theorem Th38: :: GROUP_6:38
for G being Group holds id the carrier of G is multiplicative
proof
let G be Group; ::_thesis: id the carrier of G is multiplicative
set f = id the carrier of G;
let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b)
let b be Element of G; ::_thesis: (id the carrier of G) . (a * b) = ((id the carrier of G) . a) * ((id the carrier of G) . b)
thus (id the carrier of G) . (a * b) = a * b by FUNCT_1:18
.= ((id the carrier of G) . a) * b by FUNCT_1:18
.= ((id the carrier of G) . a) * ((id the carrier of G) . b) by FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th39: :: GROUP_6:39
for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is multiplicative
proof
let G, H, I be Group; ::_thesis: for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is multiplicative
let h be Homomorphism of G,H; ::_thesis: for h1 being Homomorphism of H,I holds h1 * h is multiplicative
let h1 be Homomorphism of H,I; ::_thesis: h1 * h is multiplicative
set f = h1 * h;
let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b)
let b be Element of G; ::_thesis: (h1 * h) . (a * b) = ((h1 * h) . a) * ((h1 * h) . b)
thus (h1 * h) . (a * b) = h1 . (h . (a * b)) by FUNCT_2:15
.= h1 . ((h . a) * (h . b)) by Def6
.= (h1 . (h . a)) * (h1 . (h . b)) by Def6
.= ((h1 * h) . a) * (h1 . (h . b)) by FUNCT_2:15
.= ((h1 * h) . a) * ((h1 * h) . b) by FUNCT_2:15 ; ::_thesis: verum
end;
registration
let G, H, I be Group;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
clusterh * h1 -> multiplicative for Function of G,I;
coherence
for b1 being Function of G,I st b1 = h1 * h holds
b1 is multiplicative by Th39;
end;
definition
let G, H be Group;
func 1: (G,H) -> Function of G,H means :Def7: :: GROUP_6:def 7
for a being Element of G holds it . a = 1_ H;
existence
ex b1 being Function of G,H st
for a being Element of G holds b1 . a = 1_ H
proof
take the carrier of G --> (1_ H) ; ::_thesis: for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H
thus for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H by FUNCOP_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of G,H st ( for a being Element of G holds b1 . a = 1_ H ) & ( for a being Element of G holds b2 . a = 1_ H ) holds
b1 = b2
proof
let g, h be Function of G,H; ::_thesis: ( ( for a being Element of G holds g . a = 1_ H ) & ( for a being Element of G holds h . a = 1_ H ) implies g = h )
assume that
A1: for a being Element of G holds g . a = 1_ H and
A2: for a being Element of G holds h . a = 1_ H ; ::_thesis: g = h
for a being Element of G holds g . a = h . a
proof
let a be Element of G; ::_thesis: g . a = h . a
g . a = 1_ H by A1;
hence g . a = h . a by A2; ::_thesis: verum
end;
hence g = h by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines 1: GROUP_6:def_7_:_
for G, H being Group
for b3 being Function of G,H holds
( b3 = 1: (G,H) iff for a being Element of G holds b3 . a = 1_ H );
registration
let G, H be Group;
cluster 1: (G,H) -> multiplicative ;
coherence
1: (G,H) is multiplicative
proof
set f = 1: (G,H);
let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b)
let b be Element of G; ::_thesis: (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b)
for a being Element of G holds (1: (G,H)) . a = 1_ H by Def7;
hence (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) by Lm1; ::_thesis: verum
end;
end;
theorem :: GROUP_6:40
for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
proof
let G, H, I be Group; ::_thesis: for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
let h be Homomorphism of G,H; ::_thesis: for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
let h1 be Homomorphism of H,I; ::_thesis: ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
A1: now__::_thesis:_for_a_being_Element_of_G_holds_((1:_(H,I))_*_h)_._a_=_1__I
let a be Element of G; ::_thesis: ((1: (H,I)) * h) . a = 1_ I
thus ((1: (H,I)) * h) . a = (1: (H,I)) . (h . a) by FUNCT_2:15
.= 1_ I by Def7 ; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_G_holds_(h1_*_(1:_(G,H)))_._a_=_1__I
let a be Element of G; ::_thesis: (h1 * (1: (G,H))) . a = 1_ I
thus (h1 * (1: (G,H))) . a = h1 . ((1: (G,H)) . a) by FUNCT_2:15
.= h1 . (1_ H) by Def7
.= 1_ I by Th31 ; ::_thesis: verum
end;
hence ( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) ) by A1, Def7; ::_thesis: verum
end;
definition
let G be Group;
let N be normal Subgroup of G;
func nat_hom N -> Function of G,(G ./. N) means :Def8: :: GROUP_6:def 8
for a being Element of G holds it . a = a * N;
existence
ex b1 being Function of G,(G ./. N) st
for a being Element of G holds b1 . a = a * N
proof
defpred S1[ set , set ] means ex a being Element of G st
( $1 = a & $2 = a * N );
A1: for x being set st x in the carrier of G holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of G implies ex y being set st S1[x,y] )
assume x in the carrier of G ; ::_thesis: ex y being set st S1[x,y]
then reconsider a = x as Element of G ;
reconsider y = a * N as set ;
take y ; ::_thesis: S1[x,y]
take a ; ::_thesis: ( x = a & y = a * N )
thus ( x = a & y = a * N ) ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = the carrier of G and
A3: for x being set st x in the carrier of G holds
S1[x,f . x] from CLASSES1:sch_1(A1);
rng f c= the carrier of (G ./. N)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in the carrier of (G ./. N) )
assume x in rng f ; ::_thesis: x in the carrier of (G ./. N)
then consider y being set such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def_3;
consider a being Element of G such that
y = a and
A6: f . y = a * N by A2, A3, A4;
a * N = N * a by GROUP_3:117;
then x in G ./. N by A5, A6, Th23;
hence x in the carrier of (G ./. N) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider f = f as Function of G,(G ./. N) by A2, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for a being Element of G holds f . a = a * N
let a be Element of G; ::_thesis: f . a = a * N
ex b being Element of G st
( a = b & f . a = b * N ) by A3;
hence f . a = a * N ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of G,(G ./. N) st ( for a being Element of G holds b1 . a = a * N ) & ( for a being Element of G holds b2 . a = a * N ) holds
b1 = b2
proof
let n1, n2 be Function of G,(G ./. N); ::_thesis: ( ( for a being Element of G holds n1 . a = a * N ) & ( for a being Element of G holds n2 . a = a * N ) implies n1 = n2 )
assume that
A7: for a being Element of G holds n1 . a = a * N and
A8: for a being Element of G holds n2 . a = a * N ; ::_thesis: n1 = n2
now__::_thesis:_for_a_being_Element_of_G_holds_n1_._a_=_n2_._a
let a be Element of G; ::_thesis: n1 . a = n2 . a
n1 . a = a * N by A7;
hence n1 . a = n2 . a by A8; ::_thesis: verum
end;
hence n1 = n2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines nat_hom GROUP_6:def_8_:_
for G being Group
for N being normal Subgroup of G
for b3 being Function of G,(G ./. N) holds
( b3 = nat_hom N iff for a being Element of G holds b3 . a = a * N );
registration
let G be Group;
let N be normal Subgroup of G;
cluster nat_hom N -> multiplicative ;
coherence
nat_hom N is multiplicative
proof
set f = nat_hom N;
let a be Element of G; :: according to GROUP_6:def_6 ::_thesis: for b being Element of G holds (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b)
let b be Element of G; ::_thesis: (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b)
A1: (nat_hom N) . a = a * N by Def8;
A2: (nat_hom N) . b = b * N by Def8;
A3: (nat_hom N) . (a * b) = (a * b) * N by Def8;
thus ((nat_hom N) . a) * ((nat_hom N) . b) = (@ ((nat_hom N) . a)) * (@ ((nat_hom N) . b)) by Def3
.= ((a * N) * b) * N by A1, A2, GROUP_3:9
.= (a * (N * b)) * N by GROUP_2:106
.= (a * (b * N)) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= (nat_hom N) . (a * b) by A3, GROUP_2:105 ; ::_thesis: verum
end;
end;
definition
let G, H be Group;
let g be Homomorphism of G,H;
func Ker g -> strict Subgroup of G means :Def9: :: GROUP_6:def 9
the carrier of it = { a where a is Element of G : g . a = 1_ H } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H }
proof
defpred S1[ set ] means g . $1 = 1_ H;
reconsider A = { a where a is Element of G : S1[a] } as Subset of G from DOMAIN_1:sch_7();
A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_A_&_b_in_A_holds_
a_*_b_in_A
let a, b be Element of G; ::_thesis: ( a in A & b in A implies a * b in A )
assume ( a in A & b in A ) ; ::_thesis: a * b in A
then A2: ( ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) & ex b1 being Element of G st
( b1 = b & g . b1 = 1_ H ) ) ;
g . (a * b) = (g . a) * (g . b) by Def6
.= 1_ H by A2, GROUP_1:def_4 ;
hence a * b in A ; ::_thesis: verum
end;
A3: now__::_thesis:_for_a_being_Element_of_G_st_a_in_A_holds_
a_"_in_A
let a be Element of G; ::_thesis: ( a in A implies a " in A )
assume a in A ; ::_thesis: a " in A
then ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) ;
then g . (a ") = (1_ H) " by Th32
.= 1_ H by GROUP_1:8 ;
hence a " in A ; ::_thesis: verum
end;
g . (1_ G) = 1_ H by Th31;
then 1_ G in A ;
then consider B being strict Subgroup of G such that
A4: the carrier of B = A by A1, A3, GROUP_2:52;
reconsider B = B as strict Subgroup of G ;
take B ; ::_thesis: the carrier of B = { a where a is Element of G : g . a = 1_ H }
thus the carrier of B = { a where a is Element of G : g . a = 1_ H } by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } & the carrier of b2 = { a where a is Element of G : g . a = 1_ H } holds
b1 = b2 by GROUP_2:59;
end;
:: deftheorem Def9 defines Ker GROUP_6:def_9_:_
for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of G holds
( b4 = Ker g iff the carrier of b4 = { a where a is Element of G : g . a = 1_ H } );
registration
let G, H be Group;
let g be Homomorphism of G,H;
cluster Ker g -> strict normal ;
coherence
Ker g is normal
proof
defpred S1[ set ] means g . G = 1_ H;
reconsider A = { a where a is Element of G : S1[a] } as Subset of G from DOMAIN_1:sch_7();
A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_A_&_b_in_A_holds_
a_*_b_in_A
let a, b be Element of G; ::_thesis: ( a in A & b in A implies a * b in A )
assume ( a in A & b in A ) ; ::_thesis: a * b in A
then A2: ( ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) & ex b1 being Element of G st
( b1 = b & g . b1 = 1_ H ) ) ;
g . (a * b) = (g . a) * (g . b) by Def6
.= 1_ H by A2, GROUP_1:def_4 ;
hence a * b in A ; ::_thesis: verum
end;
A3: now__::_thesis:_for_a_being_Element_of_G_st_a_in_A_holds_
a_"_in_A
let a be Element of G; ::_thesis: ( a in A implies a " in A )
assume a in A ; ::_thesis: a " in A
then ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) ;
then g . (a ") = (1_ H) " by Th32
.= 1_ H by GROUP_1:8 ;
hence a " in A ; ::_thesis: verum
end;
g . (1_ G) = 1_ H by Th31;
then 1_ G in A ;
then consider B being strict Subgroup of G such that
A4: the carrier of B = A by A1, A3, GROUP_2:52;
now__::_thesis:_for_a_being_Element_of_G_holds_B_|^_a_is_Subgroup_of_B
let a be Element of G; ::_thesis: B |^ a is Subgroup of B
now__::_thesis:_for_b_being_Element_of_G_st_b_in_B_|^_a_holds_
b_in_B
let b be Element of G; ::_thesis: ( b in B |^ a implies b in B )
assume b in B |^ a ; ::_thesis: b in B
then consider c being Element of G such that
A5: b = c |^ a and
A6: c in B by GROUP_3:58;
c in A by A4, A6, STRUCT_0:def_5;
then ex a1 being Element of G st
( c = a1 & g . a1 = 1_ H ) ;
then g . b = (1_ H) |^ (g . a) by A5, Th33
.= 1_ H by GROUP_3:17 ;
then b in A ;
hence b in B by A4, STRUCT_0:def_5; ::_thesis: verum
end;
hence B |^ a is Subgroup of B by GROUP_2:58; ::_thesis: verum
end;
then B is normal Subgroup of G by GROUP_3:122;
hence Ker g is normal by A4, Def9; ::_thesis: verum
end;
end;
theorem Th41: :: GROUP_6:41
for G, H being Group
for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
proof
let G, H be Group; ::_thesis: for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
let a be Element of G; ::_thesis: for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
let h be Homomorphism of G,H; ::_thesis: ( a in Ker h iff h . a = 1_ H )
thus ( a in Ker h implies h . a = 1_ H ) ::_thesis: ( h . a = 1_ H implies a in Ker h )
proof
assume a in Ker h ; ::_thesis: h . a = 1_ H
then a in the carrier of (Ker h) by STRUCT_0:def_5;
then a in { b where b is Element of G : h . b = 1_ H } by Def9;
then ex b being Element of G st
( a = b & h . b = 1_ H ) ;
hence h . a = 1_ H ; ::_thesis: verum
end;
assume h . a = 1_ H ; ::_thesis: a in Ker h
then a in { b where b is Element of G : h . b = 1_ H } ;
then a in the carrier of (Ker h) by Def9;
hence a in Ker h by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: GROUP_6:42
for G, H being strict Group holds Ker (1: (G,H)) = G
proof
let G, H be strict Group; ::_thesis: Ker (1: (G,H)) = G
now__::_thesis:_for_a_being_Element_of_G_holds_a_in_Ker_(1:_(G,H))
let a be Element of G; ::_thesis: a in Ker (1: (G,H))
(1: (G,H)) . a = 1_ H by Def7;
hence a in Ker (1: (G,H)) by Th41; ::_thesis: verum
end;
hence Ker (1: (G,H)) = G by GROUP_2:62; ::_thesis: verum
end;
theorem Th43: :: GROUP_6:43
for G being Group
for N being strict normal Subgroup of G holds Ker (nat_hom N) = N
proof
let G be Group; ::_thesis: for N being strict normal Subgroup of G holds Ker (nat_hom N) = N
let N be strict normal Subgroup of G; ::_thesis: Ker (nat_hom N) = N
let a be Element of G; :: according to GROUP_2:def_6 ::_thesis: ( ( not a in Ker (nat_hom N) or a in N ) & ( not a in N or a in Ker (nat_hom N) ) )
thus ( a in Ker (nat_hom N) implies a in N ) ::_thesis: ( not a in N or a in Ker (nat_hom N) )
proof
assume a in Ker (nat_hom N) ; ::_thesis: a in N
then A1: (nat_hom N) . a = 1_ (G ./. N) by Th41;
( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24;
hence a in N by A1, GROUP_2:113; ::_thesis: verum
end;
assume a in N ; ::_thesis: a in Ker (nat_hom N)
then A2: a * N = carr N by GROUP_2:113;
( (nat_hom N) . a = a * N & 1_ (G ./. N) = carr N ) by Def8, Th24;
hence a in Ker (nat_hom N) by A2, Th41; ::_thesis: verum
end;
definition
let G, H be Group;
let g be Homomorphism of G,H;
func Image g -> strict Subgroup of H means :Def10: :: GROUP_6:def 10
the carrier of it = g .: the carrier of G;
existence
ex b1 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G
proof
the carrier of G c= the carrier of G ;
then reconsider X = the carrier of G as Subset of G ;
set S = g .: X;
A1: now__::_thesis:_for_c,_d_being_Element_of_H_st_c_in_g_.:_X_&_d_in_g_.:_X_holds_
c_*_d_in_g_.:_X
let c, d be Element of H; ::_thesis: ( c in g .: X & d in g .: X implies c * d in g .: X )
assume that
A2: c in g .: X and
A3: d in g .: X ; ::_thesis: c * d in g .: X
consider b being Element of G such that
b in X and
A4: d = g . b by A3, FUNCT_2:65;
consider a being Element of G such that
a in X and
A5: c = g . a by A2, FUNCT_2:65;
c * d = g . (a * b) by A5, A4, Def6;
hence c * d in g .: X by FUNCT_2:35; ::_thesis: verum
end;
A6: now__::_thesis:_for_c_being_Element_of_H_st_c_in_g_.:_X_holds_
c_"_in_g_.:_X
let c be Element of H; ::_thesis: ( c in g .: X implies c " in g .: X )
assume c in g .: X ; ::_thesis: c " in g .: X
then consider a being Element of G such that
a in X and
A7: c = g . a by FUNCT_2:65;
g . (a ") = c " by A7, Th32;
hence c " in g .: X by FUNCT_2:35; ::_thesis: verum
end;
dom g = the carrier of G by FUNCT_2:def_1;
then consider D being strict Subgroup of H such that
A8: the carrier of D = g .: X by A1, A6, GROUP_2:52;
take D ; ::_thesis: the carrier of D = g .: the carrier of G
thus the carrier of D = g .: the carrier of G by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds
b1 = b2 by GROUP_2:59;
end;
:: deftheorem Def10 defines Image GROUP_6:def_10_:_
for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of H holds
( b4 = Image g iff the carrier of b4 = g .: the carrier of G );
theorem Th44: :: GROUP_6:44
for G, H being Group
for g being Homomorphism of G,H holds rng g = the carrier of (Image g)
proof
let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds rng g = the carrier of (Image g)
let g be Homomorphism of G,H; ::_thesis: rng g = the carrier of (Image g)
the carrier of (Image g) = g .: the carrier of G by Def10
.= g .: (dom g) by FUNCT_2:def_1
.= rng g by RELAT_1:113 ;
hence rng g = the carrier of (Image g) ; ::_thesis: verum
end;
theorem Th45: :: GROUP_6:45
for H, G being Group
for x being set
for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
proof
let H, G be Group; ::_thesis: for x being set
for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
let x be set ; ::_thesis: for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
let g be Homomorphism of G,H; ::_thesis: ( x in Image g iff ex a being Element of G st x = g . a )
thus ( x in Image g implies ex a being Element of G st x = g . a ) ::_thesis: ( ex a being Element of G st x = g . a implies x in Image g )
proof
assume x in Image g ; ::_thesis: ex a being Element of G st x = g . a
then x in the carrier of (Image g) by STRUCT_0:def_5;
then x in g .: the carrier of G by Def10;
then consider y being set such that
y in dom g and
A1: y in the carrier of G and
A2: g . y = x by FUNCT_1:def_6;
reconsider y = y as Element of G by A1;
take y ; ::_thesis: x = g . y
thus x = g . y by A2; ::_thesis: verum
end;
given a being Element of G such that A3: x = g . a ; ::_thesis: x in Image g
the carrier of G = dom g by FUNCT_2:def_1;
then x in g .: the carrier of G by A3, FUNCT_1:def_6;
then x in the carrier of (Image g) by Def10;
hence x in Image g by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: GROUP_6:46
for G, H being Group
for g being Homomorphism of G,H holds Image g = gr (rng g)
proof
let G, H be Group; ::_thesis: for g being Homomorphism of G,H holds Image g = gr (rng g)
let g be Homomorphism of G,H; ::_thesis: Image g = gr (rng g)
( rng g = the carrier of (Image g) & the carrier of (Image g) = carr (Image g) ) by Th44;
hence Image g = gr (rng g) by GROUP_4:31; ::_thesis: verum
end;
theorem :: GROUP_6:47
for G, H being Group holds Image (1: (G,H)) = (1). H
proof
let G, H be Group; ::_thesis: Image (1: (G,H)) = (1). H
set g = 1: (G,H);
A1: the carrier of (Image (1: (G,H))) c= {(1_ H)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image (1: (G,H))) or x in {(1_ H)} )
assume x in the carrier of (Image (1: (G,H))) ; ::_thesis: x in {(1_ H)}
then x in (1: (G,H)) .: the carrier of G by Def10;
then consider y being set such that
y in dom (1: (G,H)) and
A2: y in the carrier of G and
A3: (1: (G,H)) . y = x by FUNCT_1:def_6;
reconsider y = y as Element of G by A2;
(1: (G,H)) . y = 1_ H by Def7;
hence x in {(1_ H)} by A3, TARSKI:def_1; ::_thesis: verum
end;
1_ H in Image (1: (G,H)) by GROUP_2:46;
then 1_ H in the carrier of (Image (1: (G,H))) by STRUCT_0:def_5;
then {(1_ H)} c= the carrier of (Image (1: (G,H))) by ZFMISC_1:31;
then the carrier of (Image (1: (G,H))) = {(1_ H)} by A1, XBOOLE_0:def_10;
hence Image (1: (G,H)) = (1). H by GROUP_2:def_7; ::_thesis: verum
end;
theorem Th48: :: GROUP_6:48
for G being Group
for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N
proof
let G be Group; ::_thesis: for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N
let N be normal Subgroup of G; ::_thesis: Image (nat_hom N) = G ./. N
now__::_thesis:_for_S_being_Element_of_(G_./._N)_holds_S_in_Image_(nat_hom_N)
let S be Element of (G ./. N); ::_thesis: S in Image (nat_hom N)
consider a being Element of G such that
A1: S = a * N and
S = N * a by Th13;
(nat_hom N) . a = a * N by Def8;
hence S in Image (nat_hom N) by A1, Th45; ::_thesis: verum
end;
hence Image (nat_hom N) = G ./. N by GROUP_2:62; ::_thesis: verum
end;
theorem Th49: :: GROUP_6:49
for H, G being Group
for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h)
proof
let H, G be Group; ::_thesis: for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h)
let h be Homomorphism of G,H; ::_thesis: h is Homomorphism of G,(Image h)
( rng h = the carrier of (Image h) & dom h = the carrier of G ) by Th44, FUNCT_2:def_1;
then reconsider f9 = h as Function of G,(Image h) by RELSET_1:4;
now__::_thesis:_for_a,_b_being_Element_of_G_holds_(f9_._a)_*_(f9_._b)_=_f9_._(a_*_b)
let a, b be Element of G; ::_thesis: (f9 . a) * (f9 . b) = f9 . (a * b)
thus (f9 . a) * (f9 . b) = (h . a) * (h . b) by GROUP_2:43
.= f9 . (a * b) by Def6 ; ::_thesis: verum
end;
hence h is Homomorphism of G,(Image h) by Def6; ::_thesis: verum
end;
theorem Th50: :: GROUP_6:50
for H, G being Group
for g being Homomorphism of G,H st G is finite holds
Image g is finite
proof
let H, G be Group; ::_thesis: for g being Homomorphism of G,H st G is finite holds
Image g is finite
let g be Homomorphism of G,H; ::_thesis: ( G is finite implies Image g is finite )
assume G is finite ; ::_thesis: Image g is finite
then g .: the carrier of G is finite ;
hence Image g is finite by Def10; ::_thesis: verum
end;
registration
let G be finite Group;
let H be Group;
let g be Homomorphism of G,H;
cluster Image g -> finite strict ;
coherence
Image g is finite by Th50;
end;
Lm2: for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
theorem :: GROUP_6:51
for H, G being Group
for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative
proof
let H, G be Group; ::_thesis: for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative
let g be Homomorphism of G,H; ::_thesis: ( G is commutative Group implies Image g is commutative )
assume A1: G is commutative Group ; ::_thesis: Image g is commutative
let h1, h2 be Element of (Image g); :: according to GROUP_1:def_12 ::_thesis: h1 * h2 = h2 * h1
reconsider c = h1, d = h2 as Element of H by GROUP_2:42;
h1 in Image g by STRUCT_0:def_5;
then consider a being Element of G such that
A2: h1 = g . a by Th45;
h2 in Image g by STRUCT_0:def_5;
then consider b being Element of G such that
A3: h2 = g . b by Th45;
thus h1 * h2 = c * d by GROUP_2:43
.= g . (a * b) by A2, A3, Def6
.= g . (b * a) by A1, Lm2
.= d * c by A2, A3, Def6
.= h2 * h1 by GROUP_2:43 ; ::_thesis: verum
end;
theorem Th52: :: GROUP_6:52
for H, G being Group
for g being Homomorphism of G,H holds card (Image g) c= card G
proof
let H, G be Group; ::_thesis: for g being Homomorphism of G,H holds card (Image g) c= card G
let g be Homomorphism of G,H; ::_thesis: card (Image g) c= card G
card (g .: the carrier of G) c= card the carrier of G by CARD_1:67;
hence card (Image g) c= card G by Def10; ::_thesis: verum
end;
theorem :: GROUP_6:53
for G being finite Group
for H being Group
for g being Homomorphism of G,H holds card (Image g) <= card G
proof
let G be finite Group; ::_thesis: for H being Group
for g being Homomorphism of G,H holds card (Image g) <= card G
let H be Group; ::_thesis: for g being Homomorphism of G,H holds card (Image g) <= card G
let g be Homomorphism of G,H; ::_thesis: card (Image g) <= card G
card (Image g) c= card G by Th52;
hence card (Image g) <= card G by NAT_1:39; ::_thesis: verum
end;
theorem :: GROUP_6:54
for G, H being Group
for c being Element of H
for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
proof
let G, H be Group; ::_thesis: for c being Element of H
for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
let c be Element of H; ::_thesis: for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one & c in Image h implies h . ((h ") . c) = c )
reconsider h9 = h as Function of G,(Image h) by Th49;
assume that
A1: h is one-to-one and
A2: c in Image h ; ::_thesis: h . ((h ") . c) = c
A3: rng h9 = the carrier of (Image h) by Th44;
c in the carrier of (Image h) by A2, STRUCT_0:def_5;
hence h . ((h ") . c) = c by A1, A3, FUNCT_1:35; ::_thesis: verum
end;
theorem Th55: :: GROUP_6:55
for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (Image h),G
proof
let H, G be Group; ::_thesis: for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (Image h),G
let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one implies h " is Homomorphism of (Image h),G )
assume A1: h is one-to-one ; ::_thesis: h " is Homomorphism of (Image h),G
reconsider Imh = Image h as Group ;
( h is Function of G,Imh & rng h = the carrier of Imh ) by Th44, Th49;
then reconsider h9 = h " as Function of Imh,G by A1, FUNCT_2:25;
now__::_thesis:_for_a,_b_being_Element_of_Imh_holds_h9_._(a_*_b)_=_(h9_._a)_*_(h9_._b)
let a, b be Element of Imh; ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b)
reconsider a9 = a, b9 = b as Element of H by GROUP_2:42;
a9 in Imh by STRUCT_0:def_5;
then consider a1 being Element of G such that
A2: h . a1 = a9 by Th45;
b9 in Imh by STRUCT_0:def_5;
then consider b1 being Element of G such that
A3: h . b1 = b9 by Th45;
thus h9 . (a * b) = h9 . ((h . a1) * (h . b1)) by A2, A3, GROUP_2:43
.= h9 . (h . (a1 * b1)) by Def6
.= a1 * b1 by A1, FUNCT_2:26
.= (h9 . a) * b1 by A1, A2, FUNCT_2:26
.= (h9 . a) * (h9 . b) by A1, A3, FUNCT_2:26 ; ::_thesis: verum
end;
hence h " is Homomorphism of (Image h),G by Def6; ::_thesis: verum
end;
theorem Th56: :: GROUP_6:56
for H, G being Group
for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )
proof
let H, G be Group; ::_thesis: for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )
let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one iff Ker h = (1). G )
thus ( h is one-to-one implies Ker h = (1). G ) ::_thesis: ( Ker h = (1). G implies h is one-to-one )
proof
assume A1: h is one-to-one ; ::_thesis: Ker h = (1). G
now__::_thesis:_for_x_being_set_holds_
(_x_in_the_carrier_of_(Ker_h)_iff_x_=_1__G_)
let x be set ; ::_thesis: ( x in the carrier of (Ker h) iff x = 1_ G )
thus ( x in the carrier of (Ker h) iff x = 1_ G ) ::_thesis: verum
proof
thus ( x in the carrier of (Ker h) implies x = 1_ G ) ::_thesis: ( x = 1_ G implies x in the carrier of (Ker h) )
proof
assume A2: x in the carrier of (Ker h) ; ::_thesis: x = 1_ G
then x in Ker h by STRUCT_0:def_5;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def_5;
a in Ker h by A2, STRUCT_0:def_5;
then h . a = 1_ H by Th41
.= h . (1_ G) by Th31 ;
hence x = 1_ G by A1, Th1; ::_thesis: verum
end;
assume A3: x = 1_ G ; ::_thesis: x in the carrier of (Ker h)
then reconsider a = x as Element of G ;
h . a = 1_ H by A3, Th31;
then a in Ker h by Th41;
hence x in the carrier of (Ker h) by STRUCT_0:def_5; ::_thesis: verum
end;
end;
then the carrier of (Ker h) = {(1_ G)} by TARSKI:def_1;
hence Ker h = (1). G by GROUP_2:def_7; ::_thesis: verum
end;
assume Ker h = (1). G ; ::_thesis: h is one-to-one
then A4: the carrier of (Ker h) = {(1_ G)} by GROUP_2:def_7;
now__::_thesis:_for_a,_b_being_Element_of_G_st_a_<>_b_holds_
not_h_._a_=_h_._b
let a, b be Element of G; ::_thesis: ( a <> b implies not h . a = h . b )
assume that
A5: a <> b and
A6: h . a = h . b ; ::_thesis: contradiction
(h . a) * (h . (a ")) = h . (a * (a ")) by Def6
.= h . (1_ G) by GROUP_1:def_5
.= 1_ H by Th31 ;
then 1_ H = h . (b * (a ")) by A6, Def6;
then b * (a ") in Ker h by Th41;
then A7: b * (a ") in the carrier of (Ker h) by STRUCT_0:def_5;
a = (1_ G) * a by GROUP_1:def_4
.= (b * (a ")) * a by A4, A7, TARSKI:def_1
.= b * ((a ") * a) by GROUP_1:def_3
.= b * (1_ G) by GROUP_1:def_5
.= b by GROUP_1:def_4 ;
hence contradiction by A5; ::_thesis: verum
end;
then for a, b being Element of G st h . a = h . b holds
a = b ;
hence h is one-to-one by Th1; ::_thesis: verum
end;
theorem Th57: :: GROUP_6:57
for G being Group
for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
proof
let G be Group; ::_thesis: for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let H be strict Group; ::_thesis: for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let h be Homomorphism of G,H; ::_thesis: ( h is onto iff Image h = H )
thus ( h is onto implies Image h = H ) ::_thesis: ( Image h = H implies h is onto )
proof
assume rng h = the carrier of H ; :: according to FUNCT_2:def_3 ::_thesis: Image h = H
then the carrier of (Image h) = the carrier of H by Th44;
hence Image h = H by GROUP_2:61; ::_thesis: verum
end;
assume A1: Image h = H ; ::_thesis: h is onto
the carrier of H c= rng h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in rng h )
assume x in the carrier of H ; ::_thesis: x in rng h
then x in h .: the carrier of G by A1, Def10;
then ex y being set st
( y in dom h & y in the carrier of G & h . y = x ) by FUNCT_1:def_6;
hence x in rng h by FUNCT_1:def_3; ::_thesis: verum
end;
then rng h = the carrier of H by XBOOLE_0:def_10;
hence h is onto by FUNCT_2:def_3; ::_thesis: verum
end;
theorem Th58: :: GROUP_6:58
for G, H being non empty set
for h being Function of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c
proof
let G, H be non empty set ; ::_thesis: for h being Function of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c
let h be Function of G,H; ::_thesis: ( h is onto implies for c being Element of H ex a being Element of G st h . a = c )
assume A1: rng h = H ; :: according to FUNCT_2:def_3 ::_thesis: for c being Element of H ex a being Element of G st h . a = c
let c be Element of H; ::_thesis: ex a being Element of G st h . a = c
ex a being set st
( a in G & h . a = c ) by A1, FUNCT_2:11;
hence ex a being Element of G st h . a = c ; ::_thesis: verum
end;
theorem Th59: :: GROUP_6:59
for G being Group
for N being normal Subgroup of G holds nat_hom N is onto
proof
let G be Group; ::_thesis: for N being normal Subgroup of G holds nat_hom N is onto
let N be normal Subgroup of G; ::_thesis: nat_hom N is onto
Image (nat_hom N) = G ./. N by Th48;
hence nat_hom N is onto by Th57; ::_thesis: verum
end;
theorem Th60: :: GROUP_6:60
for G, H being set
for h being Function of G,H holds
( h is bijective iff ( rng h = H & h is one-to-one ) )
proof
let G, H be set ; ::_thesis: for h being Function of G,H holds
( h is bijective iff ( rng h = H & h is one-to-one ) )
let h be Function of G,H; ::_thesis: ( h is bijective iff ( rng h = H & h is one-to-one ) )
thus ( h is bijective implies ( rng h = H & h is one-to-one ) ) by FUNCT_2:def_3; ::_thesis: ( rng h = H & h is one-to-one implies h is bijective )
assume ( rng h = H & h is one-to-one ) ; ::_thesis: h is bijective
hence ( h is one-to-one & h is onto ) by FUNCT_2:def_3; :: according to FUNCT_2:def_4 ::_thesis: verum
end;
theorem :: GROUP_6:61
for G being set
for H being non empty set
for h being Function of G,H st h is bijective holds
( dom h = G & rng h = H ) by FUNCT_2:def_1, FUNCT_2:def_3;
theorem Th62: :: GROUP_6:62
for G being Group
for H being strict Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
proof
let G be Group; ::_thesis: for H being strict Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
let H be strict Group; ::_thesis: for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
let h be Homomorphism of G,H; ::_thesis: ( h is bijective implies h " is Homomorphism of H,G )
assume A1: ( h is one-to-one & h is onto ) ; :: according to FUNCT_2:def_4 ::_thesis: h " is Homomorphism of H,G
then H = Image h by Th57;
hence h " is Homomorphism of H,G by A1, Th55; ::_thesis: verum
end;
theorem Th63: :: GROUP_6:63
for G being set
for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
proof
let G be set ; ::_thesis: for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let H be non empty set ; ::_thesis: for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let h be Function of G,H; ::_thesis: for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
let g1 be Function of H,G; ::_thesis: ( h is bijective & g1 = h " implies g1 is bijective )
assume A1: ( h is bijective & g1 = h " ) ; ::_thesis: g1 is bijective
then ( dom h = G & rng g1 = dom h ) by FUNCT_1:33, FUNCT_2:def_1;
hence g1 is bijective by A1, Th60; ::_thesis: verum
end;
theorem Th64: :: GROUP_6:64
for G being set
for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
proof
let G be set ; ::_thesis: for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let H, I be non empty set ; ::_thesis: for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h be Function of G,H; ::_thesis: for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
let h1 be Function of H,I; ::_thesis: ( h is bijective & h1 is bijective implies h1 * h is bijective )
assume that
A1: h is bijective and
A2: h1 is bijective ; ::_thesis: h1 * h is bijective
( dom h1 = H & rng h = H ) by A1, Th60, FUNCT_2:def_1;
then rng (h1 * h) = rng h1 by RELAT_1:28
.= I by A2, Th60 ;
hence h1 * h is bijective by A1, A2, Th60; ::_thesis: verum
end;
theorem Th65: :: GROUP_6:65
for G being Group holds nat_hom ((1). G) is bijective
proof
let G be Group; ::_thesis: nat_hom ((1). G) is bijective
set g = nat_hom ((1). G);
Ker (nat_hom ((1). G)) = (1). G by Th43;
then A1: nat_hom ((1). G) is one-to-one by Th56;
nat_hom ((1). G) is onto by Th59;
hence nat_hom ((1). G) is bijective by A1; ::_thesis: verum
end;
definition
let G, H be Group;
predG,H are_isomorphic means :Def11: :: GROUP_6:def 11
ex h being Homomorphism of G,H st h is bijective ;
reflexivity
for G being Group ex h being Homomorphism of G,G st h is bijective
proof
let G be Group; ::_thesis: ex h being Homomorphism of G,G st h is bijective
reconsider i = id the carrier of G as Homomorphism of G,G by Th38;
i is bijective ;
hence ex h being Homomorphism of G,G st h is bijective ; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines are_isomorphic GROUP_6:def_11_:_
for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );
theorem Th66: :: GROUP_6:66
for G, H being strict Group st G,H are_isomorphic holds
H,G are_isomorphic
proof
let G, H be strict Group; ::_thesis: ( G,H are_isomorphic implies H,G are_isomorphic )
assume G,H are_isomorphic ; ::_thesis: H,G are_isomorphic
then consider h being Homomorphism of G,H such that
A1: h is bijective by Def11;
reconsider g = h " as Homomorphism of H,G by A1, Th62;
take g ; :: according to GROUP_6:def_11 ::_thesis: g is bijective
thus g is bijective by A1, Th63; ::_thesis: verum
end;
definition
let G, H be strict Group;
:: original: are_isomorphic
redefine predG,H are_isomorphic ;
symmetry
for G, H being strict Group st (b1,b2) holds
(b2,b1) by Th66;
end;
theorem :: GROUP_6:67
for G, H, I being Group st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic
proof
let G, H, I be Group; ::_thesis: ( G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic )
assume that
A1: G,H are_isomorphic and
A2: H,I are_isomorphic ; ::_thesis: G,I are_isomorphic
consider g being Homomorphism of G,H such that
A3: g is bijective by A1, Def11;
consider h1 being Homomorphism of H,I such that
A4: h1 is bijective by A2, Def11;
h1 * g is bijective by A3, A4, Th64;
hence G,I are_isomorphic by Def11; ::_thesis: verum
end;
theorem :: GROUP_6:68
for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic
proof
let H, G be Group; ::_thesis: for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic
let h be Homomorphism of G,H; ::_thesis: ( h is one-to-one implies G, Image h are_isomorphic )
reconsider ih = h as Homomorphism of G,(Image h) by Th49;
assume A1: h is one-to-one ; ::_thesis: G, Image h are_isomorphic
take ih ; :: according to GROUP_6:def_11 ::_thesis: ih is bijective
the carrier of (Image h) = rng ih by Th44;
then ih is onto by FUNCT_2:def_3;
hence ih is bijective by A1; ::_thesis: verum
end;
theorem Th69: :: GROUP_6:69
for G, H being strict Group st G is trivial & H is trivial holds
G,H are_isomorphic
proof
let G, H be strict Group; ::_thesis: ( G is trivial & H is trivial implies G,H are_isomorphic )
assume that
A1: G is trivial and
A2: H is trivial ; ::_thesis: G,H are_isomorphic
take 1: (G,H) ; :: according to GROUP_6:def_11 ::_thesis: 1: (G,H) is bijective
A3: H = (1). H by A2, Th12;
set h = 1: (G,H);
A4: G = (1). G by A1, Th12;
now__::_thesis:_for_a,_b_being_Element_of_G_st_(1:_(G,H))_._a_=_(1:_(G,H))_._b_holds_
a_=_b
let a, b be Element of G; ::_thesis: ( (1: (G,H)) . a = (1: (G,H)) . b implies a = b )
assume (1: (G,H)) . a = (1: (G,H)) . b ; ::_thesis: a = b
a in the carrier of ((1). G) by A4;
then a in {(1_ G)} by GROUP_2:def_7;
then A5: a = 1_ G by TARSKI:def_1;
b in the carrier of ((1). G) by A4;
then b in {(1_ G)} by GROUP_2:def_7;
hence a = b by A5, TARSKI:def_1; ::_thesis: verum
end;
then A6: 1: (G,H) is one-to-one by Th1;
the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7;
then rng (1: (G,H)) = {((1: (G,H)) . (1_ G))} by A4, FUNCT_2:48
.= {(1_ H)} by Def7
.= the carrier of ((1). H) by GROUP_2:def_7 ;
then 1: (G,H) is onto by A3, FUNCT_2:def_3;
hence 1: (G,H) is bijective by A6; ::_thesis: verum
end;
theorem :: GROUP_6:70
for G, H being Group holds (1). G, (1). H are_isomorphic by Th69;
theorem :: GROUP_6:71
for G being strict Group holds G,G ./. ((1). G) are_isomorphic
proof
let G be strict Group; ::_thesis: G,G ./. ((1). G) are_isomorphic
nat_hom ((1). G) is bijective by Th65;
hence G,G ./. ((1). G) are_isomorphic by Def11; ::_thesis: verum
end;
theorem :: GROUP_6:72
for G being Group holds G ./. ((Omega). G) is trivial
proof
let G be Group; ::_thesis: G ./. ((Omega). G) is trivial
the carrier of (G ./. ((Omega). G)) = { the carrier of G} by GROUP_2:142;
hence G ./. ((Omega). G) is trivial by Def2; ::_thesis: verum
end;
theorem Th73: :: GROUP_6:73
for G, H being strict Group st G,H are_isomorphic holds
card G = card H
proof
let G, H be strict Group; ::_thesis: ( G,H are_isomorphic implies card G = card H )
assume A1: G,H are_isomorphic ; ::_thesis: card G = card H
then consider h being Homomorphism of G,H such that
A2: h is bijective by Def11;
consider g1 being Homomorphism of H,G such that
A3: g1 is bijective by A1, Def11;
Image g1 = G by A3, Th57;
then A4: card G c= card H by Th52;
Image h = H by A2, Th57;
then card H c= card G by Th52;
hence card G = card H by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th74: :: GROUP_6:74
for G, H being Group st G,H are_isomorphic & G is finite holds
H is finite
proof
let G, H be Group; ::_thesis: ( G,H are_isomorphic & G is finite implies H is finite )
assume that
A1: G,H are_isomorphic and
A2: G is finite ; ::_thesis: H is finite
consider h being Homomorphism of G,H such that
A3: h is bijective by A1, Def11;
rng h = the carrier of H by A3, FUNCT_2:def_3;
hence H is finite by A2; ::_thesis: verum
end;
theorem :: GROUP_6:75
for G, H being strict Group st G,H are_isomorphic & G is finite holds
card G = card H by Th73;
theorem :: GROUP_6:76
for G being trivial strict Group
for H being strict Group st G,H are_isomorphic holds
H is trivial
proof
let G be trivial strict Group; ::_thesis: for H being strict Group st G,H are_isomorphic holds
H is trivial
let H be strict Group; ::_thesis: ( G,H are_isomorphic implies H is trivial )
assume A1: G,H are_isomorphic ; ::_thesis: H is trivial
then reconsider H = H as finite Group by Th74;
card G = 1 by Th11;
then card H = 1 by A1, Th73;
hence H is trivial by Th11; ::_thesis: verum
end;
theorem :: GROUP_6:77
for G being Group
for H being strict Group st G,H are_isomorphic & G is commutative holds
H is commutative
proof
let G be Group; ::_thesis: for H being strict Group st G,H are_isomorphic & G is commutative holds
H is commutative
let H be strict Group; ::_thesis: ( G,H are_isomorphic & G is commutative implies H is commutative )
assume that
A1: G,H are_isomorphic and
A2: G is commutative ; ::_thesis: H is commutative
consider h being Homomorphism of G,H such that
A3: h is bijective by A1, Def11;
now__::_thesis:_for_c,_d_being_Element_of_H_holds_c_*_d_=_d_*_c
let c, d be Element of H; ::_thesis: c * d = d * c
consider a being Element of G such that
A4: h . a = c by A3, Th58;
consider b being Element of G such that
A5: h . b = d by A3, Th58;
thus c * d = h . (a * b) by A4, A5, Def6
.= h . (b * a) by A2, Lm2
.= d * c by A4, A5, Def6 ; ::_thesis: verum
end;
hence H is commutative by GROUP_1:def_12; ::_thesis: verum
end;
Lm3: for H, G being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
proof
let H, G be Group; ::_thesis: for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
let g be Homomorphism of G,H; ::_thesis: ( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
set I = G ./. (Ker g);
set J = Image g;
defpred S1[ set , set ] means for a being Element of G st $1 = a * (Ker g) holds
$2 = g . a;
A1: dom (nat_hom (Ker g)) = the carrier of G by FUNCT_2:def_1;
A2: for S being Element of (G ./. (Ker g)) ex T being Element of (Image g) st S1[S,T]
proof
let S be Element of (G ./. (Ker g)); ::_thesis: ex T being Element of (Image g) st S1[S,T]
consider a being Element of G such that
A3: S = a * (Ker g) and
S = (Ker g) * a by Th13;
g . a in Image g by Th45;
then reconsider T = g . a as Element of (Image g) by STRUCT_0:def_5;
take T ; ::_thesis: S1[S,T]
let b be Element of G; ::_thesis: ( S = b * (Ker g) implies T = g . b )
assume S = b * (Ker g) ; ::_thesis: T = g . b
then (a ") * b in Ker g by A3, GROUP_2:114;
then 1_ H = g . ((a ") * b) by Th41
.= (g . (a ")) * (g . b) by Def6
.= ((g . a) ") * (g . b) by Th32 ;
then g . b = ((g . a) ") " by GROUP_1:12;
hence T = g . b ; ::_thesis: verum
end;
consider f being Function of (G ./. (Ker g)),(Image g) such that
A4: for S being Element of (G ./. (Ker g)) holds S1[S,f . S] from FUNCT_2:sch_3(A2);
now__::_thesis:_for_S,_T_being_Element_of_(G_./._(Ker_g))_holds_f_._(S_*_T)_=_(f_._S)_*_(f_._T)
let S, T be Element of (G ./. (Ker g)); ::_thesis: f . (S * T) = (f . S) * (f . T)
consider a being Element of G such that
A5: S = a * (Ker g) and
S = (Ker g) * a by Th13;
consider b being Element of G such that
A6: T = b * (Ker g) and
A7: T = (Ker g) * b by Th13;
A8: f . T = g . b by A4, A6;
f . S = g . a by A4, A5;
then A9: (f . S) * (f . T) = (g . a) * (g . b) by A8, GROUP_2:43
.= g . (a * b) by Def6 ;
S * T = (a * (Ker g)) * ((Ker g) * b) by A5, A7, Def3
.= ((a * (Ker g)) * (Ker g)) * b by GROUP_3:11
.= (a * (Ker g)) * b by Th5
.= a * ((Ker g) * b) by GROUP_2:106
.= a * (b * (Ker g)) by GROUP_3:117
.= (a * b) * (Ker g) by GROUP_2:105 ;
hence f . (S * T) = (f . S) * (f . T) by A4, A9; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of (G ./. (Ker g)),(Image g) by Def6;
A10: f is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume ( y1 in dom f & y2 in dom f ) ; ::_thesis: ( not f . y1 = f . y2 or y1 = y2 )
then reconsider S = y1, T = y2 as Element of (G ./. (Ker g)) ;
assume A11: f . y1 = f . y2 ; ::_thesis: y1 = y2
consider a being Element of G such that
A12: S = a * (Ker g) and
S = (Ker g) * a by Th13;
consider b being Element of G such that
A13: T = b * (Ker g) and
T = (Ker g) * b by Th13;
A14: f . T = g . b by A4, A13;
f . S = g . a by A4, A12;
then ((g . b) ") * (g . a) = 1_ H by A11, A14, GROUP_1:def_5;
then 1_ H = (g . (b ")) * (g . a) by Th32
.= g . ((b ") * a) by Def6 ;
then (b ") * a in Ker g by Th41;
hence y1 = y2 by A12, A13, GROUP_2:114; ::_thesis: verum
end;
A15: dom g = the carrier of G by FUNCT_2:def_1;
A16: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_g_implies_(_x_in_dom_(nat_hom_(Ker_g))_&_(nat_hom_(Ker_g))_._x_in_dom_f_)_)_&_(_x_in_dom_(nat_hom_(Ker_g))_&_(nat_hom_(Ker_g))_._x_in_dom_f_implies_x_in_dom_g_)_)
let x be set ; ::_thesis: ( ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) & ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g ) )
thus ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) ::_thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g )
proof
assume A17: x in dom g ; ::_thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f )
hence x in dom (nat_hom (Ker g)) by A1; ::_thesis: (nat_hom (Ker g)) . x in dom f
A18: dom f = the carrier of (G ./. (Ker g)) by FUNCT_2:def_1;
(nat_hom (Ker g)) . x in rng (nat_hom (Ker g)) by A1, A17, FUNCT_1:def_3;
hence (nat_hom (Ker g)) . x in dom f by A18; ::_thesis: verum
end;
assume that
A19: x in dom (nat_hom (Ker g)) and
(nat_hom (Ker g)) . x in dom f ; ::_thesis: x in dom g
thus x in dom g by A15, A19; ::_thesis: verum
end;
the carrier of (Image g) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Image g) or x in rng f )
assume x in the carrier of (Image g) ; ::_thesis: x in rng f
then x in Image g by STRUCT_0:def_5;
then consider a being Element of G such that
A20: x = g . a by Th45;
reconsider S = a * (Ker g) as Element of (G ./. (Ker g)) by Th14;
( f . S = g . a & the carrier of (G ./. (Ker g)) = dom f ) by A4, FUNCT_2:def_1;
hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum
end;
then A21: rng f = the carrier of (Image g) by XBOOLE_0:def_10;
then f is bijective by A10, Th60;
hence G ./. (Ker g), Image g are_isomorphic by Def11; ::_thesis: ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) )
take f ; ::_thesis: ( f is bijective & g = f * (nat_hom (Ker g)) )
thus f is bijective by A21, A10, Th60; ::_thesis: g = f * (nat_hom (Ker g))
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_f_._((nat_hom_(Ker_g))_._x)
let x be set ; ::_thesis: ( x in dom g implies g . x = f . ((nat_hom (Ker g)) . x) )
assume x in dom g ; ::_thesis: g . x = f . ((nat_hom (Ker g)) . x)
then reconsider a = x as Element of G ;
(nat_hom (Ker g)) . a = a * (Ker g) by Def8;
hence g . x = f . ((nat_hom (Ker g)) . x) by A4; ::_thesis: verum
end;
hence g = f * (nat_hom (Ker g)) by A16, FUNCT_1:10; ::_thesis: verum
end;
theorem :: GROUP_6:78
for H, G being Group
for g being Homomorphism of G,H holds G ./. (Ker g), Image g are_isomorphic by Lm3;
theorem :: GROUP_6:79
for H, G being Group
for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) by Lm3;
theorem :: GROUP_6:80
for G being Group
for N being normal Subgroup of G
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
proof
let G be Group; ::_thesis: for N being normal Subgroup of G
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let N be normal Subgroup of G; ::_thesis: for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let M be strict normal Subgroup of G; ::_thesis: for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic
let J be strict normal Subgroup of G ./. M; ::_thesis: ( J = N ./. ((N,M) `*`) & M is Subgroup of N implies (G ./. M) ./. J,G ./. N are_isomorphic )
assume that
A1: J = N ./. ((N,M) `*`) and
A2: M is Subgroup of N ; ::_thesis: (G ./. M) ./. J,G ./. N are_isomorphic
defpred S1[ set , set ] means for a being Element of G st $1 = a * M holds
$2 = a * N;
A3: for x being Element of (G ./. M) ex y being Element of (G ./. N) st S1[x,y]
proof
let x be Element of (G ./. M); ::_thesis: ex y being Element of (G ./. N) st S1[x,y]
consider a being Element of G such that
A4: x = a * M and
x = M * a by Th13;
reconsider y = a * N as Element of (G ./. N) by Th14;
take y ; ::_thesis: S1[x,y]
let b be Element of G; ::_thesis: ( x = b * M implies y = b * N )
assume x = b * M ; ::_thesis: y = b * N
then (a ") * b in M by A4, GROUP_2:114;
then (a ") * b in N by A2, GROUP_2:40;
hence y = b * N by GROUP_2:114; ::_thesis: verum
end;
consider f being Function of (G ./. M),(G ./. N) such that
A5: for x being Element of (G ./. M) holds S1[x,f . x] from FUNCT_2:sch_3(A3);
now__::_thesis:_for_x,_y_being_Element_of_(G_./._M)_holds_f_._(x_*_y)_=_(f_._x)_*_(f_._y)
let x, y be Element of (G ./. M); ::_thesis: f . (x * y) = (f . x) * (f . y)
consider a being Element of G such that
A6: x = a * M and
x = M * a by Th13;
consider b being Element of G such that
A7: y = b * M and
y = M * b by Th13;
A8: x * y = (@ x) * (@ y) by Def3
.= ((a * M) * b) * M by A6, A7, GROUP_3:9
.= (a * (M * b)) * M by GROUP_2:106
.= (a * (b * M)) * M by GROUP_3:117
.= a * ((b * M) * M) by GROUP_2:96
.= a * (b * M) by Th5
.= (a * b) * M by GROUP_2:105 ;
A9: f . y = b * N by A5, A7;
A10: f . x = a * N by A5, A6;
(f . x) * (f . y) = (@ (f . x)) * (@ (f . y)) by Def3
.= ((a * N) * b) * N by A10, A9, GROUP_3:9
.= (a * (N * b)) * N by GROUP_2:106
.= (a * (b * N)) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= (a * b) * N by GROUP_2:105 ;
hence f . (x * y) = (f . x) * (f . y) by A5, A8; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of (G ./. M),(G ./. N) by Def6;
A11: Ker f = J
proof
let S be Element of (G ./. M); :: according to GROUP_2:def_6 ::_thesis: ( ( not S in Ker f or S in J ) & ( not S in J or S in Ker f ) )
thus ( S in Ker f implies S in J ) ::_thesis: ( not S in J or S in Ker f )
proof
assume S in Ker f ; ::_thesis: S in J
then A12: f . S = 1_ (G ./. N) by Th41
.= carr N by Th24 ;
consider a being Element of G such that
A13: S = a * M and
A14: S = M * a by Th13;
f . S = a * N by A5, A13;
then a in N by A12, GROUP_2:113;
then reconsider q = a as Element of N by STRUCT_0:def_5;
(N,M) `*` = M by A2, Def1;
then ( S = q * ((N,M) `*`) & S = ((N,M) `*`) * q ) by A13, A14, Th2;
hence S in J by A1, Th23; ::_thesis: verum
end;
assume S in J ; ::_thesis: S in Ker f
then consider a being Element of N such that
A15: S = a * ((N,M) `*`) and
S = ((N,M) `*`) * a by A1, Th23;
reconsider a9 = a as Element of G by GROUP_2:42;
(N,M) `*` = M by A2, Def1;
then S = a9 * M by A15, Th2;
then A16: f . S = a9 * N by A5;
a in N by STRUCT_0:def_5;
then f . S = carr N by A16, GROUP_2:113
.= 1_ (G ./. N) by Th24 ;
hence S in Ker f by Th41; ::_thesis: verum
end;
the carrier of (G ./. N) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (G ./. N) or x in rng f )
assume x in the carrier of (G ./. N) ; ::_thesis: x in rng f
then x in G ./. N by STRUCT_0:def_5;
then consider a being Element of G such that
A17: x = a * N and
x = N * a by Th23;
reconsider S = a * M as Element of (G ./. M) by Th14;
( f . S = a * N & dom f = the carrier of (G ./. M) ) by A5, FUNCT_2:def_1;
hence x in rng f by A17, FUNCT_1:def_3; ::_thesis: verum
end;
then rng f = the carrier of (G ./. N) by XBOOLE_0:def_10;
then f is onto by FUNCT_2:def_3;
then Image f = G ./. N by Th57;
hence (G ./. M) ./. J,G ./. N are_isomorphic by A11, Lm3; ::_thesis: verum
end;
theorem :: GROUP_6:81
for G being Group
for B being Subgroup of G
for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
proof
let G be Group; ::_thesis: for B being Subgroup of G
for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
let B be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
let N be strict normal Subgroup of G; ::_thesis: (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic
set f = nat_hom N;
set g = (nat_hom N) | the carrier of B;
set I = (B "\/" N) ./. (((B "\/" N),N) `*`);
set J = ((B "\/" N),N) `*` ;
A1: the carrier of B c= the carrier of G by GROUP_2:def_5;
A2: ( dom ((nat_hom N) | the carrier of B) = (dom (nat_hom N)) /\ the carrier of B & dom (nat_hom N) = the carrier of G ) by FUNCT_2:def_1, RELAT_1:61;
then A3: dom ((nat_hom N) | the carrier of B) = the carrier of B by A1, XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:60;
then A5: N = ((B "\/" N),N) `*` by Def1;
A6: B is Subgroup of B "\/" N by GROUP_4:60;
rng ((nat_hom N) | the carrier of B) c= the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((nat_hom N) | the carrier of B) or y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) )
assume y in rng ((nat_hom N) | the carrier of B) ; ::_thesis: y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`))
then consider x being set such that
A7: x in dom ((nat_hom N) | the carrier of B) and
A8: ((nat_hom N) | the carrier of B) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of B by A2, A1, A7, XBOOLE_1:28;
reconsider x9 = x as Element of G by GROUP_2:42;
reconsider x99 = x as Element of (B "\/" N) by A6, GROUP_2:42;
A9: ( x99 * (((B "\/" N),N) `*`) = x9 * N & N * x9 = (((B "\/" N),N) `*`) * x99 ) by A5, Th2;
A10: ((nat_hom N) | the carrier of B) . x = (nat_hom N) . x9 by A7, FUNCT_1:47
.= x9 * N by Def8 ;
then ((nat_hom N) | the carrier of B) . x = N * x9 by GROUP_3:117;
then y in (B "\/" N) ./. (((B "\/" N),N) `*`) by A8, A10, A9, Th23;
hence y in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider g = (nat_hom N) | the carrier of B as Function of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by A3, FUNCT_2:def_1, RELSET_1:4;
A11: (B "\/" N) ./. (((B "\/" N),N) `*`) is Subgroup of G ./. N by A4, Th28;
now__::_thesis:_for_a,_b_being_Element_of_B_holds_g_._(a_*_b)_=_(g_._a)_*_(g_._b)
let a, b be Element of B; ::_thesis: g . (a * b) = (g . a) * (g . b)
reconsider a9 = a, b9 = b as Element of G by GROUP_2:42;
A12: ( (nat_hom N) . a9 = g . a & (nat_hom N) . b9 = g . b ) by FUNCT_1:49;
a * b = a9 * b9 by GROUP_2:43;
hence g . (a * b) = (nat_hom N) . (a9 * b9) by FUNCT_1:49
.= ((nat_hom N) . a9) * ((nat_hom N) . b9) by Def6
.= (g . a) * (g . b) by A11, A12, GROUP_2:43 ;
::_thesis: verum
end;
then reconsider g = g as Homomorphism of B,((B "\/" N) ./. (((B "\/" N),N) `*`)) by Def6;
A13: Ker g = B /\ N
proof
let b be Element of B; :: according to GROUP_2:def_6 ::_thesis: ( ( not b in Ker g or b in B /\ N ) & ( not b in B /\ N or b in Ker g ) )
reconsider c = b as Element of G by GROUP_2:42;
A14: g . b = (nat_hom N) . c by FUNCT_1:49
.= c * N by Def8 ;
thus ( b in Ker g implies b in B /\ N ) ::_thesis: ( not b in B /\ N or b in Ker g )
proof
assume b in Ker g ; ::_thesis: b in B /\ N
then g . b = 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th41
.= carr (((B "\/" N),N) `*`) by Th24
.= carr N by A4, Def1 ;
then ( b in B & b in N ) by A14, GROUP_2:113, STRUCT_0:def_5;
hence b in B /\ N by GROUP_2:82; ::_thesis: verum
end;
assume b in B /\ N ; ::_thesis: b in Ker g
then b in N by GROUP_2:82;
then c * N = carr (((B "\/" N),N) `*`) by A5, GROUP_2:113
.= 1_ ((B "\/" N) ./. (((B "\/" N),N) `*`)) by Th24 ;
hence b in Ker g by A14, Th41; ::_thesis: verum
end;
the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) c= rng g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) or x in rng g )
assume x in the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) ; ::_thesis: x in rng g
then x in (B "\/" N) ./. (((B "\/" N),N) `*`) by STRUCT_0:def_5;
then consider b being Element of (B "\/" N) such that
A15: x = b * (((B "\/" N),N) `*`) and
x = (((B "\/" N),N) `*`) * b by Th23;
( B * N = N * B & b in B "\/" N ) by GROUP_5:8, STRUCT_0:def_5;
then consider a1, a2 being Element of G such that
A16: b = a1 * a2 and
A17: a1 in B and
A18: a2 in N by GROUP_5:5;
A19: a1 in the carrier of B by A17, STRUCT_0:def_5;
x = (a1 * a2) * N by A5, A15, A16, Th2
.= a1 * (a2 * N) by GROUP_2:105
.= a1 * N by A18, GROUP_2:113
.= (nat_hom N) . a1 by Def8
.= g . a1 by A19, FUNCT_1:49 ;
hence x in rng g by A3, A19, FUNCT_1:def_3; ::_thesis: verum
end;
then the carrier of ((B "\/" N) ./. (((B "\/" N),N) `*`)) = rng g by XBOOLE_0:def_10;
then g is onto by FUNCT_2:def_3;
then Image g = (B "\/" N) ./. (((B "\/" N),N) `*`) by Th57;
hence (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic by A13, Lm3; ::_thesis: verum
end;