let V be RealLinearSpace; :: thesis: for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle holds

u1,v1,w1 are_LinDep

let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle implies u1,v1,w1 are_LinDep )

assume that

A1: not o is zero and

A2: u,v,w are_Prop_Vect and

A3: u2,v2,w2 are_Prop_Vect and

A4: u1,v1,w1 are_Prop_Vect and

A5: o,u,v,w,u2,v2,w2 are_perspective and

A6: not are_Prop o,u2 and

A7: not are_Prop o,v2 and

A8: not are_Prop o,w2 and

A9: not are_Prop u,u2 and

A10: not are_Prop v,v2 and

A11: not are_Prop w,w2 and

A12: not o,u,v are_LinDep and

A13: not o,u,w are_LinDep and

A14: not o,v,w are_LinDep and

A15: u,v,w,u1,v1,w1 lie_on_a_triangle and

A16: u2,v2,w2,u1,v1,w1 lie_on_a_triangle ; :: thesis: u1,v1,w1 are_LinDep

A17: not w is zero by A2;

A18: ( o,w,w2 are_LinDep & not are_Prop w,o ) by A5, A13, ANPROJ_1:11;

A19: not w2 is zero by A3;

then o,w,w2 are_Prop_Vect by A1, A17;

then consider a3, b3 being Real such that

A20: b3 * w2 = o + (a3 * w) and

a3 <> 0 and

A21: b3 <> 0 by A8, A11, A18, Th6;

A22: not u is zero by A2;

A23: not v is zero by A2;

A24: ( o,v,v2 are_LinDep & not are_Prop o,v ) by A5, A12, ANPROJ_1:11;

A25: ( o,u,u2 are_LinDep & not are_Prop o,u ) by A5, A12, ANPROJ_1:11;

A26: not u2 is zero by A3;

then o,u,u2 are_Prop_Vect by A1, A22;

then consider a1, b1 being Real such that

A27: b1 * u2 = o + (a1 * u) and

A28: a1 <> 0 and

A29: b1 <> 0 by A6, A9, A25, Th6;

A30: not v2 is zero by A3;

then o,v,v2 are_Prop_Vect by A1, A23;

then consider a2, b2 being Real such that

A31: b2 * v2 = o + (a2 * v) and

A32: a2 <> 0 and

A33: b2 <> 0 by A7, A10, A24, Th6;

set u29 = o + (a1 * u);

set v29 = o + (a2 * v);

set w29 = o + (a3 * w);

A34: are_Prop v2,o + (a2 * v) by A31, A33, Lm9;

A35: not o + (a2 * v) is zero by A30, A31, A33, Lm11;

A36: are_Prop w2,o + (a3 * w) by A20, A21, Lm9;

A37: ( u,v,w1 are_LinDep & not are_Prop u,v ) by A12, A15, ANPROJ_1:12;

A38: not w1 is zero by A4;

then u,v,w1 are_Prop_Vect by A22, A23;

then consider c3, d3 being Real such that

A39: w1 = (c3 * u) + (d3 * v) by A37, Th7;

A40: are_Prop u2,o + (a1 * u) by A27, A29, Lm9;

A41: ( v,w,u1 are_LinDep & not are_Prop v,w ) by A14, A15, ANPROJ_1:12;

A42: not u1 is zero by A4;

then v,w,u1 are_Prop_Vect by A23, A17;

then consider c1, d1 being Real such that

A43: u1 = (c1 * v) + (d1 * w) by A41, Th7;

v2,w2,u1 are_LinDep by A16;

then A44: o + (a2 * v),o + (a3 * w),u1 are_LinDep by A34, A36, ANPROJ_1:4;

A45: not are_Prop o + (a2 * v),o + (a3 * w) by A14, A32, Lm10;

A46: not o + (a3 * w) is zero by A19, A20, A21, Lm11;

then o + (a2 * v),o + (a3 * w),u1 are_Prop_Vect by A42, A35;

then consider A1, B1 being Real such that

A47: u1 = (A1 * (o + (a2 * v))) + (B1 * (o + (a3 * w))) by A44, A45, Th7;

A48: ( u,w,v1 are_LinDep & not are_Prop u,w ) by A13, A15, ANPROJ_1:12;

A49: not v1 is zero by A4;

then u,w,v1 are_Prop_Vect by A22, A17;

then consider c2, d2 being Real such that

A50: v1 = (c2 * u) + (d2 * w) by A48, Th7;

