let K be Field; for V being VectSp of K
for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let V be VectSp of K; for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let X be Subspace of V; for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let fi be linear-Functional of X; for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let v be Vector of V; for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let y be Vector of (X + (Lin {v})); ( v = y & not v in X implies for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r ) )
assume that
A1:
v = y
and
A2:
not v in X
; for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
reconsider W1 = X as Subspace of X + (Lin {v}) by VECTSP_5:11;
let r be Element of K; ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
defpred S1[ Element of (X + (Lin {v})), Element of K] means for x being Vector of X
for s being Element of K st ($1 |-- W1,(Lin {y})) `1 = x & ($1 |-- W1,(Lin {y})) `2 = s * v holds
$2 = (fi . x) + (s * r);
A3:
for e being Element of (X + (Lin {v})) ex a being Element of K st S1[e,a]
proof
let e be
Element of
(X + (Lin {v}));
ex a being Element of K st S1[e,a]
consider x being
Vector of
X,
s being
Element of
K such that A4:
e |-- W1,
(Lin {y}) = [x,(s * v)]
by A1, A2, Th19;
take u =
(fi . x) + (s * r);
S1[e,u]
let x9 be
Vector of
X;
for s being Element of K st (e |-- W1,(Lin {y})) `1 = x9 & (e |-- W1,(Lin {y})) `2 = s * v holds
u = (fi . x9) + (s * r)let t be
Element of
K;
( (e |-- W1,(Lin {y})) `1 = x9 & (e |-- W1,(Lin {y})) `2 = t * v implies u = (fi . x9) + (t * r) )
assume that A5:
(e |-- W1,(Lin {y})) `1 = x9
and A6:
(e |-- W1,(Lin {y})) `2 = t * v
;
u = (fi . x9) + (t * r)
v <> 0. V
by A2, VECTSP_4:25;
then
t = s
by A4, A6, Th5, MCART_1:7;
hence
u = (fi . x9) + (t * r)
by A4, A5, MCART_1:7;
verum
end;
consider f being Function of the carrier of (X + (Lin {v})),the carrier of K such that
A7:
for e being Element of (X + (Lin {v})) holds S1[e,f . e]
from FUNCT_2:sch 3(A3);
reconsider f = f as Functional of (X + (Lin {v})) ;
A10:
y |-- W1,(Lin {y}) = [(0. W1),y]
by A1, A2, Th16;
then A11:
(y |-- W1,(Lin {y})) `1 = 0. X
by MCART_1:7;
A12:
f is additive
proof
let v1,
v2 be
Vector of
(X + (Lin {v}));
HAHNBAN1:def 11 f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being
Vector of
X,
s1 being
Element of
K such that A13:
v1 |-- W1,
(Lin {y}) = [x1,(s1 * v)]
by A1, A2, Th19;
A14:
(
(v1 |-- W1,(Lin {y})) `1 = x1 &
(v1 |-- W1,(Lin {y})) `2 = s1 * v )
by A13, MCART_1:7;
consider x2 being
Vector of
X,
s2 being
Element of
K such that A15:
v2 |-- W1,
(Lin {y}) = [x2,(s2 * v)]
by A1, A2, Th19;
A16:
(
(v2 |-- W1,(Lin {y})) `1 = x2 &
(v2 |-- W1,(Lin {y})) `2 = s2 * v )
by A15, MCART_1:7;
(v1 + v2) |-- W1,
(Lin {y}) = [(x1 + x2),((s1 + s2) * v)]
by A1, A2, A13, A15, Th20;
then
(
((v1 + v2) |-- W1,(Lin {y})) `1 = x1 + x2 &
((v1 + v2) |-- W1,(Lin {y})) `2 = (s1 + s2) * v )
by MCART_1:7;
hence f . (v1 + v2) =
(fi . (x1 + x2)) + ((s1 + s2) * r)
by A7
.=
(fi . (x1 + x2)) + ((s1 * r) + (s2 * r))
by VECTSP_1:def 12
.=
((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r))
by HAHNBAN1:def 11
.=
(((fi . x1) + (fi . x2)) + (s1 * r)) + (s2 * r)
by RLVECT_1:def 6
.=
(((fi . x1) + (s1 * r)) + (fi . x2)) + (s2 * r)
by RLVECT_1:def 6
.=
((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))
by RLVECT_1:def 6
.=
(f . v1) + ((fi . x2) + (s2 * r))
by A7, A14
.=
(f . v1) + (f . v2)
by A7, A16
;
verum
end;
f is homogeneous
proof
let v0 be
Vector of
(X + (Lin {v}));
HAHNBAN1:def 12 for b1 being Element of the carrier of K holds f . (b1 * v0) = b1 * (f . v0)let t be
Element of
K;
f . (t * v0) = t * (f . v0)
consider x0 being
Vector of
X,
s0 being
Element of
K such that A17:
v0 |-- W1,
(Lin {y}) = [x0,(s0 * v)]
by A1, A2, Th19;
A18:
(
(v0 |-- W1,(Lin {y})) `1 = x0 &
(v0 |-- W1,(Lin {y})) `2 = s0 * v )
by A17, MCART_1:7;
(t * v0) |-- W1,
(Lin {y}) = [(t * x0),((t * s0) * v)]
by A1, A2, A17, Th21;
then
(
((t * v0) |-- W1,(Lin {y})) `1 = t * x0 &
((t * v0) |-- W1,(Lin {y})) `2 = (t * s0) * v )
by MCART_1:7;
hence f . (t * v0) =
(fi . (t * x0)) + ((t * s0) * r)
by A7
.=
(t * (fi . x0)) + ((t * s0) * r)
by HAHNBAN1:def 12
.=
(t * (fi . x0)) + (t * (s0 * r))
by GROUP_1:def 4
.=
t * ((fi . x0) + (s0 * r))
by VECTSP_1:def 11
.=
t * (f . v0)
by A7, A18
;
verum
end;
then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
take
f
; ( f | the carrier of X = fi & f . y = r )
A19:
dom fi = the carrier of X
by FUNCT_2:def 1;
( dom f = the carrier of (X + (Lin {v})) & X is Subspace of X + (Lin {v}) )
by FUNCT_2:def 1, VECTSP_5:11;
then
dom fi c= dom f
by A19, VECTSP_4:def 2;
then
dom fi = (dom f) /\ the carrier of X
by A19, XBOOLE_1:28;
hence
f | the carrier of X = fi
by A8, FUNCT_1:68; f . y = r
(y |-- W1,(Lin {y})) `2 =
y
by A10, MCART_1:7
.=
(1_ K) * v
by A1, VECTSP_1:def 26
;
hence f . y =
(fi . (0. X)) + ((1_ K) * r)
by A7, A11
.=
(0. K) + ((1_ K) * r)
by HAHNBAN1:def 13
.=
(0. K) + r
by VECTSP_1:def 19
.=
r
by RLVECT_1:10
;
verum