let R be Skew-Field; :: thesis: for V being LeftMod of R
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) )
let V be LeftMod of R; :: thesis: for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R 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 Scalar of R holds v1 <> a * v2 ) ) )
A1:
0. R <> 1. R
;
thus
( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) )
:: thesis: ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )proof
assume that A2:
v1 <> v2
and A3:
{v1,v2} is
linearly-independent
;
:: thesis: ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) )
thus
v2 <> 0. V
by A1, A3, LMOD_5:5;
:: thesis: for a being Scalar of R holds v1 <> a * v2
let a be
Scalar of
R;
:: thesis: v1 <> a * v2
assume A4:
v1 = a * v2
;
:: thesis: contradiction
deffunc H1(
Element of
V)
-> Element of the
carrier of
R =
0. R;
consider f being
Function of the
carrier of
V,the
carrier of
R such that A5:
(
f . v1 = - (1. R) &
f . v2 = a )
and A6:
for
v being
Element of
V st
v <> v1 &
v <> v2 holds
f . v = H1(
v)
from FUNCT_2:sch 7(A2);
reconsider f =
f as
Element of
Funcs the
carrier of
V,the
carrier of
R 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. R)) * (a * v2)) + (a * v2)
by A2, A4, A5, VECTSP_6:44
.=
(- (a * v2)) + (a * v2)
by VECTSP_1:59
.=
0. V
by RLVECT_1:16
;
hence
contradiction
by A3, A8, LMOD_5:def 1;
:: thesis: verum
end;
assume A9:
v2 <> 0. V
; :: thesis: ( ex a being Scalar of R st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A10:
for a being Scalar of R holds v1 <> a * v2
; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
then A11:
( v1 <> (1. R) * v2 & (1. R) * 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 LMOD_5:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A12:
Sum l = 0. V
and
A13:
Carrier l <> {}
; :: thesis: contradiction
consider x being Element of Carrier l;
x in Carrier l
by A13;
then A14:
ex u being Vector of V st
( x = u & l . u <> 0. R )
;
Carrier l c= {v1,v2}
by VECTSP_6:def 7;
then A15:
x in {v1,v2}
by A13, TARSKI:def 3;
A16:
0. V = ((l . v1) * v1) + ((l . v2) * v2)
by A11, A12, VECTSP_6:44;
hence
contradiction
; :: thesis: verum