let O be set ; :: thesis: 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; :: 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 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 () by Def22 ;
now :: thesis: for x being object holds
( ( x in the carrier of (Ker h) implies x in the carrier of (Ker h9) ) & ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) ) )
let x be object ; :: thesis: ( ( x in the carrier of (Ker h) implies x in the carrier of (Ker h9) ) & ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) ) )
hereby :: thesis: ( x in the carrier of (Ker h9) implies x in the carrier of (Ker h) )
assume x in the carrier of (Ker h) ; :: thesis: x in the carrier of (Ker h9)
then x in { a where a is Element of G : h . a = 1_ H } by Def21;
hence x in the carrier of (Ker h9) by GROUP_6:def 9; :: thesis: verum
end;
assume x in the carrier of (Ker h9) ; :: thesis: x in the carrier of (Ker h)
then x in { a9 where a9 is Element of G9 : h9 . a9 = 1_ H9 } by GROUP_6:def 9;
hence x in the carrier of (Ker h) by Def21; :: thesis: verum
end;
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 ;
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)),() 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 (), the multF of () #) by ;
A7: now :: thesis: for a, b being Element of (G ./. (Ker h)) holds g . (a * b) = (g . a) * (g . b)
let a, b be Element of (G ./. (Ker h)); :: thesis: g . (a * b) = (g . a) * (g . b)
reconsider b9 = b as Element of (G9 ./. (Ker h9)) by ;
reconsider a9 = a as Element of (G9 ./. (Ker h9)) by ;
thus g . (a * b) = g9 . (a9 * b9) by
.= (g9 . a9) * (g9 . b9) by GROUP_6:def 6
.= (g . a) * (g . b) by A6 ; :: thesis: verum
end;
now :: thesis: for o being Element of O
for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ o) . a) = (() ^ o) . (g . a)
let o be Element of O; :: thesis: for a being Element of (G ./. (Ker h)) holds g . (((G ./. (Ker h)) ^ b2) . b3) = (() ^ b2) . (g . b3)
let a be Element of (G ./. (Ker h)); :: thesis: g . (((G ./. (Ker h)) ^ b1) . b2) = (() ^ b1) . (g . b2)
per cases ( O is empty or not O is empty ) ;
suppose A8: O is empty ; :: thesis: g . (((G ./. (Ker h)) ^ b1) . b2) = (() ^ b1) . (g . b2)
hence g . (((G ./. (Ker h)) ^ o) . a) = g . ((id the carrier of (G ./. (Ker h))) . a) by Def6
.= (id the carrier of ()) . (g . a)
.= (() ^ o) . (g . a) by ;
:: thesis: verum
end;
suppose A9: not O is empty ; :: thesis: g . (((G ./. (Ker h)) ^ b1) . b2) = (() ^ 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 ;
the action of (G ./. (Ker h)) . o = (G ./. (Ker h)) ^ o by ;
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 ;
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 ;
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: (() ^ o) . (g . a) = ((H ^ o) | the carrier of ()) . (g . a) by Def7
.= (H ^ o) . (g . a) by FUNCT_1:49
.= (H ^ o) . (g9 . (g1 * (Ker h9))) by ;
A20: B = g2 * (Ker h9) by ;
h9 . g2 = (H ^ o) . (h9 . g1) by ;
then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . ((g9 * (nat_hom (Ker h9))) . g1) by ;
then g9 . ((nat_hom (Ker h9)) . g2) = (H ^ o) . (g9 . ((nat_hom (Ker h9)) . g1)) by ;
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
.= g9 . (g2 * (Ker h9)) by ;
hence g . (((G ./. (Ker h)) ^ o) . a) = (() ^ o) . (g . a) by ; :: thesis: verum
end;
end;
end;
then reconsider g = g as Homomorphism of (G ./. (Ker h)),() by ;
g is onto by A1, A3;
hence G ./. (Ker h), Image h are_isomorphic by A1; :: thesis: verum