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, 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

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, 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

hence
Lambda OAS is Pappian
by AFF_2:def 2; :: thesis: verum
let M, N be Subset of (Lambda OAS); :: thesis: 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

let o, a, b, c, a9, b9, c9 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 <> 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 ; :: thesis: 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 )

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; :: thesis: verum

end;a,c9 // c,a9

let o, a, b, c, a9, b9, c9 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 <> 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 ; :: thesis: 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

LIN o,c,b
by A2, A5, A13, A14, AFF_1:21;
assume
( q,v '||' q,w9 or q,v '||' q,u9 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum