let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V holds

( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

let v1, v2 be VECTOR of V; :: thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

thus ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) ) :: thesis: ( ( for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

( a = 0 & b = 0 ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

let v1, v2 be VECTOR of V; :: thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) )

thus ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) ) :: thesis: ( ( for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

assume A6:
for a, b being Real st (a * v1) + (b * v2) = 0. V holds
assume A1:
( v1 <> v2 & {v1,v2} is linearly-independent )
; :: thesis: for a, b being Real st (a * v1) + (b * v2) = 0. V holds

( a = 0 & b = 0 )

let a, b be Real; :: thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0 & b = 0 ) )

assume that

A2: (a * v1) + (b * v2) = 0. V and

A3: ( a <> 0 or b <> 0 ) ; :: thesis: contradiction

end;( a = 0 & b = 0 )

let a, b be Real; :: thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0 & b = 0 ) )

assume that

A2: (a * v1) + (b * v2) = 0. V and

A3: ( a <> 0 or b <> 0 ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( a <> 0 or b <> 0 )
by A3;

end;

suppose A4:
a <> 0
; :: thesis: contradiction

0. V =
(a ") * ((a * v1) + (b * v2))
by A2

.= ((a ") * (a * v1)) + ((a ") * (b * v2)) by RLVECT_1:def 5

.= (((a ") * a) * v1) + ((a ") * (b * v2)) by RLVECT_1:def 7

.= (((a ") * a) * v1) + (((a ") * b) * v2) by RLVECT_1:def 7

.= (1 * v1) + (((a ") * b) * v2) by A4, XCMPLX_0:def 7

.= v1 + (((a ") * b) * v2) by RLVECT_1:def 8 ;

then v1 = - (((a ") * b) * v2) by RLVECT_1:6

.= (- 1) * (((a ") * b) * v2) by RLVECT_1:16

.= ((- 1) * ((a ") * b)) * v2 by RLVECT_1:def 7 ;

hence contradiction by A1, Th12; :: thesis: verum

end;.= ((a ") * (a * v1)) + ((a ") * (b * v2)) by RLVECT_1:def 5

.= (((a ") * a) * v1) + ((a ") * (b * v2)) by RLVECT_1:def 7

.= (((a ") * a) * v1) + (((a ") * b) * v2) by RLVECT_1:def 7

.= (1 * v1) + (((a ") * b) * v2) by A4, XCMPLX_0:def 7

.= v1 + (((a ") * b) * v2) by RLVECT_1:def 8 ;

then v1 = - (((a ") * b) * v2) by RLVECT_1:6

.= (- 1) * (((a ") * b) * v2) by RLVECT_1:16

.= ((- 1) * ((a ") * b)) * v2 by RLVECT_1:def 7 ;

hence contradiction by A1, Th12; :: thesis: verum

suppose A5:
b <> 0
; :: thesis: contradiction

0. V =
(b ") * ((a * v1) + (b * v2))
by A2

.= ((b ") * (a * v1)) + ((b ") * (b * v2)) by RLVECT_1:def 5

.= (((b ") * a) * v1) + ((b ") * (b * v2)) by RLVECT_1:def 7

.= (((b ") * a) * v1) + (((b ") * b) * v2) by RLVECT_1:def 7

.= (((b ") * a) * v1) + (1 * v2) by A5, XCMPLX_0:def 7

.= (((b ") * a) * v1) + v2 by RLVECT_1:def 8 ;

then v2 = - (((b ") * a) * v1) by RLVECT_1:def 10

.= (- 1) * (((b ") * a) * v1) by RLVECT_1:16

.= ((- 1) * ((b ") * a)) * v1 by RLVECT_1:def 7 ;

hence contradiction by A1, Th12; :: thesis: verum

end;.= ((b ") * (a * v1)) + ((b ") * (b * v2)) by RLVECT_1:def 5

.= (((b ") * a) * v1) + ((b ") * (b * v2)) by RLVECT_1:def 7

.= (((b ") * a) * v1) + (((b ") * b) * v2) by RLVECT_1:def 7

.= (((b ") * a) * v1) + (1 * v2) by A5, XCMPLX_0:def 7

.= (((b ") * a) * v1) + v2 by RLVECT_1:def 8 ;

then v2 = - (((b ") * a) * v1) by RLVECT_1:def 10

.= (- 1) * (((b ") * a) * v1) by RLVECT_1:16

.= ((- 1) * ((b ") * a)) * v1 by RLVECT_1:def 7 ;

hence contradiction by A1, Th12; :: thesis: verum

( a = 0 & b = 0 ) ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )

A7: now :: thesis: for a being Real holds not v1 = a * v2

let a be Real; :: thesis: not v1 = a * v2

assume v1 = a * v2 ; :: thesis: contradiction

then v1 = (0. V) + (a * v2) ;

then 0. V = v1 - (a * v2) by RLSUB_2:61

.= v1 + (- (a * v2)) by RLVECT_1:def 11

.= v1 + (a * (- v2)) by RLVECT_1:25

.= v1 + ((- a) * v2) by RLVECT_1:24

.= (1 * v1) + ((- a) * v2) by RLVECT_1:def 8 ;

hence contradiction by A6; :: thesis: verum

end;assume v1 = a * v2 ; :: thesis: contradiction

then v1 = (0. V) + (a * v2) ;

then 0. V = v1 - (a * v2) by RLSUB_2:61

.= v1 + (- (a * v2)) by RLVECT_1:def 11

.= v1 + (a * (- v2)) by RLVECT_1:25

.= v1 + ((- a) * v2) by RLVECT_1:24

.= (1 * v1) + ((- a) * v2) by RLVECT_1:def 8 ;

hence contradiction by A6; :: thesis: verum

now :: thesis: not v2 = 0. V

hence
( v1 <> v2 & {v1,v2} is linearly-independent )
by A7, Th12; :: thesis: verumassume A8:
v2 = 0. V
; :: thesis: contradiction

0. V = (0. V) + (0. V)

.= (0 * v1) + (0. V) by RLVECT_1:10

.= (0 * v1) + (1 * v2) by A8 ;

hence contradiction by A6; :: thesis: verum

end;0. V = (0. V) + (0. V)

.= (0 * v1) + (0. V) by RLVECT_1:10

.= (0 * v1) + (1 * v2) by A8 ;

hence contradiction by A6; :: thesis: verum