let V be RealLinearSpace; for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Pappian
let OAS be OAffinSpace; ( OAS = OASpace V implies Lambda OAS is Pappian )
assume A1:
OAS = OASpace V
; Lambda OAS is Pappian
set AS = Lambda OAS;
for M, N being Subset of (Lambda OAS)
for o, a, b, c, a9, b9, c9 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 <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
proof
let M,
N be
Subset of
(Lambda OAS);
for o, a, b, c, a9, b9, c9 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 <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
(Lambda OAS);
( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
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 <> a9
and A9:
o <> b
and
o <> b9
and A10:
o <> c
and A11:
o <> c9
and A12:
a in M
and A13:
b in M
and A14:
c in M
and A15:
a9 in N
and A16:
b9 in N
and A17:
c9 in N
and A18:
a,
b9 // b,
a9
and A19:
b,
c9 // c,
b9
;
a,c9 // c,a9
reconsider o1 =
o,
a1 =
a,
b1 =
b,
c1 =
c,
a19 =
a9,
b19 =
b9,
c19 =
c9 as
Element of
OAS by Th1;
reconsider q =
o1,
u =
a1,
v =
b1,
w =
c1,
u9 =
a19,
v9 =
b19,
w9 =
c19 as
VECTOR of
V by A1, Th3;
b1,
c19 '||' c1,
b19
by A19, DIRAF:38;
then A20:
v,
w9 '||' w,
v9
by A1, Th4;
A21:
( not
q,
v '||' q,
w9 & not
q,
v '||' q,
u9 )
proof
assume
(
q,
v '||' q,
w9 or
q,
v '||' q,
u9 )
;
contradiction
then
(
o1,
b1 '||' o1,
c19 or
o1,
b1 '||' o1,
a19 )
by A1, Th4;
then
(
o,
b // o,
c9 or
o,
b // o,
a9 )
by DIRAF:38;
then
(
LIN o,
b,
c9 or
LIN o,
b,
a9 )
by AFF_1:def 1;
then
(
c9 in M or
a9 in M )
by A2, A5, A9, A13, AFF_1:25;
hence
contradiction
by A2, A3, A4, A5, A6, A8, A11, A15, A17, AFF_1:18;
verum
end;
LIN o,
c,
b
by A2, A5, A13, A14, AFF_1:21;
then
o,
c // o,
b
by AFF_1:def 1;
then
o1,
c1 '||' o1,
b1
by DIRAF:38;
then
q,
w '||' q,
v
by A1, Th4;
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:21;
then
o,
a // o,
b
by AFF_1:def 1;
then
o1,
a1 '||' o1,
b1
by DIRAF:38;
then
q,
u '||' q,
v
by A1, Th4;
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:24
.=
u - q
by A25, RLVECT_1:33
;
LIN o,
c9,
b9
by A3, A6, A16, A17, AFF_1:21;
then
o,
c9 // o,
b9
by AFF_1:def 1;
then
o1,
c19 '||' o1,
b19
by DIRAF:38;
then A28:
q,
w9 '||' q,
v9
by A1, Th4;
(- r2) * (q - v) =
r2 * (- (q - v))
by RLVECT_1:24
.=
w - q
by A22, RLVECT_1:33
;
then A29:
q - v = ((- r2) ") * (w - q)
by A24, ANALOAF:5;
(- r2) " <> 0
by A24, XCMPLX_1:202;
then v9 =
q + (((- ((- r2) ")) ") * (w9 - q))
by A20, A29, A28, A21, Th10
.=
q + (((- (- (r2 "))) ") * (w9 - q))
by XCMPLX_1:222
.=
q + (r2 * (w9 - q))
;
then A30:
v9 - q = r2 * (w9 - q)
by RLSUB_2:61;
LIN o,
a9,
b9
by A3, A6, A15, A16, AFF_1:21;
then
o,
a9 // o,
b9
by AFF_1:def 1;
then
o1,
a19 '||' o1,
b19
by DIRAF:38;
then A31:
q,
u9 '||' q,
v9
by A1, Th4;
a1,
b19 '||' b1,
a19
by A18, DIRAF:38;
then
b1,
a19 '||' a1,
b19
by DIRAF:22;
then A32:
v,
u9 '||' u,
v9
by A1, Th4;
r1 " <> 0
by A26, XCMPLX_1:202;
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:6
.=
(r1 * (r2 ")) * (w - q)
by RLVECT_1:def 7
;
- r1 <> 0
by A26;
then A35:
(- r1) " <> 0
by XCMPLX_1:202;
- r1 <> 0
by A26;
then
q - v = ((- r1) ") * (u - q)
by A27, ANALOAF:6;
then v9 =
q + (((- ((- r1) ")) ") * (u9 - q))
by A32, A35, A31, A21, Th10
.=
q + (((- (- (r1 "))) ") * (u9 - q))
by XCMPLX_1:222
.=
q + (r1 * (u9 - q))
;
then
v9 - q = r1 * (u9 - q)
by RLSUB_2:61;
then u9 - q =
(r1 ") * (r2 * (w9 - q))
by A26, A30, ANALOAF:6
.=
((r1 ") * r2) * (w9 - q)
by RLVECT_1:def 7
;
then A36:
w9 - q =
(((r1 ") * r2) ") * (u9 - q)
by A33, ANALOAF:6
.=
(((r1 ") ") * (r2 ")) * (u9 - q)
by XCMPLX_1:204
.=
(r1 * (r2 ")) * (u9 - q)
;
1
* (w9 - u) =
w9 - u
by RLVECT_1:def 8
.=
((r1 * (r2 ")) * (u9 - q)) - ((r1 * (r2 ")) * (w - q))
by A36, A34, Lm3
.=
(r1 * (r2 ")) * ((u9 - q) - (w - q))
by RLVECT_1:34
.=
(r1 * (r2 ")) * (u9 - w)
by Lm3
;
then
(
u,
w9 // w,
u9 or
u,
w9 // u9,
w )
by ANALMETR:14;
then
u,
w9 '||' w,
u9
by GEOMTRAP:def 1;
then
a1,
c19 '||' c1,
a19
by A1, Th4;
hence
a,
c9 // c,
a9
by DIRAF:38;
verum
end;
hence
Lambda OAS is Pappian
by AFF_2:def 2; verum