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 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, 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 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
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 lie_on_an_angle
and
A6:
o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop
and
A7:
u,v2,w1 are_LinDep
and
A8:
u2,v,w1 are_LinDep
and
A9:
u,w2,v1 are_LinDep
and
A10:
w,u2,v1 are_LinDep
and
A11:
v,w2,u1 are_LinDep
and
A12:
w,v2,u1 are_LinDep
; u1,v1,w1 are_LinDep
A13:
not u is zero
by A2;
A14:
not are_Prop u2,v2
by A6;
A15:
not are_Prop o,v
by A6;
A16:
not are_Prop u,v
by A6;
A17:
o,u2,v2 are_LinDep
by A5;
A18:
( not are_Prop o,w2 & not are_Prop u2,w2 )
by A6;
A19:
not u2 is zero
by A3;
A20:
( not are_Prop o,w & not are_Prop u,w )
by A6;
A21:
o,u,w are_LinDep
by A5;
A22:
not are_Prop o,v2
by A6;
A23:
o,u2,w2 are_LinDep
by A5;
A24:
not o,u,u2 are_LinDep
by A5;
then A25:
not are_Prop o,u
by ANPROJ_1:12;
A26:
not w is zero
by A2;
then
o,u,w are_Prop_Vect
by A1, A13;
then consider a3, b3 being Real such that
A27:
b3 * w = o + (a3 * u)
and
a3 <> 0
and
A28:
b3 <> 0
by A21, A20, A25, Th6;
A29:
not are_Prop u2,o
by A24, ANPROJ_1:12;
A30:
not w2 is zero
by A3;
then
o,u2,w2 are_Prop_Vect
by A1, A19;
then consider c3, d3 being Real such that
A31:
d3 * w2 = o + (c3 * u2)
and
c3 <> 0
and
A32:
d3 <> 0
by A23, A18, A29, Th6;
A33:
o,u,v are_LinDep
by A5;
A34:
not v2 is zero
by A3;
then
o,u2,v2 are_Prop_Vect
by A1, A19;
then consider c2, d2 being Real such that
A35:
d2 * v2 = o + (c2 * u2)
and
A36:
c2 <> 0
and
A37:
d2 <> 0
by A17, A22, A14, A29, Th6;
A38:
not v is zero
by A2;
then
o,u,v are_Prop_Vect
by A1, A13;
then consider a2, b2 being Real such that
A39:
b2 * v = o + (a2 * u)
and
a2 <> 0
and
A40:
b2 <> 0
by A33, A15, A16, A25, Th6;
set v9 = o + (a2 * u);
set w9 = o + (a3 * u);
set v29 = o + (c2 * u2);
set w29 = o + (c3 * u2);
A41:
not o + (c2 * u2) is zero
by A34, A35, A37, Lm20;
A42:
not o + (a2 * u) is zero
by A38, A39, A40, Lm20;
A43:
not o + (a3 * u) is zero
by A26, A27, A28, Lm20;
A44:
not o + (c3 * u2) is zero
by A30, A31, A32, Lm20;
A45:
are_Prop w2,o + (c3 * u2)
by A31, A32, Lm16;
then A46:
u,o + (c3 * u2),v1 are_LinDep
by A9, ANPROJ_1:4;
A47:
are_Prop v,o + (a2 * u)
by A39, A40, Lm16;
then A48:
o + (a2 * u),o + (c3 * u2),u1 are_LinDep
by A11, A45, ANPROJ_1:4;
A49:
are_Prop v2,o + (c2 * u2)
by A35, A37, Lm16;
then A50:
u,o + (c2 * u2),w1 are_LinDep
by A7, ANPROJ_1:4;
A51:
are_Prop w,o + (a3 * u)
by A27, A28, Lm16;
then A52:
o + (a3 * u),o + (c2 * u2),u1 are_LinDep
by A12, A49, ANPROJ_1:4;
not are_Prop u,v2
then
not are_Prop u,o + (c2 * u2)
by A35, A37, Lm17;
then consider A3, B3 being Real such that
A53:
w1 = (A3 * u) + (B3 * (o + (c2 * u2)))
by A13, A50, A41, ANPROJ_1:6;
not o,u2,v are_LinDep
proof
assume
o,
u2,
v are_LinDep
;
contradiction
then A54:
o,
v,
u2 are_LinDep
by ANPROJ_1:5;
(
o,
v,
u are_LinDep &
o,
v,
o are_LinDep )
by A33, ANPROJ_1:5, ANPROJ_1:11;
hence
contradiction
by A1, A38, A24, A15, A54, ANPROJ_1:14;
verum
end;
then
not are_Prop v,w2
by A23, ANPROJ_1:4;
then
not are_Prop o + (a2 * u),o + (c3 * u2)
by A39, A40, A31, A32, Lm21;
then consider A1, B1 being Real such that
A55:
u1 = (A1 * (o + (a2 * u))) + (B1 * (o + (c3 * u2)))
by A42, A44, A48, ANPROJ_1:6;
not o,u,v2 are_LinDep
proof
assume
o,
u,
v2 are_LinDep
;
contradiction
then A56:
o,
v2,
u are_LinDep
by ANPROJ_1:5;
(
o,
v2,
u2 are_LinDep &
o,
v2,
o are_LinDep )
by A17, ANPROJ_1:5, ANPROJ_1:11;
hence
contradiction
by A1, A34, A24, A22, A56, ANPROJ_1:14;
verum
end;
then
not are_Prop v2,w
by A21, ANPROJ_1:4;
then
not are_Prop o + (a3 * u),o + (c2 * u2)
by A27, A28, A35, A37, Lm21;
then consider A19, B19 being Real such that
A57:
u1 = (A19 * (o + (a3 * u))) + (B19 * (o + (c2 * u2)))
by A41, A43, A52, ANPROJ_1:6;
A58:
u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2)
by A55, Lm22;
A59:
not are_Prop v2,w2
by A6;
A60:
not are_Prop v,w
by A6;
A61:
( not are_Prop o + (a2 * u),o + (a3 * u) & not are_Prop o + (c2 * u2),o + (c3 * u2) )
not are_Prop u,w2
then
not are_Prop u,o + (c3 * u2)
by A31, A32, Lm17;
then consider A2, B2 being Real such that
A64:
v1 = (A2 * u) + (B2 * (o + (c3 * u2)))
by A13, A44, A46, ANPROJ_1:6;
u2,w,v1 are_LinDep
by A10;
then A65:
u2,o + (a3 * u),v1 are_LinDep
by A51, ANPROJ_1:4;
not are_Prop u2,w
by A24, A21, ANPROJ_1:4;
then
not are_Prop u2,o + (a3 * u)
by A27, A28, Lm17;
then consider A29, B29 being Real such that
A66:
v1 = (A29 * u2) + (B29 * (o + (a3 * u)))
by A19, A43, A65, ANPROJ_1:6;
A67:
v1 = ((B2 * o) + (A2 * u)) + ((B2 * c3) * u2)
by A64, Lm18;
A68:
u2,o + (a2 * u),w1 are_LinDep
by A8, A47, ANPROJ_1:4;
not are_Prop u2,v
by A24, A33, ANPROJ_1:4;
then
not are_Prop u2,o + (a2 * u)
by A39, A40, Lm17;
then consider A39, B39 being Real such that
A69:
w1 = (A39 * u2) + (B39 * (o + (a2 * u)))
by A19, A68, A42, ANPROJ_1:6;
A70:
w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2)
by A53, Lm18;
v1 = ((B29 * o) + ((B29 * a3) * u)) + (A29 * u2)
by A66, Lm19;
then A71:
( B2 = B29 & A2 = B29 * a3 )
by A24, A67, ANPROJ_1:8;
w1 = ((B39 * o) + ((B39 * a2) * u)) + (A39 * u2)
by A69, Lm19;
then A72:
( B3 = B39 & A3 = B39 * a2 )
by A24, A70, ANPROJ_1:8;
A73:
u1 = (((A19 + B19) * o) + ((A19 * a3) * u)) + ((B19 * c2) * u2)
by A57, Lm22;
then A74:
B1 * c3 = B19 * c2
by A24, A58, ANPROJ_1:8;
( A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 )
by A24, A58, A73, ANPROJ_1:8;
then A75:
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1
by A36, A61, A74, Lm24;
set v19 = (o + (a3 * u)) + (c3 * u2);
set C2 = a2 * c2;
set C3 = - (a3 * c3);
set u19 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2);
set w19 = (o + (a2 * u)) + (c2 * u2);
A76:
((a2 * c2) * c3) + ((- (a3 * c3)) * c2) = (c2 * c3) * (a2 - a3)
;
( (a2 * c2) + (- (a3 * c3)) = (a2 * c2) - (a3 * c3) & ((a2 * c2) * a3) + ((- (a3 * c3)) * a2) = (a2 * a3) * (c2 - c3) )
;
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 A76, Lm28;
then A77:
((((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
;
A78:
not v1 is zero
by A4;
A79:
B2 <> 0
v1 = B2 * ((o + (a3 * u)) + (c3 * u2))
by A67, A71, Lm29;
then A80:
are_Prop (o + (a3 * u)) + (c3 * u2),v1
by A79, Lm16;
A81:
not w1 is zero
by A4;
A82:
B3 <> 0
w1 = B3 * ((o + (a2 * u)) + (c2 * u2))
by A70, A72, Lm29;
then A83:
are_Prop (o + (a2 * u)) + (c2 * u2),w1
by A82, Lm16;
A84:
not u1 is zero
by A4;
A85:
B1 <> 0
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
by A36, A61, A58, A75, Lm26;
then
are_Prop ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),u1
by A36, A61, A85, Lm16, Lm25;
hence
u1,v1,w1 are_LinDep
by A83, A80, A77, ANPROJ_1:4; verum