let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds

Lambda OAS is translational

let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies Lambda OAS is translational )

assume A1: OAS = OASpace V ; :: thesis: Lambda OAS is translational

set AS = Lambda OAS;

for A, P, C being Subset of (Lambda OAS)

for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

Lambda OAS is translational

let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies Lambda OAS is translational )

assume A1: OAS = OASpace V ; :: thesis: Lambda OAS is translational

set AS = Lambda OAS;

for A, P, C being Subset of (Lambda OAS)

for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

proof

hence
Lambda OAS is translational
by AFF_2:def 11; :: thesis: verum
let A, P, C be Subset of (Lambda OAS); :: thesis: for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let a, b, c, a9, b9, c9 be Element of (Lambda OAS); :: thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A2: A // P and

A3: A // C and

A4: a in A and

A5: a9 in A and

A6: b in P and

A7: b9 in P and

A8: c in C and

A9: c9 in C and

A10: A is being_line and

A11: P is being_line and

A12: C is being_line and

A13: A <> P and

A14: A <> C and

A15: a,b // a9,b9 and

A16: a,c // a9,c9 ; :: thesis: b,c // b9,c9

reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;

reconsider u = a1, v = b1, w = c1, u9 = a19 as VECTOR of V by A1, Th3;

end;b,c // b9,c9

let a, b, c, a9, b9, c9 be Element of (Lambda OAS); :: thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A2: A // P and

A3: A // C and

A4: a in A and

A5: a9 in A and

A6: b in P and

A7: b9 in P and

A8: c in C and

A9: c9 in C and

A10: A is being_line and

A11: P is being_line and

A12: C is being_line and

A13: A <> P and

A14: A <> C and

A15: a,b // a9,b9 and

A16: a,c // a9,c9 ; :: thesis: b,c // b9,c9

reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;

reconsider u = a1, v = b1, w = c1, u9 = a19 as VECTOR of V by A1, Th3;

