let O be set ; :: thesis: 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; :: thesis: for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic
let h be Homomorphism of G,H; :: thesis: 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 & h' = g' * (nat_hom (Ker h')) )
by GROUP_6:91;
A2:
Ker h is Subgroup of G
by Def7;
then
the carrier of (Ker h') = the carrier of (Ker h)
by TARSKI:2;
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 A2, GROUP_2:68;
then A6:
the carrier of (G' ./. (Ker h')) = the carrier of (G ./. (Ker h))
by Def14;
A7:
Image h is Subgroup of H
by Def7;
A8: the carrier of (Image h') =
h' .: the carrier of G'
by GROUP_6:def 11
.=
the carrier of (Image h)
by Def25
;
then A9:
multMagma(# the carrier of (Image h'),the multF of (Image h') #) = multMagma(# the carrier of (Image h),the multF of (Image h) #)
by A7, GROUP_2:68;
reconsider g = g' as Function of (G ./. (Ker h)),(Image h) by A6, A8;
A10:
now let o be
Element of
O;
:: thesis: 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));
:: thesis: g . (((G ./. (Ker h)) ^ b1) . b2) = ((Image h) ^ b1) . (g . b2)per cases
( O is empty or not O is empty )
;
suppose A12:
not
O is
empty
;
:: thesis: 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;
A13:
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 A12, Def16;
the
action of
(G ./. (Ker h)) . o = (G ./. (Ker h)) ^ o
by A12, 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 A14:
(
[A,B] = [a,(f . a)] & ex
g1,
g2 being
Element of
G st
(
g1 in A &
g2 in B &
g2 = (G ^ o) . g1 ) )
by A13;
reconsider A =
A,
B =
B as
Element of
Cosets (Ker h') by A5, Def14;
consider g1,
g2 being
Element of
G' such that A15:
(
g1 in A &
g2 in B &
g2 = (G ^ o) . g1 )
by A14;
A16:
(
A = g1 * (Ker h') &
B = g2 * (Ker h') )
by A15, Lm9;
A17:
g . (((G ./. (Ker h)) ^ o) . a) =
g . (f . a)
by A12, Def6
.=
g' . (g2 * (Ker h'))
by A14, A16, ZFMISC_1:33
;
A18:
((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 A14, A16, ZFMISC_1:33
;
g2 in the
carrier of
G'
;
then A19:
g2 in dom (nat_hom (Ker h'))
by FUNCT_2:def 1;
g1 in the
carrier of
G'
;
then A20:
g1 in dom (nat_hom (Ker h'))
by FUNCT_2:def 1;
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 A1, A19, FUNCT_1:23;
then
g' . ((nat_hom (Ker h')) . g2) = (H ^ o) . (g' . ((nat_hom (Ker h')) . g1))
by A20, FUNCT_1:23;
then
g' . (g2 * (Ker h')) = (H ^ o) . (g' . ((nat_hom (Ker h')) . g1))
by GROUP_6:def 9;
hence
g . (((G ./. (Ker h)) ^ o) . a) = ((Image h) ^ o) . (g . a)
by A17, A18, GROUP_6:def 9;
:: thesis: verum end; end;
then reconsider g = g as Homomorphism of (G ./. (Ker h)),(Image h) by A10, Def18, GROUP_6:def 7;
A21:
( g' is onto & g' is one-to-one )
by A1;
then A22:
rng g = the carrier of (Image h)
by A8, FUNCT_2:def 3;
g is one-to-one
by A21;
then
( g is onto & g is one-to-one )
by A22, FUNCT_2:def 3;
then
g is bijective
;
hence
G ./. (Ker h), Image h are_isomorphic
by Def22; :: thesis: verum