let O be set ; for H, G being GroupWithOperators of O
for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic
let H, G 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 G' = G, H' = H as Group ;
reconsider h' = h as Homomorphism of G',H' ;
consider g' being Homomorphism of G' ./. (Ker h'), Image h' such that
A1:
g' is bijective
and
A2:
h' = g' * (nat_hom (Ker h'))
by GROUP_6:91;
A3: the carrier of (Image h') =
h' .: the carrier of G'
by GROUP_6:def 11
.=
the carrier of (Image h)
by Def25
;
then A4:
the carrier of (Ker h') = the carrier of (Ker h)
by TARSKI:2;
Ker h is Subgroup of G
by Def7;
then A5:
multMagma(# the carrier of (Ker h'),the multF of (Ker h') #) = multMagma(# the carrier of (Ker h),the multF of (Ker h) #)
by A4, GROUP_2:68;
then
the carrier of (G' ./. (Ker h')) = the carrier of (G ./. (Ker h))
by Def14;
then reconsider g = g' 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 h'),the multF of (Image h') #) = multMagma(# the carrier of (Image h),the multF of (Image h) #)
by A3, GROUP_2:68;
now let o be
Element of
O;
for a being Element of holds g . (((G ./. (Ker h)) ^ b2) . b3) = ((Image h) ^ b2) . (g . b3)let a be
Element of ;
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 G'' =
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 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
G'',
G'' ;
a in the
carrier of
G''
;
then
a in dom f
by FUNCT_2:def 1;
then
[a,(f . a)] in f
by FUNCT_1:8;
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 st
(
g1 in A &
g2 in B &
g2 = (G ^ o) . g1 )
by A10;
reconsider A =
A,
B =
B as
Element of
Cosets (Ker h') by A5, Def14;
consider g1,
g2 being
Element of
such that A13:
g1 in A
and A14:
g2 in B
and A15:
g2 = (G ^ o) . g1
by A12;
A16:
A = g1 * (Ker h')
by A13, Lm9;
g1 in the
carrier of
G'
;
then A17:
g1 in dom (nat_hom (Ker h'))
by FUNCT_2:def 1;
g2 in the
carrier of
G'
;
then A18:
g2 in dom (nat_hom (Ker h'))
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:72
.=
(H ^ o) . (g' . (g1 * (Ker h')))
by A11, A16, ZFMISC_1:33
;
A20:
B = g2 * (Ker h')
by A14, Lm9;
h' . g2 = (H ^ o) . (h' . g1)
by A15, Def18;
then
g' . ((nat_hom (Ker h')) . g2) = (H ^ o) . ((g' * (nat_hom (Ker h'))) . g1)
by A2, A18, FUNCT_1:23;
then
g' . ((nat_hom (Ker h')) . g2) = (H ^ o) . (g' . ((nat_hom (Ker h')) . g1))
by A17, FUNCT_1:23;
then A21:
g' . (g2 * (Ker h')) = (H ^ o) . (g' . ((nat_hom (Ker h')) . g1))
by GROUP_6:def 9;
g . (((G ./. (Ker h)) ^ o) . a) =
g . (f . a)
by A9, Def6
.=
g' . (g2 * (Ker h'))
by A11, A20, ZFMISC_1:33
;
hence
g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)
by A19, A21, GROUP_6:def 9;
verum end; end;
then reconsider g = g as Homomorphism of (G ./. (Ker h)),(Image h) by A7, Def18, GROUP_6:def 7;
g is onto
by A1, A3;
hence
G ./. (Ker h), Image h are_isomorphic
by A1, Def22; verum