let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st not v is zero & not w is zero & not are_Prop v,w holds

( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

let u, v, w be Element of V; :: thesis: ( not v is zero & not w is zero & not are_Prop v,w implies ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) )

assume that

A1: not v is zero and

A2: not w is zero and

A3: not are_Prop v,w ; :: thesis: ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

A4: w <> 0. V by A2;

A5: v <> 0. V by A1;

A6: ( v,w,u are_LinDep implies ex a, b being Real st u = (a * v) + (b * w) )

( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

let u, v, w be Element of V; :: thesis: ( not v is zero & not w is zero & not are_Prop v,w implies ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) ) )

assume that

A1: not v is zero and

A2: not w is zero and

A3: not are_Prop v,w ; :: thesis: ( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

A4: w <> 0. V by A2;

A5: v <> 0. V by A1;

A6: ( v,w,u are_LinDep implies ex a, b being Real st u = (a * v) + (b * w) )

proof

( ex a, b being Real st u = (a * v) + (b * w) implies v,w,u are_LinDep )
assume
v,w,u are_LinDep
; :: thesis: ex a, b being Real st u = (a * v) + (b * w)

then u,v,w are_LinDep by Th5;

then consider a, b, c being Real such that

A7: ((a * u) + (b * v)) + (c * w) = 0. V and

A8: ( a <> 0 or b <> 0 or c <> 0 ) ;

a <> 0

hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum

end;then u,v,w are_LinDep by Th5;

then consider a, b, c being Real such that

A7: ((a * u) + (b * v)) + (c * w) = 0. V and

A8: ( a <> 0 or b <> 0 or c <> 0 ) ;

a <> 0

proof

then
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
by A7, Lm2;
assume A9:
a = 0
; :: thesis: contradiction

then A10: 0. V = ((0. V) + (b * v)) + (c * w) by A7, RLVECT_1:10

.= (b * v) + (c * w) ;

A11: b <> 0

then ( b = 0 or - c = 0 ) by A3;

hence contradiction by A11, A13; :: thesis: verum

end;then A10: 0. V = ((0. V) + (b * v)) + (c * w) by A7, RLVECT_1:10

.= (b * v) + (c * w) ;

A11: b <> 0

proof

A13:
c <> 0
assume A12:
b = 0
; :: thesis: contradiction

then 0. V = (0. V) + (c * w) by A10, RLVECT_1:10

.= c * w ;

hence contradiction by A4, A8, A9, A12, RLVECT_1:11; :: thesis: verum

end;then 0. V = (0. V) + (c * w) by A10, RLVECT_1:10

.= c * w ;

hence contradiction by A4, A8, A9, A12, RLVECT_1:11; :: thesis: verum

proof

b * v = (- c) * w
by A10, Lm1;
assume A14:
c = 0
; :: thesis: contradiction

then 0. V = (b * v) + (0. V) by A10, RLVECT_1:10

.= b * v ;

hence contradiction by A5, A8, A9, A14, RLVECT_1:11; :: thesis: verum

end;then 0. V = (b * v) + (0. V) by A10, RLVECT_1:10

.= b * v ;

hence contradiction by A5, A8, A9, A14, RLVECT_1:11; :: thesis: verum

then ( b = 0 or - c = 0 ) by A3;

hence contradiction by A11, A13; :: thesis: verum

hence ex a, b being Real st u = (a * v) + (b * w) ; :: thesis: verum

proof

hence
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )
by A6; :: thesis: verum
given a, b being Real such that A15:
u = (a * v) + (b * w)
; :: thesis: v,w,u are_LinDep

0. V = ((a * v) + (b * w)) + (- u) by A15, RLVECT_1:5

.= ((a * v) + (b * w)) + ((- 1) * u) by RLVECT_1:16 ;

hence v,w,u are_LinDep ; :: thesis: verum

end;0. V = ((a * v) + (b * w)) + (- u) by A15, RLVECT_1:5

.= ((a * v) + (b * w)) + ((- 1) * u) by RLVECT_1:16 ;

hence v,w,u are_LinDep ; :: thesis: verum