let AFP be AffinPlane; :: thesis: for f being Permutation of the carrier of AFP st AFP is Fanoian & AFP is translational & f is translation holds

ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

let f be Permutation of the carrier of AFP; :: thesis: ( AFP is Fanoian & AFP is translational & f is translation implies ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) )

assume that

A1: AFP is Fanoian and

A2: AFP is translational and

A3: f is translation ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

( g is translation & g * g = f ) by A4; :: thesis: verum

ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

let f be Permutation of the carrier of AFP; :: thesis: ( AFP is Fanoian & AFP is translational & f is translation implies ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) )

assume that

A1: AFP is Fanoian and

A2: AFP is translational and

A3: f is translation ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

A4: now :: thesis: ( f <> id the carrier of AFP implies ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) )

( g is translation & g * g = f ) )

set a = the Element of AFP;

set b = f . the Element of AFP;

assume f <> id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

then the Element of AFP <> f . the Element of AFP by A3, TRANSGEO:def 11;

then consider c being Element of AFP such that

A5: not LIN the Element of AFP,f . the Element of AFP,c by AFF_1:13;

consider d being Element of AFP such that

A6: c,f . the Element of AFP // the Element of AFP,d and

A7: c, the Element of AFP // f . the Element of AFP,d by DIRAF:40;

not LIN c,f . the Element of AFP, the Element of AFP by A5, AFF_1:6;

then consider p being Element of AFP such that

A8: LIN f . the Element of AFP, the Element of AFP,p and

A9: LIN c,d,p by A1, A6, A7, Th2;

consider f1 being Permutation of the carrier of AFP such that

A10: f1 is translation and

A11: f1 . p = the Element of AFP by A2, Th7;

consider f2 being Permutation of the carrier of AFP such that

A12: f2 is translation and

A13: f2 . p = f . the Element of AFP by A2, Th7;

A14: f1 * f2 is translation by A10, A12, TRANSGEO:86;

A15: LIN p,c,d by A9, AFF_1:6;

then A16: p,c // p,d by AFF_1:def 1;

A19: f3 is translation and

A20: f3 . p = c by A2, Th7;

f3 " is translation by A19, TRANSGEO:85;

