let V be RealLinearSpace; :: thesis:
let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis:
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:
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: