:: Fanoian, Pappian and Desarguesian Affine Spaces
:: by Krzysztof Pra\.zmowski
::
:: Received November 16, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: PAPDESAF:1
canceled;
theorem Th2: :: PAPDESAF:2
theorem Th3: :: PAPDESAF:3
theorem Th4: :: PAPDESAF:4
theorem Th5: :: PAPDESAF:5
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 )
theorem :: PAPDESAF:6
definition
let AS be
AffinSpace;
canceled;canceled;canceled;canceled;redefine attr AS is
Fanoian means :
Def5:
:: PAPDESAF:def 5
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
( 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;
:: deftheorem PAPDESAF:def 1 :
canceled;
:: deftheorem PAPDESAF:def 2 :
canceled;
:: deftheorem PAPDESAF:def 3 :
canceled;
:: deftheorem PAPDESAF:def 4 :
canceled;
:: deftheorem Def5 defines Fanoian PAPDESAF:def 5 :
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 PAPDESAF:def 6 :
canceled;
:: deftheorem PAPDESAF:def 7 :
canceled;
:: deftheorem PAPDESAF:def 8 :
canceled;
:: deftheorem PAPDESAF:def 9 :
canceled;
:: deftheorem PAPDESAF:def 10 :
canceled;
:: deftheorem Def11 defines Pappian PAPDESAF:def 11 :
:: deftheorem Def12 defines Desarguesian PAPDESAF:def 12 :
:: deftheorem Def13 defines Moufangian PAPDESAF:def 13 :
:: deftheorem Def14 defines translation PAPDESAF:def 14 :
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_DES means :
Def15:
:: PAPDESAF:def 15
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
LIN o,
a,
b & not
LIN o,
a,
c &
a,
b // a1,
b1 &
a,
c // a1,
c1 holds
b,
c // b1,
c1;
end;
:: deftheorem Def15 defines satisfying_DES PAPDESAF:def 15 :
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
LIN o,
a,
b & not
LIN o,
a,
c &
a,
b // a1,
b1 &
a,
c // a1,
c1 holds
b,
c // b1,
c1 );
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_DES_1 means :
Def16:
:: PAPDESAF:def 16
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
LIN o,
a,
b & not
LIN o,
a,
c &
a,
b // b1,
a1 &
a,
c // c1,
a1 holds
b,
c // c1,
b1;
end;
:: deftheorem Def16 defines satisfying_DES_1 PAPDESAF:def 16 :
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
LIN o,
a,
b & not
LIN o,
a,
c &
a,
b // b1,
a1 &
a,
c // c1,
a1 holds
b,
c // c1,
b1 );
theorem :: PAPDESAF:7
canceled;
theorem :: PAPDESAF:8
canceled;
theorem :: PAPDESAF:9
canceled;
theorem :: PAPDESAF:10
canceled;
theorem Th11: :: PAPDESAF:11
theorem Th12: :: PAPDESAF:12
for
OAS being
OAffinSpace for
o,
a,
b,
a',
b' being
Element of the
carrier of
OAS st not
LIN o,
a,
b &
a,
o // o,
a' &
LIN o,
b,
b' &
a,
b '||' a',
b' holds
(
b,
o // o,
b' &
a,
b // b',
a' )
theorem Th13: :: PAPDESAF:13
for
OAS being
OAffinSpace for
o,
a,
b,
a',
b' being
Element of the
carrier of
OAS st not
LIN o,
a,
b &
o,
a // o,
a' &
LIN o,
b,
b' &
a,
b '||' a',
b' holds
(
o,
b // o,
b' &
a,
b // a',
b' )
theorem Th14: :: PAPDESAF:14
theorem Th15: :: PAPDESAF:15
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) )
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 )
theorem :: PAPDESAF:16
canceled;
theorem Th17: :: PAPDESAF:17
theorem :: PAPDESAF:18
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 )
Lm3:
for V being RealLinearSpace
for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v
theorem Th19: :: PAPDESAF:19
theorem Th20: :: PAPDESAF:20
theorem Th21: :: PAPDESAF:21
theorem Th22: :: PAPDESAF:22
theorem Th23: :: PAPDESAF:23
theorem Th24: :: PAPDESAF:24