let x be object ; for K being Field
for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let K be Field; for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let V be VectSp of K; for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let u, v be Vector of V; ( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
per cases
( u = v or u <> v )
;
suppose A1:
u = v
;
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )then A2:
{u,v} = {u}
by ENUMSET1:29;
thus
(
x in Lin {u,v} implies ex
a,
b being
Element of
K st
x = (a * u) + (b * v) )
( ex a, b being Element of K st x = (a * u) + (b * v) implies x in Lin {u,v} )given a,
b being
Element of
K such that A4:
x = (a * u) + (b * v)
;
x in Lin {u,v}
x = (a + b) * u
by A1, A4, VECTSP_1:def 15;
hence
x in Lin {u,v}
by A2, VECTSP10:3;
verum end; suppose A5:
u <> v
;
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )thus
(
x in Lin {u,v} implies ex
a,
b being
Element of
K st
x = (a * u) + (b * v) )
( ex a, b being Element of K st x = (a * u) + (b * v) implies x in Lin {u,v} )deffunc H1(
set )
-> Element of the
carrier of
K =
0. K;
given a,
b being
Element of
K such that A7:
x = (a * u) + (b * v)
;
x in Lin {u,v}consider L being
Function of the
carrier of
V, the
carrier of
K such that A8:
(
L . u = a &
L . v = b )
and A9:
for
z being
Element of
V st
z <> u &
z <> v holds
L . z = H1(
z)
from FUNCT_2:sch 7(A5);
reconsider L =
L as
Element of
Funcs ( the
carrier of
V, the
carrier of
K)
by FUNCT_2:8;
then reconsider L =
L as
Linear_Combination of
V by VECTSP_6:def 1;
Carrier L c= {u,v}
then reconsider L =
L as
Linear_Combination of
{u,v} by VECTSP_6:def 4;
Sum L = x
by A5, A7, A8, VECTSP_6:18;
hence
x in Lin {u,v}
by VECTSP_7:7;
verum end;