let G, H be strict Group; :: thesis: for h being Homomorphism of G,H
for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let h be Homomorphism of G,H; :: thesis: for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let A be strict Subgroup of G; :: thesis: for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let a be Element of G; :: thesis: ( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
now :: thesis: for x being object st x in h .: (a * A) holds
x in (h . a) * (h .: A)
let x be object ; :: thesis: ( x in h .: (a * A) implies x in (h . a) * (h .: A) )
assume x in h .: (a * A) ; :: thesis: x in (h . a) * (h .: A)
then consider y being object such that
A1: y in the carrier of G and
A2: y in a * A and
A3: x = h . y by FUNCT_2:64;
reconsider y = y as Element of G by A1;
consider b being Element of G such that
A4: y = a * b and
A5: b in A by A2, GROUP_2:103;
b in the carrier of A by A5, STRUCT_0:def 5;
then h . b in h .: the carrier of A by FUNCT_2:35;
then h . b in the carrier of (h .: A) by Th8;
then A6: h . b in h .: A by STRUCT_0:def 5;
x = (h . a) * (h . b) by A3, A4, GROUP_6:def 6;
hence x in (h . a) * (h .: A) by A6, GROUP_2:103; :: thesis: verum
end;
then A7: h .: (a * A) c= (h . a) * (h .: A) ;
now :: thesis: for x being object st x in (h . a) * (h .: A) holds
x in h .: (a * A)
let x be object ; :: thesis: ( x in (h . a) * (h .: A) implies x in h .: (a * A) )
assume x in (h . a) * (h .: A) ; :: thesis: x in h .: (a * A)
then consider b1 being Element of H such that
A8: x = (h . a) * b1 and
A9: b1 in h .: A by GROUP_2:103;
consider b being Element of A such that
A10: b1 = (h | A) . b by A9, GROUP_6:45;
A11: b in A by STRUCT_0:def 5;
reconsider b = b as Element of G by GROUP_2:42;
b1 = h . b by A10, FUNCT_1:49;
then A12: x = h . (a * b) by A8, GROUP_6:def 6;
a * b in a * A by A11, GROUP_2:103;
hence x in h .: (a * A) by A12, FUNCT_2:35; :: thesis: verum
end;
then (h . a) * (h .: A) c= h .: (a * A) ;
hence (h . a) * (h .: A) = h .: (a * A) by A7, XBOOLE_0:def 10; :: thesis: (h .: A) * (h . a) = h .: (A * a)
now :: thesis: for x being object st x in h .: (A * a) holds
x in (h .: A) * (h . a)
let x be object ; :: thesis: ( x in h .: (A * a) implies x in (h .: A) * (h . a) )
assume x in h .: (A * a) ; :: thesis: x in (h .: A) * (h . a)
then consider y being object such that
A13: y in the carrier of G and
A14: y in A * a and
A15: x = h . y by FUNCT_2:64;
reconsider y = y as Element of G by A13;
consider b being Element of G such that
A16: y = b * a and
A17: b in A by A14, GROUP_2:104;
b in the carrier of A by A17, STRUCT_0:def 5;
then h . b in h .: the carrier of A by FUNCT_2:35;
then h . b in the carrier of (h .: A) by Th8;
then A18: h . b in h .: A by STRUCT_0:def 5;
x = (h . b) * (h . a) by A15, A16, GROUP_6:def 6;
hence x in (h .: A) * (h . a) by A18, GROUP_2:104; :: thesis: verum
end;
then A19: h .: (A * a) c= (h .: A) * (h . a) ;
now :: thesis: for x being object st x in (h .: A) * (h . a) holds
x in h .: (A * a)
let x be object ; :: thesis: ( x in (h .: A) * (h . a) implies x in h .: (A * a) )
assume x in (h .: A) * (h . a) ; :: thesis: x in h .: (A * a)
then consider b1 being Element of H such that
A20: x = b1 * (h . a) and
A21: b1 in h .: A by GROUP_2:104;
consider b being Element of A such that
A22: b1 = (h | A) . b by A21, GROUP_6:45;
A23: b in A by STRUCT_0:def 5;
reconsider b = b as Element of G by GROUP_2:42;
b1 = h . b by A22, FUNCT_1:49;
then A24: x = h . (b * a) by A20, GROUP_6:def 6;
b * a in A * a by A23, GROUP_2:104;
hence x in h .: (A * a) by A24, FUNCT_2:35; :: thesis: verum
end;
then (h .: A) * (h . a) c= h .: (A * a) ;
hence (h .: A) * (h . a) = h .: (A * a) by A19, XBOOLE_0:def 10; :: thesis: verum