let V be non trivial RealLinearSpace; ( ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies V is up-3-dimensional )
given y, u, v, w being Element of V such that A1:
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 )
; V is up-3-dimensional
take
y
; ANPROJ_2:def 6 ex v, w1 being Element of V st
for a, b, c being Real st ((a * y) + (b * v)) + (c * w1) = 0. V holds
( a = 0 & b = 0 & c = 0 )
take
u
; ex w1 being Element of V st
for a, b, c being Real st ((a * y) + (b * u)) + (c * w1) = 0. V holds
( a = 0 & b = 0 & c = 0 )
take
v
; for a, b, c being Real st ((a * y) + (b * u)) + (c * v) = 0. V holds
( a = 0 & b = 0 & c = 0 )
let a, b, a1 be Real; ( ((a * y) + (b * u)) + (a1 * v) = 0. V implies ( a = 0 & b = 0 & a1 = 0 ) )
assume
((a * y) + (b * u)) + (a1 * v) = 0. V
; ( a = 0 & b = 0 & a1 = 0 )
then 0. V =
(((a * y) + (b * u)) + (a1 * v)) + (0. V)
by RLVECT_1:4
.=
(((a * y) + (b * u)) + (a1 * v)) + (0 * w)
by RLVECT_1:10
;
hence
( a = 0 & b = 0 & a1 = 0 )
by A1; verum