let AFP be AffinPlane; :: thesis: for p being Element of AFP
for f, g being Permutation of the carrier of AFP st f is translation & g is translation & p,f . p // p,g . p holds
p,f . p // p,(f * g) . p
let p be Element of AFP; :: thesis: for f, g being Permutation of the carrier of AFP st f is translation & g is translation & p,f . p // p,g . p holds
p,f . p // p,(f * g) . p
let f, g be Permutation of the carrier of AFP; :: thesis: ( f is translation & g is translation & p,f . p // p,g . p implies p,f . p // p,(f * g) . p )
assume that
A1: f is translation and
A2: g is translation and
A3: p,f . p // p,g . p ; :: thesis: p,f . p // p,(f * g) . p
A4: f is dilatation by A1, TRANSGEO:def 11;
A5: now :: thesis: ( g <> id the carrier of AFP implies p,f . p // p,(f * g) . p )
assume g <> id the carrier of AFP ; :: thesis: p,f . p // p,(f * g) . p
then A6: g . p <> p by A2, TRANSGEO:def 11;
p,g . p // f . p,f . (g . p) by A4, TRANSGEO:68;
then p,f . p // f . p,f . (g . p) by A3, A6, AFF_1:5;
then f . p,p // f . p,f . (g . p) by AFF_1:4;
then LIN f . p,p,f . (g . p) by AFF_1:def 1;
then LIN p,f . p,f . (g . p) by AFF_1:6;
then p,f . p // p,f . (g . p) by AFF_1:def 1;
hence p,f . p // p,(f * g) . p by FUNCT_2:15; :: thesis: verum
end;
now :: thesis: ( g = id the carrier of AFP implies p,f . p // p,(f * g) . p )
assume g = id the carrier of AFP ; :: thesis: p,f . p // p,(f * g) . p
then f * g = f by FUNCT_2:17;
hence p,f . p // p,(f * g) . p by AFF_1:2; :: thesis: verum
end;
hence p,f . p // p,(f * g) . p by A5; :: thesis: verum