let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Pappian
let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies Lambda OAS is Pappian )
assume A1:
OAS = OASpace V
; :: thesis: Lambda OAS is Pappian
set AS = Lambda OAS;
for M, N being Subset of (Lambda OAS)
for o, a, b, c, a', b', c' being Element of the carrier of (Lambda OAS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
proof
let M,
N be
Subset of
(Lambda OAS);
:: thesis: for o, a, b, c, a', b', c' being Element of the carrier of (Lambda OAS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'let o,
a,
b,
c,
a',
b',
c' be
Element of the
carrier of
(Lambda OAS);
:: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' implies a,c' // c,a' )
assume that A2:
(
M is
being_line &
N is
being_line )
and A3:
M <> N
and A4:
(
o in M &
o in N )
and A5:
(
o <> a &
o <> a' &
o <> b &
o <> b' &
o <> c &
o <> c' )
and A6:
(
a in M &
b in M &
c in M &
a' in N &
b' in N &
c' in N )
and A7:
(
a,
b' // b,
a' &
b,
c' // c,
b' )
;
:: thesis: a,c' // c,a'
reconsider o1 =
o,
a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of
OAS by Th2;
reconsider q =
o1,
u =
a1,
v =
b1,
w =
c1,
u' =
a1',
v' =
b1',
w' =
c1' as
VECTOR of
V by A1, Th4;
(
a1,
b1' '||' b1,
a1' &
b1,
c1' '||' c1,
b1' )
by A7, DIRAF:45;
then
(
b1,
a1' '||' a1,
b1' &
b1,
c1' '||' c1,
b1' )
by DIRAF:27;
then A8:
(
v,
u' '||' u,
v' &
v,
w' '||' w,
v' )
by A1, Th5;
A9:
(
q,
u '||' q,
v &
q,
w '||' q,
v )
proof
(
LIN o,
a,
b &
LIN o,
c,
b )
by A2, A4, A6, AFF_1:33;
then
(
o,
a // o,
b &
o,
c // o,
b )
by AFF_1:def 1;
then
(
o1,
a1 '||' o1,
b1 &
o1,
c1 '||' o1,
b1 )
by DIRAF:45;
hence
(
q,
u '||' q,
v &
q,
w '||' q,
v )
by A1, Th5;
:: thesis: verum
end;
then consider r1 being
Real such that A10:
(
u - q = r1 * (v - q) &
r1 <> 0 )
by A5, Lm2;
consider r2 being
Real such that A11:
(
w - q = r2 * (v - q) &
r2 <> 0 )
by A5, A9, Lm2;
A12:
- r1 <> 0
by A10;
(- r1) * (q - v) =
r1 * (- (q - v))
by RLVECT_1:38
.=
u - q
by A10, RLVECT_1:47
;
then A13:
q - v = ((- r1) " ) * (u - q)
by A12, ANALOAF:13;
A14:
(
- r1 <> 0 &
- r2 <> 0 )
by A10, A11;
(- r2) * (q - v) =
r2 * (- (q - v))
by RLVECT_1:38
.=
w - q
by A11, RLVECT_1:47
;
then A15:
q - v = ((- r2) " ) * (w - q)
by A14, ANALOAF:12;
A16:
(
(- r1) " <> 0 &
(- r2) " <> 0 )
by A14, XCMPLX_1:203;
A17:
(
r1 " <> 0 &
r2 " <> 0 )
by A10, A11, XCMPLX_1:203;
A18:
(
q,
u' '||' q,
v' &
q,
w' '||' q,
v' )
proof
(
LIN o,
a',
b' &
LIN o,
c',
b' )
by A2, A4, A6, AFF_1:33;
then
(
o,
a' // o,
b' &
o,
c' // o,
b' )
by AFF_1:def 1;
then
(
o1,
a1' '||' o1,
b1' &
o1,
c1' '||' o1,
b1' )
by DIRAF:45;
hence
(
q,
u' '||' q,
v' &
q,
w' '||' q,
v' )
by A1, Th5;
:: thesis: verum
end;
A19:
( not
q,
v '||' q,
w' & not
q,
v '||' q,
u' )
proof
assume
(
q,
v '||' q,
w' or
q,
v '||' q,
u' )
;
:: thesis: contradiction
then
(
o1,
b1 '||' o1,
c1' or
o1,
b1 '||' o1,
a1' )
by A1, Th5;
then
(
o,
b // o,
c' or
o,
b // o,
a' )
by DIRAF:45;
then
(
LIN o,
b,
c' or
LIN o,
b,
a' )
by AFF_1:def 1;
then
(
c' in M or
a' in M )
by A2, A4, A5, A6, AFF_1:39;
hence
contradiction
by A2, A3, A4, A5, A6, AFF_1:30;
:: thesis: verum
end;
set s =
r1 * (r2 " );
v' =
q + (((- ((- r2) " )) " ) * (w' - q))
by A8, A15, A16, A18, A19, Th15
.=
q + (((- (- (r2 " ))) " ) * (w' - q))
by XCMPLX_1:224
.=
q + (r2 * (w' - q))
;
then A20:
v' - q = r2 * (w' - q)
by RLSUB_2:78;
v' =
q + (((- ((- r1) " )) " ) * (u' - q))
by A8, A13, A16, A18, A19, Th15
.=
q + (((- (- (r1 " ))) " ) * (u' - q))
by XCMPLX_1:224
.=
q + (r1 * (u' - q))
;
then
v' - q = r1 * (u' - q)
by RLSUB_2:78;
then A21:
u' - q =
(r1 " ) * (r2 * (w' - q))
by A10, A20, ANALOAF:13
.=
((r1 " ) * r2) * (w' - q)
by RLVECT_1:def 9
;
(r1 " ) * r2 <> 0
by A11, A17, XCMPLX_1:6;
then A22:
w' - q =
(((r1 " ) * r2) " ) * (u' - q)
by A21, ANALOAF:13
.=
(((r1 " ) " ) * (r2 " )) * (u' - q)
by XCMPLX_1:205
.=
(r1 * (r2 " )) * (u' - q)
;
A23:
u - q =
r1 * ((r2 " ) * (w - q))
by A10, A11, ANALOAF:13
.=
(r1 * (r2 " )) * (w - q)
by RLVECT_1:def 9
;
1
* (w' - u) =
w' - u
by RLVECT_1:def 9
.=
((r1 * (r2 " )) * (u' - q)) - ((r1 * (r2 " )) * (w - q))
by A22, A23, Lm3
.=
(r1 * (r2 " )) * ((u' - q) - (w - q))
by RLVECT_1:48
.=
(r1 * (r2 " )) * (u' - w)
by Lm3
;
then
(
u,
w' // w,
u' or
u,
w' // u',
w )
by ANALMETR:18;
then
u,
w' '||' w,
u'
by GEOMTRAP:def 1;
then
a1,
c1' '||' c1,
a1'
by A1, Th5;
hence
a,
c' // c,
a'
by DIRAF:45;
:: thesis: verum
end;
hence
Lambda OAS is Pappian
by AFF_2:def 2; :: thesis: verum