let AFP be AffinPlane; :: thesis: for f being Permutation of the carrier of AFP st AFP is Fanoian & f is translation & f * f = id the carrier of AFP holds
f = id the carrier of AFP
let f be Permutation of the carrier of AFP; :: thesis: ( AFP is Fanoian & f is translation & f * f = id the carrier of AFP implies f = id the carrier of AFP )
consider a being Element of AFP;
assume that
A1: AFP is Fanoian and
A2: f is translation and
A3: f * f = id the carrier of AFP ; :: thesis: f = id the carrier of AFP
assume f <> id the carrier of AFP ; :: thesis: contradiction
then a <> f . a by A2, TRANSGEO:def 11;
then consider b being Element of AFP such that
A4: not LIN a,f . a,b by AFF_1:22;
A5: f is dilatation by A2, TRANSGEO:def 11;
then A6: a,b // f . a,f . b by TRANSGEO:85;
f . b,a // f . (f . b),f . a by A5, TRANSGEO:85;
then f . b,a // (f * f) . b,f . a by FUNCT_2:21;
then f . b,a // b,f . a by A3, FUNCT_1:35;
then A7: a,f . b // f . a,b by AFF_1:13;
a,f . a // b,f . b by A2, A5, TRANSGEO:100;
hence contradiction by A1, A4, A6, A7, Def1; :: thesis: verum