let G, F be finite commutative Group; :: thesis: for a being Element of G
for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})
let a be Element of G; :: thesis: for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})
let f be Homomorphism of G,F; :: thesis: the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})
for y being object holds
( y in the carrier of (gr {(f . a)}) iff y in f .: the carrier of (gr {a}) )
proof
let y be object ; :: thesis: ( y in the carrier of (gr {(f . a)}) iff y in f .: the carrier of (gr {a}) )
hereby :: thesis: ( y in f .: the carrier of (gr {a}) implies y in the carrier of (gr {(f . a)}) )
assume AA1: y in the carrier of (gr {(f . a)}) ; :: thesis: y in f .: the carrier of (gr {a})
then reconsider y0 = y as Element of F by TARSKI:def 3, GROUP_2:def 5;
y0 in gr {(f . a)} by AA1;
then consider i being Element of NAT such that
AA2: y0 = (f . a) |^ i by GRCY26;
AA3: y0 = f . (a |^ i) by AA2, GROUP_6:37;
a |^ i in gr {a} by GRCY26;
hence y in f .: the carrier of (gr {a}) by AA3, FUNCT_2:35; :: thesis: verum
end;
assume y in f .: the carrier of (gr {a}) ; :: thesis: y in the carrier of (gr {(f . a)})
then consider x being object such that
AA2: ( x in dom f & x in the carrier of (gr {a}) & y = f . x ) by FUNCT_1:def 6;
reconsider x0 = x as Element of G by AA2;
x0 in gr {a} by AA2;
then consider i being Element of NAT such that
AA3: x0 = a |^ i by GRCY26;
f . x0 = (f . a) |^ i by AA3, GROUP_6:37;
then f . x0 in gr {(f . a)} by GRCY26;
hence y in the carrier of (gr {(f . a)}) by AA2; :: thesis: verum
end;
hence the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a}) by TARSKI:2; :: thesis: verum