:: Homotheties and Shears in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received September 21, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for AFP being AffinPlane holds
( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 )

proof end;

Lm2: for AFP being AffinPlane holds
( AFP is Moufangian iff for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 )

proof end;

Lm3: for AFP being AffinPlane st AFP is Moufangian holds
for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9

proof end;

Lm4: for AFP being AffinPlane st AFP is Moufangian holds
for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9

proof end;

theorem Th1: :: HOMOTHET:1

for AFP being AffinPlane
for a, b, o, p, p9, q, q9, x, y being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds
x,q // y,q9

proof end;

theorem Th2: :: HOMOTHET:2

for AFP being AffinPlane st ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) holds
AFP is Desarguesian

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm11: for AFP being AffinPlane
for a, b, o, r, x, y being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds
y = r

proof end;

Lm12: for AFP being AffinPlane
for a, b, o, r, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds
x = r

proof end;

Lm13: for AFP being AffinPlane
for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )

proof end;

Lm14: for AFP being AffinPlane
for a, b, o, t, x, y, z being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t

proof end;

Lm15: for AFP being AffinPlane
for a, b, o, t, x, y, z being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t

proof end;

Lm16: for AFP being AffinPlane
for a, b, o, t, x, y, z being Element of AFP st o <> a & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t

proof end;

Lm17: for AFP being AffinPlane
for a, b, o being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )

proof end;

theorem Th3: :: HOMOTHET:3

for AFP being AffinPlane st AFP is Desarguesian holds
for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )

proof end;

theorem :: HOMOTHET:4

for AFP being AffinPlane holds
( AFP is Desarguesian iff for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) by Th2, Th3;

definition

let AFP be AffinPlane;
let f be Permutation of the carrier of AFP;
let K be Subset of AFP;

pred f is_Sc K means :: HOMOTHET:def 1
( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) );

end;

:: deftheorem defines is_Sc HOMOTHET:def 1 :
for AFP being AffinPlane
for f being Permutation of the carrier of AFP
for K being Subset of AFP holds
( f is_Sc K iff ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) ) );

theorem Th5: :: HOMOTHET:5

for AFP being AffinPlane
for p being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP by TRANSGEO:97;

theorem Th6: :: HOMOTHET:6

for AFP being AffinPlane st ( for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) holds
AFP is Moufangian

proof end;

Lm18: for AFP being AffinPlane
for a, b, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) )
by AFF_1:34, AFF_1:35;

Lm19: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )

proof end;

Lm20: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )

proof end;

theorem Th7: :: HOMOTHET:7

for AFP being AffinPlane
for a, b, p, p9, q, q9, x, y being Element of AFP
for M, K being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y

proof end;

Lm21: for AFP being AffinPlane
for a, b, p, p9, q, q9, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y

proof end;

Lm22: for AFP being AffinPlane
for a, b, p, p9, q, q9, s, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y

proof end;

Lm23: for AFP being AffinPlane
for a, b, r, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r

proof end;

Lm24: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )

proof end;

Lm25: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f . a = b

proof end;

Lm26: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K

proof end;

Lm27: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is collineation

proof end;

Lm28: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is_Sc K
by Lm26, AFF_1:26, Lm27;

theorem Th8: :: HOMOTHET:8

for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )

proof end;

theorem :: HOMOTHET:9

for AFP being AffinPlane holds
( AFP is Moufangian iff for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) by Th6, Th8;