let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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})); :: thesis: ( 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 ; :: thesis: 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:7;
let r be Element of K; :: thesis: 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})); :: thesis: 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, Th18;
take (fi . x) + (s * r) ; :: thesis: S1[e,(fi . x) + (s * r)]
let x9 be Vector of X; :: thesis: for s being Element of K st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds
(fi . x) + (s * r) = (fi . x9) + (s * r)
let t be Element of K; :: thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies (fi . x) + (s * r) = (fi . x9) + (t * r) )
assume that
A5: (e |-- (W1,(Lin {y}))) `1 = x9 and
A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; :: thesis: (fi . x) + (s * r) = (fi . x9) + (t * r)
v <> 0. V by A2, VECTSP_4:17;
then t = s by A4, A6, Th4;
hence (fi . x) + (s * r) = (fi . x9) + (t * r) by A4, A5; :: thesis: 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);
A8: now :: thesis: for a being object st a in dom fi holds
fi . a = f . a
let a be object ; :: thesis: ( a in dom fi implies fi . a = f . a )
assume a in dom fi ; :: thesis: fi . a = f . a
then reconsider x = a as Vector of X ;
X is Subspace of X + (Lin {v}) by VECTSP_5:7;
then the carrier of X c= the carrier of (X + (Lin {v})) by VECTSP_4:def 2;
then reconsider v1 = x as Vector of (X + (Lin {v})) ;
v1 in X ;
then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th16
.= [v1,((0. K) * v)] by Th1 ;
then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `2 = (0. K) * v ) ;
thus fi . a = (fi . x) + (0. K) by RLVECT_1:4
.= (fi . x) + ((0. K) * r)
.= f . a by A7, A9 ; :: thesis: verum
end;
reconsider f = f as Functional of (X + (Lin {v})) ;
A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th15;
then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X ;
A12: f is additive
proof
let v1, v2 be Vector of (X + (Lin {v})); :: according to VECTSP_1:def 19 :: thesis: 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, Th18;
A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13;
consider x2 being Vector of X, s2 being Element of K such that
A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th18;
A16: ( (v2 |-- (W1,(Lin {y}))) `1 = x2 & (v2 |-- (W1,(Lin {y}))) `2 = s2 * v ) by A15;
(v1 + v2) |-- (W1,(Lin {y})) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th19;
then ( ((v1 + v2) |-- (W1,(Lin {y}))) `1 = x1 + x2 & ((v1 + v2) |-- (W1,(Lin {y}))) `2 = (s1 + s2) * v ) ;
hence f . (v1 + v2) = (fi . (x1 + x2)) + ((s1 + s2) * r) by A7
.= (fi . (x1 + x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def 3
.= ((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def 20
.= (((fi . x1) + (fi . x2)) + (s1 * r)) + (s2 * r) by RLVECT_1:def 3
.= (((fi . x1) + (s1 * r)) + (fi . x2)) + (s2 * r) by RLVECT_1:def 3
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r)) by RLVECT_1:def 3
.= (f . v1) + ((fi . x2) + (s2 * r)) by A7, A14
.= (f . v1) + (f . v2) by A7, A16 ;
:: thesis: verum
end;
f is homogeneous
proof
let v0 be Vector of (X + (Lin {v})); :: according to HAHNBAN1:def 8 :: thesis: for b1 being Element of the carrier of K holds f . (b1 * v0) = b1 * (f . v0)
let t be Element of K; :: thesis: 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, Th18;
A18: ( (v0 |-- (W1,(Lin {y}))) `1 = x0 & (v0 |-- (W1,(Lin {y}))) `2 = s0 * v ) by A17;
(t * v0) |-- (W1,(Lin {y})) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th20;
then ( ((t * v0) |-- (W1,(Lin {y}))) `1 = t * x0 & ((t * v0) |-- (W1,(Lin {y}))) `2 = (t * s0) * v ) ;
hence f . (t * v0) = (fi . (t * x0)) + ((t * s0) * r) by A7
.= (t * (fi . x0)) + ((t * s0) * r) by HAHNBAN1:def 8
.= (t * (fi . x0)) + (t * (s0 * r)) by GROUP_1:def 3
.= t * ((fi . x0) + (s0 * r)) by VECTSP_1:def 2
.= t * (f . v0) by A7, A18 ;
:: thesis: verum
end;
then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
take f ; :: thesis: ( 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:7;
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:46; :: thesis: f . y = r
(y |-- (W1,(Lin {y}))) `2 = y by A10
.= (1_ K) * v by A1 ;
hence f . y = (fi . (0. X)) + ((1_ K) * r) by A7, A11
.= (0. K) + ((1_ K) * r) by HAHNBAN1:def 9
.= (0. K) + r
.= r by RLVECT_1:4 ;
:: thesis: verum