:: by Krzysztof Pra\.zmowski

::

:: Received November 16, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

registration

let OAS be OAffinSpace;

correctness

coherence

( Lambda OAS is AffinSpace-like & not Lambda OAS is trivial );

by DIRAF:41;

end;
correctness

coherence

( Lambda OAS is AffinSpace-like & not Lambda OAS is trivial );

by DIRAF:41;

registration
end;

theorem Th1: :: PAPDESAF:1

for OAS being OAffinSpace

for x being set holds

( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )

for x being set holds

( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )

proof end;

theorem Th2: :: PAPDESAF:2

for OAS being OAffinSpace

for a, b, c being Element of OAS

for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds

( a,b,c are_collinear iff LIN a9,b9,c9 )

for a, b, c being Element of OAS

for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds

( a,b,c are_collinear iff LIN a9,b9,c9 )

proof end;

theorem Th3: :: PAPDESAF:3

for V being RealLinearSpace

for x being set holds

( x is Element of (OASpace V) iff x is VECTOR of V )

for x being set holds

( x is Element of (OASpace V) iff x is VECTOR of V )

proof end;

theorem Th4: :: PAPDESAF:4

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

for a, b, c, d being Element of OAS

for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds

( a,b '||' c,d iff u,v '||' w,y )

for OAS being OAffinSpace st OAS = OASpace V holds

for a, b, c, d being Element of OAS

for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds

( a,b '||' c,d iff u,v '||' w,y )

proof end;

theorem :: PAPDESAF:5

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

for OAS being OAffinSpace st OAS = OASpace V holds

ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

proof end;

definition

let AS be AffinSpace;

( 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

a,b // a,c )

end;
redefine attr AS is Fanoian means :: PAPDESAF: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

a,b // a,c;

compatibility for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds

a,b // a,c;

( 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

a,b // a,c )

proof end;

:: deftheorem defines Fanoian PAPDESAF: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

a,b // a,c );

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

a,b // a,c );

:: deftheorem Def2 defines Pappian PAPDESAF:def 2 :

for IT being OAffinSpace holds

( IT is Pappian iff Lambda IT is Pappian );

for IT being OAffinSpace holds

( IT is Pappian iff Lambda IT is Pappian );

:: deftheorem Def3 defines Desarguesian PAPDESAF:def 3 :

for IT being OAffinSpace holds

( IT is Desarguesian iff Lambda IT is Desarguesian );

for IT being OAffinSpace holds

( IT is Desarguesian iff Lambda IT is Desarguesian );

:: deftheorem Def4 defines Moufangian PAPDESAF:def 4 :

for IT being OAffinSpace holds

( IT is Moufangian iff Lambda IT is Moufangian );

for IT being OAffinSpace holds

( IT is Moufangian iff Lambda IT is Moufangian );

:: deftheorem Def5 defines translation PAPDESAF:def 5 :

for IT being OAffinSpace holds

( IT is translation iff Lambda IT is translational );

for IT being OAffinSpace holds

( IT is translation iff Lambda IT is translational );

definition

let OAS be OAffinSpace;

end;
attr OAS is satisfying_DES means :: PAPDESAF:def 6

for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds

b,c // b1,c1;

for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds

b,c // b1,c1;

:: deftheorem defines satisfying_DES PAPDESAF:def 6 :

for OAS being OAffinSpace holds

( OAS is satisfying_DES iff for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds

b,c // b1,c1 );

for OAS being OAffinSpace holds

( OAS is satisfying_DES iff for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1 & a,c // a1,c1 holds

b,c // b1,c1 );

definition

let OAS be OAffinSpace;

end;
attr OAS is satisfying_DES_1 means :: PAPDESAF:def 7

for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds

b,c // c1,b1;

for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds

b,c // c1,b1;

:: deftheorem defines satisfying_DES_1 PAPDESAF:def 7 :

for OAS being OAffinSpace holds

( OAS is satisfying_DES_1 iff for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds

b,c // c1,b1 );

for OAS being OAffinSpace holds

( OAS is satisfying_DES_1 iff for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 holds

b,c // c1,b1 );

theorem Th7: :: PAPDESAF:7

for OAS being OAffinSpace

for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & a,o // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds

( b,o // o,b9 & a,b // b9,a9 )

for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & a,o // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds

( b,o // o,b9 & a,b // b9,a9 )

proof end;

theorem Th8: :: PAPDESAF:8

for OAS being OAffinSpace

for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds

( o,b // o,b9 & a,b // a9,b9 )

for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds

( o,b // o,b9 & a,b // a9,b9 )

proof end;

theorem Th10: :: PAPDESAF:10

for V being RealLinearSpace

for o, u, v, u1, v1 being VECTOR of V

for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds

( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )

for o, u, v, u1, v1 being VECTOR of V

for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds

( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )

proof end;

Lm1: for V being RealLinearSpace

for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds

ex r being Real st

( v - u = r * (w - v) & 0 < r )

proof end;

theorem Th11: :: PAPDESAF:11

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

OAS is satisfying_DES_1

for OAS being OAffinSpace st OAS = OASpace V holds

OAS is satisfying_DES_1

proof end;

theorem :: PAPDESAF:12

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

( OAS is satisfying_DES_1 & OAS is satisfying_DES ) by Th6, Th11;

for OAS being OAffinSpace st OAS = OASpace V holds

( OAS is satisfying_DES_1 & OAS is satisfying_DES ) by Th6, Th11;

Lm2: for V being RealLinearSpace

for y, u, v being VECTOR of V st y,u '||' y,v & y <> u & y <> v holds

ex r being Real st

( u - y = r * (v - y) & r <> 0 )

proof end;

Lm3: for V being RealLinearSpace

for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v

proof end;

theorem Th13: :: PAPDESAF:13

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Pappian

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Pappian

proof end;

theorem Th14: :: PAPDESAF:14

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Desarguesian by Th9, Th11;

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Desarguesian by Th9, Th11;

theorem Th16: :: PAPDESAF:16

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Moufangian

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is Moufangian

proof end;

theorem Th17: :: PAPDESAF:17

for V being RealLinearSpace

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is translational

for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is translational

proof end;

registration

ex b_{1} being OAffinSpace st

( b_{1} is Pappian & b_{1} is Desarguesian & b_{1} is Moufangian & b_{1} is translation )
end;

cluster V54() non trivial OAffinSpace-like Pappian Desarguesian Moufangian translation for AffinStruct ;

existence ex b

( b

proof end;

registration

ex b_{1} being AffinPlane st

( b_{1} is strict & b_{1} is Fanoian & b_{1} is Pappian & b_{1} is Desarguesian & b_{1} is Moufangian & b_{1} is translational )
end;

cluster V54() non trivial strict AffinSpace-like 2-dimensional Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;

existence ex b

( b

proof end;

registration

ex b_{1} being AffinSpace st

( b_{1} is strict & b_{1} is Fanoian & b_{1} is Pappian & b_{1} is Desarguesian & b_{1} is Moufangian & b_{1} is translational )
end;

cluster V54() non trivial strict AffinSpace-like Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;

existence ex b

( b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;