let GF be Field; :: thesis: for V being VectSp of GF
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
let V be VectSp of GF; :: thesis: for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
let v1, v2 be Vector of V; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
thus
( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
:: thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )proof
assume that A1:
v1 <> v2
and A2:
{v1,v2} is
linearly-independent
;
:: thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) )
thus
v2 <> 0. V
by A2, Th6;
:: thesis: for a being Element of GF holds v1 <> a * v2
let a be
Element of
GF;
:: thesis: v1 <> a * v2
assume A3:
v1 = a * v2
;
:: thesis: contradiction
deffunc H1(
set )
-> Element of the
carrier of
GF =
0. GF;
consider f being
Function of the
carrier of
V,the
carrier of
GF such that A4:
(
f . v1 = - (1_ GF) &
f . v2 = a )
and A5:
for
v being
Element of
V st
v <> v1 &
v <> v2 holds
f . v = H1(
v)
from FUNCT_2:sch 7(A1);
reconsider f =
f as
Element of
Funcs the
carrier of
V,the
carrier of
GF by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by VECTSP_6:def 4;
Carrier f c= {v1,v2}
then reconsider f =
f as
Linear_Combination of
{v1,v2} by VECTSP_6:def 7;
set w =
a * v2;
Sum f =
((- (1_ GF)) * (a * v2)) + (a * v2)
by A1, A3, A4, VECTSP_6:44
.=
(- (a * v2)) + (a * v2)
by VECTSP_1:59
.=
- ((a * v2) - (a * v2))
by VECTSP_1:64
.=
- (0. V)
by VECTSP_1:66
.=
0. V
by RLVECT_1:25
;
hence
contradiction
by A2, A7, Def1;
:: thesis: verum
end;
assume A8:
v2 <> 0. V
; :: thesis: ( ex a being Element of GF st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A9:
for a being Element of GF holds v1 <> a * v2
; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
then A10:
( v1 <> (1_ GF) * v2 & (1_ GF) * v2 = v2 )
by VECTSP_1:def 26;
hence
v1 <> v2
; :: thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A11:
Sum l = 0. V
and
A12:
Carrier l <> {}
; :: thesis: contradiction
consider x being Element of Carrier l;
x in Carrier l
by A12;
then A13:
ex u being Vector of V st
( x = u & l . u <> 0. GF )
;
Carrier l c= {v1,v2}
by VECTSP_6:def 7;
then A14:
x in {v1,v2}
by A12, TARSKI:def 3;
A15:
0. V = ((l . v1) * v1) + ((l . v2) * v2)
by A10, A11, VECTSP_6:44;
hence
contradiction
; :: thesis: verum