:: Translations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received June 12, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let AS be AffinSpace;

attr AS is Fanoian means :: TRANSLAC:def 1
for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c;

end;

:: deftheorem defines Fanoian TRANSLAC:def 1 :
for AS being AffinSpace holds
( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c );

Lm1: for AS being AffinSpace
for a, b, c, p being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p holds
ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )

proof end;

Lm2: for AS being AffinSpace
for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q holds
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )

proof end;

Lm3: for AS being AffinSpace
for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & p,q // a,b holds
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )

proof end;

theorem Th1: :: TRANSLAC:1

for AS being AffinSpace st ex a, b, c being Element of AS st
( LIN a,b,c & a <> b & a <> c & b <> c ) holds
for p, q being Element of AS ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )

proof end;

theorem Th2: :: TRANSLAC:2

for AFP being AffinPlane
for a, b, c, d being Element of AFP st AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c holds
ex p being Element of AFP st
( LIN b,c,p & LIN a,d,p )

proof end;

Lm4: for AFP being AffinPlane
for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & x <> y holds
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )

proof end;

Lm5: for AFP being AffinPlane
for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & a,x // b,y holds
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )

proof end;

theorem Th3: :: TRANSLAC:3

for AFP being AffinPlane
for a, x, y being Element of AFP
for f being Permutation of the carrier of AFP st f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y holds
y = f . x

proof end;

theorem Th4: :: TRANSLAC:4

for AFP being AffinPlane holds
( AFP is translational iff for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 )

proof end;

theorem Th5: :: TRANSLAC:5

for AFP being AffinPlane
for a being Element of AFP ex f being Permutation of the carrier of AFP st
( f is translation & f . a = a )

proof end;

Lm6: for AFP being AffinPlane
for a, b, x being Element of AFP st a <> b holds
ex y being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )

proof end;

Lm7: for AFP being AffinPlane
for a, b, y being Element of AFP st a <> b holds
ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )

proof end;

Lm8: for AFP being AffinPlane
for a, b, p, p9, q, q9, x, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 holds
y = y9

proof end;

theorem Th6: :: TRANSLAC:6

for AFP being AffinPlane
for a, b, p, q being Element of AFP st ( for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q ) & a,b // p,q & a,p // b,q & not LIN a,b,p holds
a,q // b,p

proof end;

Lm9: for AFP being AffinPlane
for a, b, p, p9, q, q9, x, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 holds
y = y9

proof end;

Lm10: for AFP being AffinPlane
for a, b, p, q, x, y being Element of AFP st a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p holds
( p <> q & LIN a,b,y )

proof end;

Lm11: for AFP being AffinPlane
for a, b, p, p9, q, q9, x, x9, y being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9,y & not LIN a,b,p & not LIN a,b,p9 holds
x = x9

proof end;

Lm12: for AFP being AffinPlane
for a, b being Element of AFP st AFP is translational & a <> b holds
ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )

proof end;

theorem Th7: :: TRANSLAC:7

for AFP being AffinPlane
for a, b being Element of AFP st AFP is translational holds
ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )

proof end;

theorem :: TRANSLAC:8

for AFP being AffinPlane st ( for a, b being Element of AFP ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b ) ) holds
AFP is translational

proof end;

theorem Th9: :: TRANSLAC:9

for AFP being AffinPlane
for a being Element of AFP
for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds
f * g = g * f

proof end;

theorem Th10: :: TRANSLAC:10

for AFP being AffinPlane
for f, g being Permutation of the carrier of AFP st AFP is translational & f is translation & g is translation holds
f * g = g * f

proof end;

theorem Th11: :: TRANSLAC:11

for AFP being AffinPlane
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

proof end;

theorem :: TRANSLAC:12

for AFP being 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 )

proof end;

theorem Th13: :: TRANSLAC:13

for AFP being AffinPlane
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

proof end;

theorem :: TRANSLAC:14

for AFP being AffinPlane
for g, f1, f2 being Permutation of the carrier of AFP st AFP is translational & AFP is Fanoian & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 holds
f1 = f2

proof end;