let AFP be AffinPlane; 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; ( 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
; ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
A4:
now ( f <> id the carrier of AFP implies ex g being Permutation of the carrier of AFP st
( 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
;
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 not p,c // p, the Element of AFPassume
p,
c // p, the
Element of
AFP
;
contradictionthen
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;
verum end; consider f3 being
Permutation of the
carrier of
AFP such that 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;
verum end;
hence
ex g being Permutation of the carrier of AFP st
( g is translation & g * g = f )
by A4; verum