let V be RealLinearSpace; for p, q, r, u, v, w, y being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds
v,w,y are_LinDep
let p, q, r, u, v, w, y be Element of V; ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep implies v,w,y are_LinDep )
assume that
A1:
u,v,q are_LinDep
and
A2:
w,y,q are_LinDep
and
A3:
u,w,p are_LinDep
and
A4:
v,y,p are_LinDep
and
A5:
u,y,r are_LinDep
and
A6:
v,w,r are_LinDep
and
A7:
p,q,r are_LinDep
and
A8:
not p is zero
and
A9:
not q is zero
and
A10:
not r is zero
; ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )
assume A11:
( not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep & not v,w,y are_LinDep )
; contradiction
then A12:
not v is zero
by Th12;
A13:
not w is zero
by A11, Th12;
A14:
not y is zero
by A11, Th12;
A15:
not u is zero
by A11, Th12;
not are_Prop v,y
by A11, Th12;
then consider a19, b19 being Real such that
A16:
p = (a19 * v) + (b19 * y)
by A4, A12, A14, Th6;
not are_Prop u,v
by A11, Th12;
then consider a2, b2 being Real such that
A17:
q = (a2 * u) + (b2 * v)
by A1, A15, A12, Th6;
not are_Prop v,w
by A11, Th12;
then consider a39, b39 being Real such that
A18:
r = (a39 * v) + (b39 * w)
by A6, A12, A13, Th6;
not are_Prop u,w
by A11, Th12;
then consider a1, b1 being Real such that
A19:
p = (a1 * u) + (b1 * w)
by A3, A15, A13, Th6;
not are_Prop w,y
by A11, Th12;
then consider a29, b29 being Real such that
A20:
q = (a29 * w) + (b29 * y)
by A2, A13, A14, Th6;
not are_Prop y,u
by A11, Th12;
then consider a3, b3 being Real such that
A21:
r = (a3 * u) + (b3 * y)
by A5, A15, A14, Th6;
consider A, B, C being Real such that
A22:
((A * p) + (B * q)) + (C * r) = 0. V
and
A23:
( A <> 0 or B <> 0 or C <> 0 )
by A7;
A24:
0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y)
by A19, A20, A21, A22, Lm9;
then A25:
(A * a1) + (C * a3) = 0
by A11;
A26: 0. V =
((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y)))
by A16, A20, A18, A22, RLVECT_1:def 3
.=
((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y)
by Lm9
;
then A27:
(C * a39) + (A * a19) = 0
by A11;
A28:
0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y)
by A16, A17, A21, A22, Lm9;
then A29:
(B * a2) + (C * a3) = 0
by A11;
A30:
0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w)
by A19, A17, A18, A22, Lm9;
then A31:
(B * a2) + (A * a1) = 0
by A11;
A32:
(C * b39) + (B * a29) = 0
by A11, A26;
A33:
(C * b39) + (A * b1) = 0
by A11, A30;
A34:
(B * b29) + (A * b19) = 0
by A11, A26;
A35:
(A * b19) + (C * b3) = 0
by A11, A28;
A36:
(B * b29) + (C * b3) = 0
by A11, A24;
A39:
(B * b2) + (C * a39) = 0
by A11, A30;
A40:
(B * b2) + (A * a19) = 0
by A11, A28;
A43:
(A * b1) + (B * a29) = 0
by A11, A24;
hence
contradiction
by A23, A41, A37; verum