A17: now :: thesis: ( a <> a9 implies b,c // b9,c9 )

assume A18:
a <> a9
; :: thesis: b,c // b9,c9

A19: not a1,a19,b1 are_collinear

then A21: a1,a19 '||' c1,c19 by DIRAF:38;

a,a9 // b,b9 by A2, A4, A5, A6, A7, AFF_1:39;

then A22: a1,a19 '||' b1,b19 by DIRAF:38;

set v99 = (u9 + v) - u;

set w99 = (u9 + w) - u;

reconsider b199 = (u9 + v) - u, c199 = (u9 + w) - u as Element of OAS by A1, Th3;

((u9 + w) - u) - ((u9 + v) - u) = (u9 + w) - (((u9 + v) - u) + u) by RLVECT_1:27

.= (u9 + w) - (u9 + v) by RLSUB_2:61

.= ((w + u9) - u9) - v by RLVECT_1:27

.= w - v by RLSUB_2:61 ;

then v,w // (u9 + v) - u,(u9 + w) - u by ANALOAF:15;

then A23: v,w '||' (u9 + v) - u,(u9 + w) - u by GEOMTRAP:def 1;

u,u9 // v,(u9 + v) - u by ANALOAF:16;

then u,u9 '||' v,(u9 + v) - u by GEOMTRAP:def 1;

then A24: a1,a19 '||' b1,b199 by A1, Th4;

u,w // u9,(u9 + w) - u by ANALOAF:16;

then u,w '||' u9,(u9 + w) - u by GEOMTRAP:def 1;

then A25: a1,c1 '||' a19,c199 by A1, Th4;

u,u9 // w,(u9 + w) - u by ANALOAF:16;

then u,u9 '||' w,(u9 + w) - u by GEOMTRAP:def 1;

then A26: a1,a19 '||' c1,c199 by A1, Th4;

u,v // u9,(u9 + v) - u by ANALOAF:16;

then u,v '||' u9,(u9 + v) - u by GEOMTRAP:def 1;

then A27: a1,b1 '||' a19,b199 by A1, Th4;

a1,c1 '||' a19,c19 by A16, DIRAF:38;

then A28: c199 = c19 by A20, A21, A26, A25, PASCH:5;

a1,b1 '||' a19,b19 by A15, DIRAF:38;

then b199 = b19 by A19, A22, A24, A27, PASCH:5;

then b1,c1 '||' b19,c19 by A1, A28, A23, Th4;

hence b,c // b9,c9 by DIRAF:38; :: thesis: verum

end;A19: not a1,a19,b1 are_collinear

proof

A20:
not a1,a19,c1 are_collinear
assume
a1,a19,b1 are_collinear
; :: thesis: contradiction

then LIN a,a9,b by Th2;

then b in A by A4, A5, A10, A18, AFF_1:25;

hence contradiction by A2, A6, A13, AFF_1:45; :: thesis: verum

end;then LIN a,a9,b by Th2;

then b in A by A4, A5, A10, A18, AFF_1:25;

hence contradiction by A2, A6, A13, AFF_1:45; :: thesis: verum

proof

a,a9 // c,c9
by A3, A4, A5, A8, A9, AFF_1:39;
assume
a1,a19,c1 are_collinear
; :: thesis: contradiction

then LIN a,a9,c by Th2;

then c in A by A4, A5, A10, A18, AFF_1:25;

hence contradiction by A3, A8, A14, AFF_1:45; :: thesis: verum

end;then LIN a,a9,c by Th2;

then c in A by A4, A5, A10, A18, AFF_1:25;

hence contradiction by A3, A8, A14, AFF_1:45; :: thesis: verum

then A21: a1,a19 '||' c1,c19 by DIRAF:38;

a,a9 // b,b9 by A2, A4, A5, A6, A7, AFF_1:39;

then A22: a1,a19 '||' b1,b19 by DIRAF:38;

set v99 = (u9 + v) - u;

set w99 = (u9 + w) - u;

reconsider b199 = (u9 + v) - u, c199 = (u9 + w) - u as Element of OAS by A1, Th3;

((u9 + w) - u) - ((u9 + v) - u) = (u9 + w) - (((u9 + v) - u) + u) by RLVECT_1:27

.= (u9 + w) - (u9 + v) by RLSUB_2:61

.= ((w + u9) - u9) - v by RLVECT_1:27

.= w - v by RLSUB_2:61 ;

then v,w // (u9 + v) - u,(u9 + w) - u by ANALOAF:15;

then A23: v,w '||' (u9 + v) - u,(u9 + w) - u by GEOMTRAP:def 1;

u,u9 // v,(u9 + v) - u by ANALOAF:16;

then u,u9 '||' v,(u9 + v) - u by GEOMTRAP:def 1;

then A24: a1,a19 '||' b1,b199 by A1, Th4;

u,w // u9,(u9 + w) - u by ANALOAF:16;

then u,w '||' u9,(u9 + w) - u by GEOMTRAP:def 1;

then A25: a1,c1 '||' a19,c199 by A1, Th4;

u,u9 // w,(u9 + w) - u by ANALOAF:16;

then u,u9 '||' w,(u9 + w) - u by GEOMTRAP:def 1;

then A26: a1,a19 '||' c1,c199 by A1, Th4;

u,v // u9,(u9 + v) - u by ANALOAF:16;

then u,v '||' u9,(u9 + v) - u by GEOMTRAP:def 1;

then A27: a1,b1 '||' a19,b199 by A1, Th4;

a1,c1 '||' a19,c19 by A16, DIRAF:38;

then A28: c199 = c19 by A20, A21, A26, A25, PASCH:5;

a1,b1 '||' a19,b19 by A15, DIRAF:38;

then b199 = b19 by A19, A22, A24, A27, PASCH:5;

then b1,c1 '||' b19,c19 by A1, A28, A23, Th4;

hence b,c // b9,c9 by DIRAF:38; :: thesis: verum

now :: thesis: ( a = a9 implies b,c // b9,c9 )

hence
b,c // b9,c9
by A17; :: thesis: verumassume A29:
a = a9
; :: thesis: b,c // b9,c9

A30: c = c9

end;A30: c = c9

proof

b = b9
LIN a,c,c9
by A16, A29, AFF_1:def 1;

then A31: LIN c,c9,a by AFF_1:6;

assume c <> c9 ; :: thesis: contradiction

then a in C by A8, A9, A12, A31, AFF_1:25;

hence contradiction by A3, A4, A14, AFF_1:45; :: thesis: verum

end;then A31: LIN c,c9,a by AFF_1:6;

assume c <> c9 ; :: thesis: contradiction

then a in C by A8, A9, A12, A31, AFF_1:25;

hence contradiction by A3, A4, A14, AFF_1:45; :: thesis: verum

proof

hence
b,c // b9,c9
by A30, AFF_1:2; :: thesis: verum
LIN a,b,b9
by A15, A29, AFF_1:def 1;

then A32: LIN b,b9,a by AFF_1:6;

assume b <> b9 ; :: thesis: contradiction

then a in P by A6, A7, A11, A32, AFF_1:25;

hence contradiction by A2, A4, A13, AFF_1:45; :: thesis: verum

end;then A32: LIN b,b9,a by AFF_1:6;

assume b <> b9 ; :: thesis: contradiction

then a in P by A6, A7, A11, A32, AFF_1:25;

hence contradiction by A2, A4, A13, AFF_1:45; :: thesis: verum