let V be RealLinearSpace; :: thesis: for o, u, v, w, u2, v2, w2, u1, v1, w1 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 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds
u1,v1,w1 are_LinDep
let o, u, v, w, u2, v2, w2, u1, v1, w1 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 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep )
assume that
A1:
( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect )
and
A2:
o,u,v,w,u2,v2,w2 lie_on_an_angle
and
A3:
o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop
and
A4:
( u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep )
; :: thesis: u1,v1,w1 are_LinDep
A5:
( not o is zero & not u is zero & not v is zero & not w is zero & not u2 is zero & not v2 is zero & not w2 is zero & not u1 is zero & not v1 is zero & not w1 is zero )
by A1, Def1;
A6:
( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep )
by A2, Def4;
A7:
( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 )
by A3, Def5;
A8:
( not are_Prop o,u & not are_Prop u,u2 & not are_Prop u2,o )
by A6, ANPROJ_1:17;
A9:
( o,u,v are_Prop_Vect & o,u,w are_Prop_Vect & o,u2,v2 are_Prop_Vect & o,u2,w2 are_Prop_Vect )
by A5, Def1;
then consider a2, b2 being Real such that
A10:
( b2 * v = o + (a2 * u) & a2 <> 0 & b2 <> 0 )
by A6, A7, A8, Th6;
consider a3, b3 being Real such that
A11:
( b3 * w = o + (a3 * u) & a3 <> 0 & b3 <> 0 )
by A6, A7, A8, A9, Th6;
consider c2, d2 being Real such that
A12:
( d2 * v2 = o + (c2 * u2) & c2 <> 0 & d2 <> 0 )
by A6, A7, A8, A9, Th6;
consider c3, d3 being Real such that
A13:
( d3 * w2 = o + (c3 * u2) & c3 <> 0 & d3 <> 0 )
by A6, A7, A8, A9, Th6;
set v' = o + (a2 * u);
set w' = o + (a3 * u);
set v2' = o + (c2 * u2);
set w2' = o + (c3 * u2);
A14:
( are_Prop v,o + (a2 * u) & are_Prop w,o + (a3 * u) & are_Prop v2,o + (c2 * u2) & are_Prop w2,o + (c3 * u2) )
by A10, A11, A12, A13, Lm16;
A15:
( not are_Prop o + (a2 * u),o + (a3 * u) & not are_Prop o + (c2 * u2),o + (c3 * u2) )
A18:
not are_Prop u,v2
A19:
not are_Prop u2,v
by A6, ANPROJ_1:9;
A20:
not are_Prop u,w2
A21:
not are_Prop u2,w
by A6, ANPROJ_1:9;
not o,u2,v are_LinDep
proof
assume
o,
u2,
v are_LinDep
;
:: thesis: contradiction
then A22:
o,
v,
u2 are_LinDep
by ANPROJ_1:10;
A23:
o,
v,
u are_LinDep
by A6, ANPROJ_1:10;
o,
v,
o are_LinDep
by ANPROJ_1:16;
hence
contradiction
by A5, A6, A7, A22, A23, ANPROJ_1:19;
:: thesis: verum
end;
then A24:
not are_Prop v,w2
by A6, ANPROJ_1:9;
not o,u,v2 are_LinDep
proof
assume
o,
u,
v2 are_LinDep
;
:: thesis: contradiction
then A25:
o,
v2,
u are_LinDep
by ANPROJ_1:10;
A26:
o,
v2,
u2 are_LinDep
by A6, ANPROJ_1:10;
o,
v2,
o are_LinDep
by ANPROJ_1:16;
hence
contradiction
by A5, A6, A7, A25, A26, ANPROJ_1:19;
:: thesis: verum
end;
then A27:
not are_Prop v2,w
by A6, ANPROJ_1:9;
A28:
( u,o + (c2 * u2),w1 are_LinDep & u2,o + (a2 * u),w1 are_LinDep )
by A4, A14, ANPROJ_1:9;
A29:
u2,w,v1 are_LinDep
by A4, ANPROJ_1:10;
A30:
( not o + (c2 * u2) is zero & not o + (a2 * u) is zero & not o + (c3 * u2) is zero & not o + (a3 * u) is zero )
by A5, A10, A11, A12, A13, Lm20;
A31:
not are_Prop u,o + (c2 * u2)
by A12, A18, Lm17;
A32:
not are_Prop u2,o + (a2 * u)
by A10, A19, Lm17;
A33:
u,o + (c3 * u2),v1 are_LinDep
by A4, A14, ANPROJ_1:9;
A34:
u2,o + (a3 * u),v1 are_LinDep
by A14, A29, ANPROJ_1:9;
A35:
not are_Prop u,o + (c3 * u2)
by A13, A20, Lm17;
A36:
not are_Prop u2,o + (a3 * u)
by A11, A21, Lm17;
consider A3, B3 being Real such that
A37:
w1 = (A3 * u) + (B3 * (o + (c2 * u2)))
by A5, A28, A30, A31, ANPROJ_1:11;
consider A3', B3' being Real such that
A38:
w1 = (A3' * u2) + (B3' * (o + (a2 * u)))
by A5, A28, A30, A32, ANPROJ_1:11;
A39:
w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2)
by A37, Lm18;
w1 = ((B3' * o) + ((B3' * a2) * u)) + (A3' * u2)
by A38, Lm19;
then A40:
( B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' )
by A6, A39, ANPROJ_1:13;
set w1' = (o + (a2 * u)) + (c2 * u2);
A41:
B3 <> 0
w1 = B3 * ((o + (a2 * u)) + (c2 * u2))
by A39, A40, Lm29;
then A42:
are_Prop (o + (a2 * u)) + (c2 * u2),w1
by A41, Lm16;
consider A2, B2 being Real such that
A43:
v1 = (A2 * u) + (B2 * (o + (c3 * u2)))
by A5, A30, A33, A35, ANPROJ_1:11;
consider A2', B2' being Real such that
A44:
v1 = (A2' * u2) + (B2' * (o + (a3 * u)))
by A5, A30, A34, A36, ANPROJ_1:11;
A45:
v1 = ((B2 * o) + (A2 * u)) + ((B2 * c3) * u2)
by A43, Lm18;
v1 = ((B2' * o) + ((B2' * a3) * u)) + (A2' * u2)
by A44, Lm19;
then A46:
( B2 = B2' & A2 = B2' * a3 & B2 * c3 = A2' )
by A6, A45, ANPROJ_1:13;
set v1' = (o + (a3 * u)) + (c3 * u2);
A47:
B2 <> 0
v1 = B2 * ((o + (a3 * u)) + (c3 * u2))
by A45, A46, Lm29;
then A48:
are_Prop (o + (a3 * u)) + (c3 * u2),v1
by A47, Lm16;
A49:
not are_Prop o + (a2 * u),o + (c3 * u2)
by A10, A13, A24, Lm21;
A50:
not are_Prop o + (a3 * u),o + (c2 * u2)
by A11, A12, A27, Lm21;
A51:
( o + (a2 * u),o + (c3 * u2),u1 are_LinDep & o + (a3 * u),o + (c2 * u2),u1 are_LinDep )
by A4, A14, ANPROJ_1:9;
then consider A1, B1 being Real such that
A52:
u1 = (A1 * (o + (a2 * u))) + (B1 * (o + (c3 * u2)))
by A30, A49, ANPROJ_1:11;
consider A1', B1' being Real such that
A53:
u1 = (A1' * (o + (a3 * u))) + (B1' * (o + (c2 * u2)))
by A30, A50, A51, ANPROJ_1:11;
A54:
u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2)
by A52, Lm22;
u1 = (((A1' + B1') * o) + ((A1' * a3) * u)) + ((B1' * c2) * u2)
by A53, Lm22;
then
( A1 + B1 = A1' + B1' & A1 * a2 = A1' * a3 & B1 * c3 = B1' * c2 )
by A6, A54, ANPROJ_1:13;
then A55:
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1
by A12, A15, Lm24;
then A56:
u1 = (B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
by A12, A15, A54, Lm26;
set u1' = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2);
B1 <> 0
then A57:
are_Prop ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),u1
by A12, A15, A56, Lm16, Lm25;
set C2 = a2 * c2;
set C3 = - (a3 * c3);
( (a2 * c2) + (- (a3 * c3)) = (a2 * c2) - (a3 * c3) & ((a2 * c2) * a3) + ((- (a3 * c3)) * a2) = (a2 * a3) * (c2 - c3) & ((a2 * c2) * c3) + ((- (a3 * c3)) * c2) = (c2 * c3) * (a2 - a3) )
;
then
((1 * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) + ((a2 * c2) * ((o + (a3 * u)) + (c3 * u2)))) + ((- (a3 * c3)) * ((o + (a2 * u)) + (c2 * u2))) = 0. V
by Lm28;
then
((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),(o + (a3 * u)) + (c3 * u2),(o + (a2 * u)) + (c2 * u2) are_LinDep
by ANPROJ_1:def 3;
hence
u1,v1,w1 are_LinDep
by A42, A48, A57, ANPROJ_1:9; :: thesis: verum