let O be set ; for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic
let G, H be GroupWithOperators of O; for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic
let h be Homomorphism of G,H; G ./. (Ker h), Image h are_isomorphic
reconsider G9 = G, H9 = H as Group ;
reconsider h9 = h as Homomorphism of G9,H9 ;
consider g9 being Homomorphism of (G9 ./. (Ker h9)),(Image h9) such that
A1:
g9 is bijective
and
A2:
h9 = g9 * (nat_hom (Ker h9))
by GROUP_6:79;
A3: the carrier of (Image h9) =
h9 .: the carrier of G9
by GROUP_6:def 10
.=
the carrier of (Image h)
by Def22
;
then A4:
the carrier of (Ker h9) = the carrier of (Ker h)
by TARSKI:2;
Ker h is Subgroup of G
by Def7;
then A5:
multMagma(# the carrier of (Ker h9), the multF of (Ker h9) #) = multMagma(# the carrier of (Ker h), the multF of (Ker h) #)
by A4, GROUP_2:59;
then
the carrier of (G9 ./. (Ker h9)) = the carrier of (G ./. (Ker h))
by Def14;
then reconsider g = g9 as Function of (G ./. (Ker h)),(Image h) by A3;
Image h is Subgroup of H
by Def7;
then A6:
multMagma(# the carrier of (Image h9), the multF of (Image h9) #) = multMagma(# the carrier of (Image h), the multF of (Image h) #)
by A3, GROUP_2:59;
now for o being Element of O
for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)let o be
Element of
O;
for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ b2) . b3) = ((Image h) ^ b2) . (g . b3)let a be
Element of
(G ./. (Ker h));
g . (((G ./. (Ker h)) ^ b1) . b2) = ((Image h) ^ b1) . (g . b2)per cases
( O is empty or not O is empty )
;
suppose A9:
not
O is
empty
;
g . (((G ./. (Ker h)) ^ b1) . b2) = ((Image h) ^ b1) . (g . b2)reconsider G99 =
G ./. (Ker h) as
Group ;
set f = the
action of
(G ./. (Ker h)) . o;
A10:
the
action of
(G ./. (Ker h)) . o = { [A,B] where A, B is Element of Cosets (Ker h) : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) }
by A9, Def16;
the
action of
(G ./. (Ker h)) . o = (G ./. (Ker h)) ^ o
by A9, Def6;
then reconsider f = the
action of
(G ./. (Ker h)) . o as
Homomorphism of
G99,
G99 ;
a in the
carrier of
G99
;
then
a in dom f
by FUNCT_2:def 1;
then
[a,(f . a)] in f
by FUNCT_1:1;
then consider A,
B being
Element of
Cosets (Ker h) such that A11:
[A,B] = [a,(f . a)]
and A12:
ex
g1,
g2 being
Element of
G st
(
g1 in A &
g2 in B &
g2 = (G ^ o) . g1 )
by A10;
reconsider A =
A,
B =
B as
Element of
Cosets (Ker h9) by A5, Def14;
consider g1,
g2 being
Element of
G9 such that A13:
g1 in A
and A14:
g2 in B
and A15:
g2 = (G ^ o) . g1
by A12;
A16:
A = g1 * (Ker h9)
by A13, Lm8;
g1 in the
carrier of
G9
;
then A17:
g1 in dom (nat_hom (Ker h9))
by FUNCT_2:def 1;
g2 in the
carrier of
G9
;
then A18:
g2 in dom (nat_hom (Ker h9))
by FUNCT_2:def 1;
A19:
((Image h) ^ o) . (g . a) =
((H ^ o) | the carrier of (Image h)) . (g . a)
by Def7
.=
(H ^ o) . (g . a)
by FUNCT_1:49
.=
(H ^ o) . (g9 . (g1 * (Ker h9)))
by A11, A16, XTUPLE_0:1
;
A20:
B = g2 * (Ker h9)
by A14, Lm8;
h9 . g2 = (H ^ o) . (h9 . g1)
by A15, Def18;
then
g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . ((g9 * (nat_hom (Ker h9))) . g1)
by A2, A18, FUNCT_1:13;
then
g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1))
by A17, FUNCT_1:13;
then A21:
g9 . (g2 * (Ker h9)) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1))
by GROUP_6:def 8;
g . (((G ./. (Ker h)) ^ o) . a) =
g . (f . a)
by A9, Def6
.=
g9 . (g2 * (Ker h9))
by A11, A20, XTUPLE_0:1
;
hence
g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)
by A19, A21, GROUP_6:def 8;
verum end; end;
then reconsider g = g as Homomorphism of (G ./. (Ker h)),(Image h) by A7, Def18, GROUP_6:def 6;
g is onto
by A1, A3;
hence
G ./. (Ker h), Image h are_isomorphic
by A1; verum