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