A51: u1 = (((A1 + B1) * o) + ((A1 * a2) * v)) + ((B1 * a3) * w) by A47, Lm12;

u2,v2,w1 are_LinDep by A16;

then A52: o + (a1 * u),o + (a2 * v),w1 are_LinDep by A40, A34, ANPROJ_1:4;

A53: not are_Prop o + (a1 * u),o + (a2 * v) by A12, A28, Lm10;

A54: not o + (a1 * u) is zero by A26, A27, A29, Lm11;

then o + (a1 * u),o + (a2 * v),w1 are_Prop_Vect by A38, A35;

then consider A3, B3 being Real such that

A55: w1 = (A3 * (o + (a1 * u))) + (B3 * (o + (a2 * v))) by A52, A53, Th7;

u2,w2,v1 are_LinDep by A16;

then A56: o + (a1 * u),o + (a3 * w),v1 are_LinDep by A40, A36, ANPROJ_1:4;

A57: not are_Prop o + (a1 * u),o + (a3 * w) by A13, A28, Lm10;

A58: w1 = (((A3 + B3) * o) + ((A3 * a1) * u)) + ((B3 * a2) * v) by A55, Lm12;

o + (a1 * u),o + (a3 * w),v1 are_Prop_Vect by A49, A54, A46;

then consider A2, B2 being Real such that

A59: v1 = (A2 * (o + (a1 * u))) + (B2 * (o + (a3 * w))) by A56, A57, Th7;

A60: v1 = (((A2 + B2) * o) + ((A2 * a1) * u)) + ((B2 * a3) * w) by A59, Lm12;

w1 = ((0 * o) + (c3 * u)) + (d3 * v) by A39, Lm13;

then A61: A3 + B3 = 0 by A12, A58, ANPROJ_1:8;

u1 = ((0 * o) + (c1 * v)) + (d1 * w) by A43, Lm13;

then A62: A1 + B1 = 0 by A14, A51, ANPROJ_1:8;

v1 = ((0 * o) + (c2 * u)) + (d2 * w) by A50, Lm13;

then A63: A2 + B2 = 0 by A13, A60, ANPROJ_1:8;

then A64: ( A1 <> 0 & A2 <> 0 & A3 <> 0 ) by A42, A47, A62, A49, A59, A38, A55, A61, Lm14;

set u19 = (a2 * v) - (a3 * w);

set v19 = (a1 * u) - (a3 * w);

set w19 = (a1 * u) - (a2 * v);

B1 = - A1 by A62;

then u1 = A1 * ((a2 * v) - (a3 * w)) by A51, Lm15;

then A65: are_Prop (a2 * v) - (a3 * w),u1 by A64, Lm9;

B3 = - A3 by A61;

then w1 = A3 * ((a1 * u) - (a2 * v)) by A58, Lm15;

then A66: are_Prop (a1 * u) - (a2 * v),w1 by A64, Lm9;

B2 = - A2 by A63;

then v1 = A2 * ((a1 * u) - (a3 * w)) by A60, Lm15;

then A67: are_Prop (a1 * u) - (a3 * w),v1 by A64, Lm9;

((1 * ((a2 * v) - (a3 * w))) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) = (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) by RLVECT_1:def 8

