let O be set ; :: thesis: for G, H being GroupWithOperators of O
for G9 being StableSubgroup of G
for H9 being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9
let G, H be GroupWithOperators of O; :: thesis: for G9 being StableSubgroup of G
for H9 being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9
let G9 be StableSubgroup of G; :: thesis: for H9 being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9
let H9 be StableSubgroup of H; :: thesis: for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9
let f be Homomorphism of G,H; :: thesis: ( ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) implies f | the carrier of G9 is Homomorphism of G9,H9 )
set g = f | the carrier of G9;
G9 is Subgroup of G by Def7;
then A1: the carrier of G9 c= the carrier of G by GROUP_2:def 5;
then A2: the carrier of G9 c= dom f by FUNCT_2:def 1;
then A3: dom (f | the carrier of G9) = the carrier of G9 by RELAT_1:62;
assume A4: ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) ; :: thesis: f | the carrier of G9 is Homomorphism of G9,H9
A5: for x being set st x in the carrier of G9 holds
f . x in the carrier of H9
proof
let x be set ; :: thesis: ( x in the carrier of G9 implies f . x in the carrier of H9 )
assume A6: x in the carrier of G9 ; :: thesis: f . x in the carrier of H9
per cases ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) by A4;
suppose A7: the carrier of H9 = f .: the carrier of G9 ; :: thesis: f . x in the carrier of H9
assume not f . x in the carrier of H9 ; :: thesis: contradiction
hence contradiction by A2, A6, A7, FUNCT_1:def 6; :: thesis: verum
end;
suppose the carrier of G9 = f " the carrier of H9 ; :: thesis: f . x in the carrier of H9
hence f . x in the carrier of H9 by A6, FUNCT_1:def 7; :: thesis: verum
end;
end;
end;
now :: thesis: for y being object st y in rng (f | the carrier of G9) holds
y in the carrier of H9
let y be object ; :: thesis: ( y in rng (f | the carrier of G9) implies y in the carrier of H9 )
assume y in rng (f | the carrier of G9) ; :: thesis: y in the carrier of H9
then consider x being object such that
A8: x in dom (f | the carrier of G9) and
A9: y = (f | the carrier of G9) . x by FUNCT_1:def 3;
A10: x in the carrier of G9 by A2, A8, RELAT_1:62;
then y = f . x by A9, FUNCT_1:49;
hence y in the carrier of H9 by A5, A10; :: thesis: verum
end;
then rng (f | the carrier of G9) c= the carrier of H9 ;
then reconsider g = f | the carrier of G9 as Function of G9,H9 by A3, RELSET_1:4;
A11: now :: thesis: for a9, b9 being Element of G9 holds g . (a9 * b9) = (g . a9) * (g . b9)
let a9, b9 be Element of G9; :: thesis: g . (a9 * b9) = (g . a9) * (g . b9)
reconsider a = a9, b = b9 as Element of G by A1;
A12: ( f . a = g . a9 & f . b = g . b9 ) by FUNCT_1:49;
thus g . (a9 * b9) = f . (a9 * b9) by FUNCT_1:49
.= f . (a * b) by Th3
.= (f . a) * (f . b) by GROUP_6:def 6
.= (g . a9) * (g . b9) by A12, Th3 ; :: thesis: verum
end;
now :: thesis: for o being Element of O
for a9 being Element of G9 holds g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)
let o be Element of O; :: thesis: for a9 being Element of G9 holds g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)
let a9 be Element of G9; :: thesis: g . ((G9 ^ o) . a9) = (H9 ^ o) . (g . a9)
reconsider a = a9 as Element of G by A1;
thus g . ((G9 ^ o) . a9) = f . ((G9 ^ o) . a9) by FUNCT_1:49
.= f . (((G ^ o) | the carrier of G9) . a9) by Def7
.= f . ((G ^ o) . a) by FUNCT_1:49
.= (H ^ o) . (f . a) by Def18
.= (H ^ o) . (g . a9) by FUNCT_1:49
.= ((H ^ o) | the carrier of H9) . (g . a9) by FUNCT_1:49
.= (H9 ^ o) . (g . a9) by Def7 ; :: thesis: verum
end;
hence f | the carrier of G9 is Homomorphism of G9,H9 by A11, Def18, GROUP_6:def 6; :: thesis: verum