let V be RealLinearSpace; 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 Real 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 Real 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 Real 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 Real 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 Real 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 Real 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 RLSUB_2:7;
let r be Real; ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
defpred S1[ VECTOR of (X + (Lin {v})), Real] means for x being VECTOR of X
for s being Real st ($1 |-- (W1,(Lin {y}))) `1 = x & ($1 |-- (W1,(Lin {y}))) `2 = s * v holds
$2 = (fi . x) + (s * r);
A3:
now for e being Element of (X + (Lin {v})) ex u being Element of REAL st S1[e,u]let e be
Element of
(X + (Lin {v}));
ex u being Element of REAL st S1[e,u]consider x being
VECTOR of
X,
s being
Real such that A4:
e |-- (
W1,
(Lin {y}))
= [x,(s * v)]
by A1, A2, Th15;
reconsider u =
(fi . x) + (s * r) as
Element of
REAL by XREAL_0:def 1;
take u =
u;
S1[e,u]thus
S1[
e,
u]
verumproof
let x9 be
VECTOR of
X;
for s being Real st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds
u = (fi . x9) + (s * r)let t be
Real;
( (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, RLSUB_1:17;
then
t = s
by A4, A6, RLVECT_1:37;
hence
u = (fi . x9) + (t * r)
by A4, A5;
verum
end; end;
consider f being Function of the carrier of (X + (Lin {v})),REAL such that
A7:
for e being VECTOR 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, Th12;
then A11:
(y |-- (W1,(Lin {y}))) `1 = 0. X
;
A12:
f is additive
proof
let v1,
v2 be
VECTOR of
(X + (Lin {v}));
HAHNBAN:def 2 f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being
VECTOR of
X,
s1 being
Real such that A13:
v1 |-- (
W1,
(Lin {y}))
= [x1,(s1 * v)]
by A1, A2, Th15;
A14:
(
(v1 |-- (W1,(Lin {y}))) `1 = x1 &
(v1 |-- (W1,(Lin {y}))) `2 = s1 * v )
by A13;
consider x2 being
VECTOR of
X,
s2 being
Real such that A15:
v2 |-- (
W1,
(Lin {y}))
= [x2,(s2 * v)]
by A1, A2, Th15;
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, Th16;
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) + (fi . x2)) + ((s1 * r) + (s2 * r))
by Def2
.=
((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r))
.=
(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}));
HAHNBAN:def 3 for r being Real holds f . (r * v0) = r * (f . v0)let t be
Real;
f . (t * v0) = t * (f . v0)
consider x0 being
VECTOR of
X,
s0 being
Real such that A17:
v0 |-- (
W1,
(Lin {y}))
= [x0,(s0 * v)]
by A1, A2, Th15;
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, Th17;
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 Def3
.=
t * ((fi . x0) + (s0 * r))
.=
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 )
( dom fi = the carrier of X & dom f = the carrier of (X + (Lin {v})) )
by FUNCT_2:def 1;
then
dom fi = (dom f) /\ the carrier of X
by Th1, XBOOLE_1:28;
hence
f | the carrier of X = fi
by A8, FUNCT_1:46; f . y = r
(y |-- (W1,(Lin {y}))) `2 =
y
by A10
.=
1 * v
by A1, RLVECT_1:def 8
;
hence f . y =
(fi . (0. X)) + (1 * r)
by A7, A11
.=
0 + (1 * r)
by Th20
.=
r
;
verum