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 (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 (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
(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
and A3:
N is
being_line
and A4:
M <> N
and A5:
o in M
and A6:
o in N
and A7:
o <> a
and A8:
o <> a'
and A9:
o <> b
and
o <> b'
and A10:
o <> c
and A11:
o <> c'
and A12:
a in M
and A13:
b in M
and A14:
c in M
and A15:
a' in N
and A16:
b' in N
and A17:
c' in N
and A18:
a,
b' // b,
a'
and A19:
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;
b1,
c1' '||' c1,
b1'
by A19, DIRAF:45;
then A20:
v,
w' '||' w,
v'
by A1, Th5;
A21:
( 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, A5, A9, A13, AFF_1:39;
hence
contradiction
by A2, A3, A4, A5, A6, A8, A11, A15, A17, AFF_1:30;
:: thesis: verum
end;
LIN o,
c,
b
by A2, A5, A13, A14, AFF_1:33;
then
o,
c // o,
b
by AFF_1:def 1;
then
o1,
c1 '||' o1,
b1
by DIRAF:45;
then
q,
w '||' q,
v
by A1, Th5;
then consider r2 being
Real such that A22:
w - q = r2 * (v - q)
and A23:
r2 <> 0
by A9, A10, Lm2;
A24:
- r2 <> 0
by A23;
LIN o,
a,
b
by A2, A5, A12, A13, AFF_1:33;
then
o,
a // o,
b
by AFF_1:def 1;
then
o1,
a1 '||' o1,
b1
by DIRAF:45;
then
q,
u '||' q,
v
by A1, Th5;
then consider r1 being
Real such that A25:
u - q = r1 * (v - q)
and A26:
r1 <> 0
by A7, A9, Lm2;
A27:
(- r1) * (q - v) =
r1 * (- (q - v))
by RLVECT_1:38
.=
u - q
by A25, RLVECT_1:47
;
LIN o,
c',
b'
by A3, A6, A16, A17, AFF_1:33;
then
o,
c' // o,
b'
by AFF_1:def 1;
then
o1,
c1' '||' o1,
b1'
by DIRAF:45;
then A28:
q,
w' '||' q,
v'
by A1, Th5;
(- r2) * (q - v) =
r2 * (- (q - v))
by RLVECT_1:38
.=
w - q
by A22, RLVECT_1:47
;
then A29:
q - v = ((- r2) " ) * (w - q)
by A24, ANALOAF:12;
(- r2) " <> 0
by A24, XCMPLX_1:203;
then v' =
q + (((- ((- r2) " )) " ) * (w' - q))
by A20, A29, A28, A21, Th15
.=
q + (((- (- (r2 " ))) " ) * (w' - q))
by XCMPLX_1:224
.=
q + (r2 * (w' - q))
;
then A30:
v' - q = r2 * (w' - q)
by RLSUB_2:78;
LIN o,
a',
b'
by A3, A6, A15, A16, AFF_1:33;
then
o,
a' // o,
b'
by AFF_1:def 1;
then
o1,
a1' '||' o1,
b1'
by DIRAF:45;
then A31:
q,
u' '||' q,
v'
by A1, Th5;
a1,
b1' '||' b1,
a1'
by A18, DIRAF:45;
then
b1,
a1' '||' a1,
b1'
by DIRAF:27;
then A32:
v,
u' '||' u,
v'
by A1, Th5;
r1 " <> 0
by A26, XCMPLX_1:203;
then A33:
(r1 " ) * r2 <> 0
by A23, XCMPLX_1:6;
set s =
r1 * (r2 " );
A34:
u - q =
r1 * ((r2 " ) * (w - q))
by A25, A22, A23, ANALOAF:13
.=
(r1 * (r2 " )) * (w - q)
by RLVECT_1:def 9
;
- r1 <> 0
by A26;
then A35:
(- r1) " <> 0
by XCMPLX_1:203;
- r1 <> 0
by A26;
then
q - v = ((- r1) " ) * (u - q)
by A27, ANALOAF:13;
then v' =
q + (((- ((- r1) " )) " ) * (u' - q))
by A32, A35, A31, A21, Th15
.=
q + (((- (- (r1 " ))) " ) * (u' - q))
by XCMPLX_1:224
.=
q + (r1 * (u' - q))
;
then
v' - q = r1 * (u' - q)
by RLSUB_2:78;
then u' - q =
(r1 " ) * (r2 * (w' - q))
by A26, A30, ANALOAF:13
.=
((r1 " ) * r2) * (w' - q)
by RLVECT_1:def 9
;
then A36:
w' - q =
(((r1 " ) * r2) " ) * (u' - q)
by A33, ANALOAF:13
.=
(((r1 " ) " ) * (r2 " )) * (u' - q)
by XCMPLX_1:205
.=
(r1 * (r2 " )) * (u' - q)
;
1
* (w' - u) =
w' - u
by RLVECT_1:def 9
.=
((r1 * (r2 " )) * (u' - q)) - ((r1 * (r2 " )) * (w - q))
by A36, A34, 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