:: HOMOTHET semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for AFP being AffinPlane holds
( AFP satisfies_DES iff for o, a, a', p, p', q, q' being Element of AFP st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q' )
proof end;

Lm2: for AFP being AffinPlane holds
( AFP satisfies_TDES iff for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' )
proof end;

Lm3: for AFP being AffinPlane st AFP satisfies_TDES holds
for K being Subset of AFP
for o, a, b, c, a', b', c' being Element of AFP st K is_line & o in K & c in K & c' in K & not a in K & a <> b & LIN o,a,a' & a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K holds
LIN o,b,b'
proof end;

Lm4: for AFP being AffinPlane st AFP satisfies_TDES holds
for K, A, C being Subset of AFP
for p, q, a, a', b, b' being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' holds
a,b // a',b'
proof end;

theorem Th1: :: HOMOTHET:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFP being AffinPlane
for o, a, p, b, x, y, p', q, q' 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,p' & LIN o,p,q & LIN o,p,q' & p <> q & a <> x & o <> q & o <> x & a,p // b,p' & a,q // b,q' & x,p // y,p' & AFP satisfies_DES holds
x,q // y,q'
proof end;

theorem Th2: :: HOMOTHET:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_Dil & f . o = o & f . a = b ) ) holds
AFP satisfies_DES
proof end;

Lm5: for AFP being AffinPlane
for o, a, b, y, x 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
LIN o,a,x
proof end;

Lm6: for AFP being AffinPlane
for o, a, b, 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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, p' being Element of AFP st
( not LIN o,b,p & LIN o,p,p' & b,p // a,p' & p,y // p',x & LIN o,b,x ) ) ) )
proof end;

Lm7: for AFP being AffinPlane
for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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 & o <> b & 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) )
proof end;

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

Lm11: for AFP being AffinPlane
for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP satisfies_DES & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',r & LIN o,a,r ) holds
y = r
proof end;

Lm12: for AFP being AffinPlane
for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP satisfies_DES & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,r // p',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 satisfies_DES & 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) )
proof end;

Lm14: for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of AFP st AFP satisfies_DES & o <> a & o <> b & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) holds
x,z // y,t
proof end;

Lm15: for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of AFP st AFP satisfies_DES & o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',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 o, a, b, x, y, z, t being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,x & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & LIN o,a,z & ex p, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) holds
x,z // y,t
proof end;

Lm17: for AFP being AffinPlane
for o, a, b being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & o <> b & LIN o,a,b & AFP satisfies_DES & ( 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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) ) holds
( f is_Dil & f . o = o & f . a = b )
proof end;

theorem Th3: :: HOMOTHET:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFP being AffinPlane st AFP satisfies_DES 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_Dil & f . o = o & f . a = b )
proof end;

theorem :: HOMOTHET:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFP being AffinPlane holds
( AFP satisfies_DES 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_Dil & 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 :Def1: :: HOMOTHET:def 1
( f is_Col & K is_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 Def1 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_Col & K is_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th6: :: HOMOTHET:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 satisfies_TDES
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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )
proof end;

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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) )
proof end;

theorem Th7: :: HOMOTHET:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFP being AffinPlane
for p, q, p', q', a, b, x, y being Element of AFP
for K, M being Subset of AFP st K // M & p in K & q in K & p' in K & q' in K & AFP satisfies_TDES & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p',x & p,b // p',y & q,a // q',x holds
q,b // q',y
proof end;

Lm21: for AFP being AffinPlane
for a, b, x, p, p', y, q, q' being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP satisfies_TDES & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x holds
q,b // q',y
proof end;

Lm22: for AFP being AffinPlane
for a, b, x, p, p', y, q, q', s being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP satisfies_TDES & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x & x,s // K & q,b // q',s holds
s = y
proof end;

Lm23: for AFP being AffinPlane
for a, b, x, y, r being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP satisfies_TDES & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',r & p,b // p',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 satisfies_TDES 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',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 & 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',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 & AFP satisfies_TDES & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f is_Col
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 & AFP satisfies_TDES & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f is_Sc K
proof end;

theorem Th8: :: HOMOTHET:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 satisfies_TDES holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
proof end;

theorem :: HOMOTHET:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFP being AffinPlane holds
( AFP satisfies_TDES 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;