.= (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:def 8

.= (((a2 * v) - (a3 * w)) + (- ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:16

.= (((a2 * v) + (- (a3 * w))) + ((a3 * w) + (- (a1 * u)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:33

.= ((((a2 * v) + (- (a3 * w))) + (a3 * w)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 3

.= (((a2 * v) + ((- (a3 * w)) + (a3 * w))) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 3

.= (((a2 * v) + (0. V)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:5

.= ((a2 * v) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:4

.= (a2 * v) + ((- (a1 * u)) + ((a1 * u) + (- (a2 * v)))) by RLVECT_1:def 3

.= (a2 * v) + (((- (a1 * u)) + (a1 * u)) + (- (a2 * v))) by RLVECT_1:def 3

.= (a2 * v) + ((0. V) + (- (a2 * v))) by RLVECT_1:5

.= (a2 * v) + (- (a2 * v)) by RLVECT_1:4

.= 0. V by RLVECT_1:5 ;

then (a2 * v) - (a3 * w),(a1 * u) - (a3 * w),(a1 * u) - (a2 * v) are_LinDep ;

hence u1,v1,w1 are_LinDep by A65, A67, A66, ANPROJ_1:4; :: thesis: verum

u1,v1,w1 are_LinDep

let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle implies u1,v1,w1 are_LinDep )

assume that

A1: not o is zero and

A2: u,v,w are_Prop_Vect and

A3: u2,v2,w2 are_Prop_Vect and

A4: u1,v1,w1 are_Prop_Vect and

A5: o,u,v,w,u2,v2,w2 are_perspective and

A6: not are_Prop o,u2 and

A7: not are_Prop o,v2 and

A8: not are_Prop o,w2 and

A9: not are_Prop u,u2 and

A10: not are_Prop v,v2 and

A11: not are_Prop w,w2 and

A12: not o,u,v are_LinDep and

A13: not o,u,w are_LinDep and

A14: not o,v,w are_LinDep and

A15: u,v,w,u1,v1,w1 lie_on_a_triangle and

A16: u2,v2,w2,u1,v1,w1 lie_on_a_triangle ; :: thesis: u1,v1,w1 are_LinDep

A17: not w is zero by A2;

A18: ( o,w,w2 are_LinDep & not are_Prop w,o ) by A5, A13, ANPROJ_1:11;

A19: not w2 is zero by A3;

then o,w,w2 are_Prop_Vect by A1, A17;

then consider a3, b3 being Real such that

A20: b3 * w2 = o + (a3 * w) and

a3 <> 0 and

A21: b3 <> 0 by A8, A11, A18, Th6;

A22: not u is zero by A2;

A23: not v is zero by A2;

A24: ( o,v,v2 are_LinDep & not are_Prop o,v ) by A5, A12, ANPROJ_1:11;

A25: ( o,u,u2 are_LinDep & not are_Prop o,u ) by A5, A12, ANPROJ_1:11;

A26: not u2 is zero by A3;

then o,u,u2 are_Prop_Vect by A1, A22;

then consider a1, b1 being Real such that

A27: b1 * u2 = o + (a1 * u) and

A28: a1 <> 0 and

A29: b1 <> 0 by A6, A9, A25, Th6;

A30: not v2 is zero by A3;

then o,v,v2 are_Prop_Vect by A1, A23;

then consider a2, b2 being Real such that

A31: b2 * v2 = o + (a2 * v) and

A32: a2 <> 0 and

A33: b2 <> 0 by A7, A10, A24, Th6;

set u29 = o + (a1 * u);

set v29 = o + (a2 * v);

set w29 = o + (a3 * w);

A34: are_Prop v2,o + (a2 * v) by A31, A33, Lm9;

A35: not o + (a2 * v) is zero by A30, A31, A33, Lm11;

A36: are_Prop w2,o + (a3 * w) by A20, A21, Lm9;

A37: ( u,v,w1 are_LinDep & not are_Prop u,v ) by A12, A15, ANPROJ_1:12;

A38: not w1 is zero by A4;

then u,v,w1 are_Prop_Vect by A22, A23;

then consider c3, d3 being Real such that

A39: w1 = (c3 * u) + (d3 * v) by A37, Th7;

A40: are_Prop u2,o + (a1 * u) by A27, A29, Lm9;

A41: ( v,w,u1 are_LinDep & not are_Prop v,w ) by A14, A15, ANPROJ_1:12;

A42: not u1 is zero by A4;

then v,w,u1 are_Prop_Vect by A23, A17;

then consider c1, d1 being Real such that

A43: u1 = (c1 * v) + (d1 * w) by A41, Th7;

v2,w2,u1 are_LinDep by A16;

then A44: o + (a2 * v),o + (a3 * w),u1 are_LinDep by A34, A36, ANPROJ_1:4;

A45: not are_Prop o + (a2 * v),o + (a3 * w) by A14, A32, Lm10;

A46: not o + (a3 * w) is zero by A19, A20, A21, Lm11;

then o + (a2 * v),o + (a3 * w),u1 are_Prop_Vect by A42, A35;

then consider A1, B1 being Real such that

A47: u1 = (A1 * (o + (a2 * v))) + (B1 * (o + (a3 * w))) by A44, A45, Th7;

A48: ( u,w,v1 are_LinDep & not are_Prop u,w ) by A13, A15, ANPROJ_1:12;

A49: not v1 is zero by A4;

then u,w,v1 are_Prop_Vect by A22, A17;

then consider c2, d2 being Real such that

A50: v1 = (c2 * u) + (d2 * w) by A48, Th7;

A51: u1 = (((A1 + B1) * o) + ((A1 * a2) * v)) + ((B1 * a3) * w) by A47, Lm12;

u2,v2,w1 are_LinDep by A16;

then A52: o + (a1 * u),o + (a2 * v),w1 are_LinDep by A40, A34, ANPROJ_1:4;

A53: not are_Prop o + (a1 * u),o + (a2 * v) by A12, A28, Lm10;

A54: not o + (a1 * u) is zero by A26, A27, A29, Lm11;

then o + (a1 * u),o + (a2 * v),w1 are_Prop_Vect by A38, A35;

then consider A3, B3 being Real such that

A55: w1 = (A3 * (o + (a1 * u))) + (B3 * (o + (a2 * v))) by A52, A53, Th7;

u2,w2,v1 are_LinDep by A16;

then A56: o + (a1 * u),o + (a3 * w),v1 are_LinDep by A40, A36, ANPROJ_1:4;

A57: not are_Prop o + (a1 * u),o + (a3 * w) by A13, A28, Lm10;

A58: w1 = (((A3 + B3) * o) + ((A3 * a1) * u)) + ((B3 * a2) * v) by A55, Lm12;

o + (a1 * u),o + (a3 * w),v1 are_Prop_Vect by A49, A54, A46;

then consider A2, B2 being Real such that

A59: v1 = (A2 * (o + (a1 * u))) + (B2 * (o + (a3 * w))) by A56, A57, Th7;

A60: v1 = (((A2 + B2) * o) + ((A2 * a1) * u)) + ((B2 * a3) * w) by A59, Lm12;

w1 = ((0 * o) + (c3 * u)) + (d3 * v) by A39, Lm13;

then A61: A3 + B3 = 0 by A12, A58, ANPROJ_1:8;

u1 = ((0 * o) + (c1 * v)) + (d1 * w) by A43, Lm13;

then A62: A1 + B1 = 0 by A14, A51, ANPROJ_1:8;

v1 = ((0 * o) + (c2 * u)) + (d2 * w) by A50, Lm13;

then A63: A2 + B2 = 0 by A13, A60, ANPROJ_1:8;

then A64: ( A1 <> 0 & A2 <> 0 & A3 <> 0 ) by A42, A47, A62, A49, A59, A38, A55, A61, Lm14;

set u19 = (a2 * v) - (a3 * w);

set v19 = (a1 * u) - (a3 * w);

set w19 = (a1 * u) - (a2 * v);

B1 = - A1 by A62;

then u1 = A1 * ((a2 * v) - (a3 * w)) by A51, Lm15;

then A65: are_Prop (a2 * v) - (a3 * w),u1 by A64, Lm9;

B3 = - A3 by A61;

then w1 = A3 * ((a1 * u) - (a2 * v)) by A58, Lm15;

then A66: are_Prop (a1 * u) - (a2 * v),w1 by A64, Lm9;

B2 = - A2 by A63;

then v1 = A2 * ((a1 * u) - (a3 * w)) by A60, Lm15;

then A67: are_Prop (a1 * u) - (a3 * w),v1 by A64, Lm9;

((1 * ((a2 * v) - (a3 * w))) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) = (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) by RLVECT_1:def 8

.= (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:def 8

.= (((a2 * v) - (a3 * w)) + (- ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:16

.= (((a2 * v) + (- (a3 * w))) + ((a3 * w) + (- (a1 * u)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:33

.= ((((a2 * v) + (- (a3 * w))) + (a3 * w)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 3

.= (((a2 * v) + ((- (a3 * w)) + (a3 * w))) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 3

.= (((a2 * v) + (0. V)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:5

.= ((a2 * v) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:4

.= (a2 * v) + ((- (a1 * u)) + ((a1 * u) + (- (a2 * v)))) by RLVECT_1:def 3

.= (a2 * v) + (((- (a1 * u)) + (a1 * u)) + (- (a2 * v))) by RLVECT_1:def 3

.= (a2 * v) + ((0. V) + (- (a2 * v))) by RLVECT_1:5

.= (a2 * v) + (- (a2 * v)) by RLVECT_1:4

.= 0. V by RLVECT_1:5 ;

then (a2 * v) - (a3 * w),(a1 * u) - (a3 * w),(a1 * u) - (a2 * v) are_LinDep ;

hence u1,v1,w1 are_LinDep by A65, A67, A66, ANPROJ_1:4; :: thesis: verum