let V be RealLinearSpace; 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; ( 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
; 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; verum