then A21: f1 * (f3 ") is translation by A10, TRANSGEO:86;

LIN p, the Element of AFP,f . the Element of AFP by A8, AFF_1:6;

then p,f1 . p // p,f2 . p by A11, A13, AFF_1:def 1;

then A22: p, the Element of AFP // p,(f1 * f2) . p by A10, A11, A12, Th11;

consider f4 being Permutation of the carrier of AFP such that

A23: f4 is translation and

A24: f4 . p = d by A2, Th7;

f4 . ((f2 ") . (f . the Element of AFP)) = f4 . p by A13, TRANSGEO:2;

then A25: (f4 * (f2 ")) . (f . the Element of AFP) = d by A24, FUNCT_2:15;

consider h being Permutation of the carrier of AFP such that

A26: h is translation and

A27: h . c = the Element of AFP by A2, Th7;

not LIN c, the Element of AFP,f . the Element of AFP by A5, AFF_1:6;

then A28: h . (f . the Element of AFP) = d by A6, A7, A26, A27, Th3;

f1 . ((f3 ") . c) = f1 . p by A20, TRANSGEO:2;

then (f1 * (f3 ")) . c = the Element of AFP by A11, FUNCT_2:15;

then A29: f1 * (f3 ") = h by A26, A27, A21, TRANSGEO:84;

A30: f2 " is translation by A12, TRANSGEO:85;

then f4 * (f2 ") is translation by A23, TRANSGEO:86;

then f1 * (f3 ") = f4 * (f2 ") by A26, A28, A29, A25, TRANSGEO:84;

then f1 * ((f3 ") * f3) = (f4 * (f2 ")) * f3 by RELAT_1:36;

then f1 * (id the carrier of AFP) = (f4 * (f2 ")) * f3 by FUNCT_2:61;

then f1 = (f4 * (f2 ")) * f3 by FUNCT_2:17

.= f4 * ((f2 ") * f3) by RELAT_1:36

.= f4 * (f3 * (f2 ")) by A2, A19, A30, Th10

.= (f4 * f3) * (f2 ") by RELAT_1:36 ;

then A31: f1 * f2 = (f4 * f3) * ((f2 ") * f2) by RELAT_1:36

.= (f4 * f3) * (id the carrier of AFP) by FUNCT_2:61

.= f4 * f3 by FUNCT_2:17 ;

p,f3 . p // p,f4 . p by A20, A24, A15, AFF_1:def 1;

then p,c // p,(f3 * f4) . p by A19, A20, A23, Th11;

then p,c // p,(f1 * f2) . p by A2, A19, A23, A31, Th10;

then p = (f1 * f2) . p by A22, A17, AFF_1:5;

then (f1 ") * (f1 * f2) = (f1 ") * (id the carrier of AFP) by A14, TRANSGEO:def 11;

then ((f1 ") * f1) * f2 = (f1 ") * (id the carrier of AFP) by RELAT_1:36;

then (id the carrier of AFP) * f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:61;

then f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:17;

then A32: (f2 * f2) . the Element of AFP = (f2 * (f1 ")) . the Element of AFP by FUNCT_2:17

.= f2 . ((f1 ") . the Element of AFP) by FUNCT_2:15

.= f . the Element of AFP by A11, A13, TRANSGEO:2 ;

f2 * f2 is translation by A12, TRANSGEO:86;

hence ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) by A3, A12, A32, TRANSGEO:84; :: thesis: verum

end;set b = f . the Element of AFP;

assume f <> id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

then the Element of AFP <> f . the Element of AFP by A3, TRANSGEO:def 11;

then consider c being Element of AFP such that

A5: not LIN the Element of AFP,f . the Element of AFP,c by AFF_1:13;

consider d being Element of AFP such that

A6: c,f . the Element of AFP // the Element of AFP,d and

A7: c, the Element of AFP // f . the Element of AFP,d by DIRAF:40;

not LIN c,f . the Element of AFP, the Element of AFP by A5, AFF_1:6;

then consider p being Element of AFP such that

A8: LIN f . the Element of AFP, the Element of AFP,p and

A9: LIN c,d,p by A1, A6, A7, Th2;

consider f1 being Permutation of the carrier of AFP such that

A10: f1 is translation and

A11: f1 . p = the Element of AFP by A2, Th7;

consider f2 being Permutation of the carrier of AFP such that

A12: f2 is translation and

A13: f2 . p = f . the Element of AFP by A2, Th7;

A14: f1 * f2 is translation by A10, A12, TRANSGEO:86;

A15: LIN p,c,d by A9, AFF_1:6;

then A16: p,c // p,d by AFF_1:def 1;

A17: now :: thesis: not p,c // p, the Element of AFP

consider f3 being Permutation of the carrier of AFP such that assume
p,c // p, the Element of AFP
; :: thesis: contradiction

then LIN p,c, the Element of AFP by AFF_1:def 1;

then A18: LIN p, the Element of AFP,c by AFF_1:6;

( LIN p, the Element of AFP, the Element of AFP & LIN p, the Element of AFP,f . the Element of AFP ) by A8, AFF_1:6, AFF_1:7;

then p = the Element of AFP by A5, A18, AFF_1:8;

then ( the Element of AFP,c // c,f . the Element of AFP or the Element of AFP = d ) by A6, A16, AFF_1:5;

then ( c, the Element of AFP // c,f . the Element of AFP or the Element of AFP = d ) by AFF_1:4;

then ( LIN c, the Element of AFP,f . the Element of AFP or the Element of AFP = d ) by AFF_1:def 1;

then the Element of AFP,c // the Element of AFP,f . the Element of AFP by A5, A7, AFF_1:4, AFF_1:6;

then LIN the Element of AFP,c,f . the Element of AFP by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

end;then LIN p,c, the Element of AFP by AFF_1:def 1;

then A18: LIN p, the Element of AFP,c by AFF_1:6;

( LIN p, the Element of AFP, the Element of AFP & LIN p, the Element of AFP,f . the Element of AFP ) by A8, AFF_1:6, AFF_1:7;

then p = the Element of AFP by A5, A18, AFF_1:8;

then ( the Element of AFP,c // c,f . the Element of AFP or the Element of AFP = d ) by A6, A16, AFF_1:5;

then ( c, the Element of AFP // c,f . the Element of AFP or the Element of AFP = d ) by AFF_1:4;

then ( LIN c, the Element of AFP,f . the Element of AFP or the Element of AFP = d ) by AFF_1:def 1;

then the Element of AFP,c // the Element of AFP,f . the Element of AFP by A5, A7, AFF_1:4, AFF_1:6;

then LIN the Element of AFP,c,f . the Element of AFP by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

A19: f3 is translation and

A20: f3 . p = c by A2, Th7;

f3 " is translation by A19, TRANSGEO:85;

then A21: f1 * (f3 ") is translation by A10, TRANSGEO:86;

LIN p, the Element of AFP,f . the Element of AFP by A8, AFF_1:6;

then p,f1 . p // p,f2 . p by A11, A13, AFF_1:def 1;

then A22: p, the Element of AFP // p,(f1 * f2) . p by A10, A11, A12, Th11;

consider f4 being Permutation of the carrier of AFP such that

A23: f4 is translation and

A24: f4 . p = d by A2, Th7;

f4 . ((f2 ") . (f . the Element of AFP)) = f4 . p by A13, TRANSGEO:2;

then A25: (f4 * (f2 ")) . (f . the Element of AFP) = d by A24, FUNCT_2:15;

consider h being Permutation of the carrier of AFP such that

A26: h is translation and

A27: h . c = the Element of AFP by A2, Th7;

not LIN c, the Element of AFP,f . the Element of AFP by A5, AFF_1:6;

then A28: h . (f . the Element of AFP) = d by A6, A7, A26, A27, Th3;

f1 . ((f3 ") . c) = f1 . p by A20, TRANSGEO:2;

then (f1 * (f3 ")) . c = the Element of AFP by A11, FUNCT_2:15;

then A29: f1 * (f3 ") = h by A26, A27, A21, TRANSGEO:84;

A30: f2 " is translation by A12, TRANSGEO:85;

then f4 * (f2 ") is translation by A23, TRANSGEO:86;

then f1 * (f3 ") = f4 * (f2 ") by A26, A28, A29, A25, TRANSGEO:84;

then f1 * ((f3 ") * f3) = (f4 * (f2 ")) * f3 by RELAT_1:36;

then f1 * (id the carrier of AFP) = (f4 * (f2 ")) * f3 by FUNCT_2:61;

then f1 = (f4 * (f2 ")) * f3 by FUNCT_2:17

.= f4 * ((f2 ") * f3) by RELAT_1:36

.= f4 * (f3 * (f2 ")) by A2, A19, A30, Th10

.= (f4 * f3) * (f2 ") by RELAT_1:36 ;

then A31: f1 * f2 = (f4 * f3) * ((f2 ") * f2) by RELAT_1:36

.= (f4 * f3) * (id the carrier of AFP) by FUNCT_2:61

.= f4 * f3 by FUNCT_2:17 ;

p,f3 . p // p,f4 . p by A20, A24, A15, AFF_1:def 1;

then p,c // p,(f3 * f4) . p by A19, A20, A23, Th11;

then p,c // p,(f1 * f2) . p by A2, A19, A23, A31, Th10;

then p = (f1 * f2) . p by A22, A17, AFF_1:5;

then (f1 ") * (f1 * f2) = (f1 ") * (id the carrier of AFP) by A14, TRANSGEO:def 11;

then ((f1 ") * f1) * f2 = (f1 ") * (id the carrier of AFP) by RELAT_1:36;

then (id the carrier of AFP) * f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:61;

then f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:17;

then A32: (f2 * f2) . the Element of AFP = (f2 * (f1 ")) . the Element of AFP by FUNCT_2:17

.= f2 . ((f1 ") . the Element of AFP) by FUNCT_2:15

.= f . the Element of AFP by A11, A13, TRANSGEO:2 ;

f2 * f2 is translation by A12, TRANSGEO:86;

hence ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) by A3, A12, A32, TRANSGEO:84; :: thesis: verum

now :: thesis: ( f = id the carrier of AFP implies ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) )

hence
ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) )

set g = id the carrier of AFP;

A33: ( id the carrier of AFP is translation & (id the carrier of AFP) * (id the carrier of AFP) = id the carrier of AFP ) by FUNCT_2:17, TRANSGEO:81;

assume f = id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

hence ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) by A33; :: thesis: verum

end;A33: ( id the carrier of AFP is translation & (id the carrier of AFP) * (id the carrier of AFP) = id the carrier of AFP ) by FUNCT_2:17, TRANSGEO:81;

assume f = id the carrier of AFP ; :: thesis: ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f )

hence ex g being Permutation of the carrier of AFP st

( g is translation & g * g = f ) by A33; :: thesis: verum

( g is translation & g * g = f ) by A4; :: thesis: verum