let V be RealLinearSpace; :: thesis: for X being Subspace of V
for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let X be Subspace of V; :: thesis: for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let v be VECTOR of V; :: thesis: ( not v in the carrier of X implies for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) ) )
assume A1: not v in the carrier of X ; :: thesis: for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let q be Banach-Functional of V; :: thesis: for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
let fi be linear-Functional of X; :: thesis: ( ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) implies ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) ) )
assume A2: for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ; :: thesis: ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
A3: the carrier of (Lin {v}) c= the carrier of ((Lin {v}) + X) by Th14;
v in Lin {v} by RLVECT_4:12;
then v in the carrier of (Lin {v}) by STRUCT_0:def 5;
then reconsider x0 = v as VECTOR of (X + (Lin {v})) by A3, RLSUB_2:9;
consider x1 being VECTOR of X;
reconsider v1 = x1 as VECTOR of V by RLSUB_1:18;
set A = { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ;
set B = { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ;
A4: { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } c= REAL

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } or a in REAL )
assume a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: a in REAL
then ex x being VECTOR of X ex y being VECTOR of V st
( a = (fi . x) - (q . (y - v)) & x = y ) ;
hence a in REAL ; :: thesis: verum

end;

A5: { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } c= REAL

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } or b in REAL )
assume b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: b in REAL
then ex x being VECTOR of X ex y being VECTOR of V st
( b = (fi . x) + (q . (v - y)) & x = y ) ;
hence b in REAL ; :: thesis: verum

end;

A6: now

let x1, x2 be VECTOR of X; :: thesis: for y1, y2 being VECTOR of V st x1 = y1 & x2 = y2 holds
(fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2))
let y1, y2 be VECTOR of V; :: thesis: ( x1 = y1 & x2 = y2 implies (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2)) )
assume ( x1 = y1 & x2 = y2 ) ; :: thesis: (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2))
then fi . (x1 - x2) <= q . (y1 - y2) by A2, RLSUB_1:24;
then A7: (fi . x1) - (fi . x2) <= q . (y1 - y2) by Th32;
y1 - y2 = (y1 + (0. V)) + (- y2) by RLVECT_1:10
.= (y1 + ((- v) + v)) + (- y2) by RLVECT_1:16
.= ((y1 - v) + v) + (- y2) by RLVECT_1:def 6
.= (y1 - v) + (v - y2) by RLVECT_1:def 6 ;
then q . (y1 - y2) <= (q . (y1 - v)) + (q . (v - y2)) by Def3;
then (fi . x1) - (fi . x2) <= (q . (v - y2)) + (q . (y1 - v)) by A7, XXREAL_0:2;
then fi . x1 <= (fi . x2) + ((q . (v - y2)) + (q . (y1 - v))) by XREAL_1:22;
then fi . x1 <= ((fi . x2) + (q . (v - y2))) + (q . (y1 - v)) ;
hence (fi . x1) - (q . (y1 - v)) <= (fi . x2) + (q . (v - y2)) by XREAL_1:22; :: thesis: verum

end;

A8: now

let a, b be R_eal; :: thesis: ( a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } & b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } implies a <= b )
assume a in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: ( b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } implies a <= b )
then consider x1 being VECTOR of X, y1 being VECTOR of V such that
A9: ( a = (fi . x1) - (q . (y1 - v)) & x1 = y1 ) ;
assume b in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ; :: thesis: a <= b
then consider x2 being VECTOR of X, y2 being VECTOR of V such that
A10: ( b = (fi . x2) + (q . (v - y2)) & x2 = y2 ) ;
thus a <= b by A6, A9, A10; :: thesis: verum

end;

( (fi . x1) - (q . (v1 - v)) in { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } & (fi . x1) + (q . (v - v1)) in { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } ) ;
then reconsider A = { ((fi . x) - (q . (y - v))) where x is VECTOR of X, y is VECTOR of V : x = y } , B = { ((fi . x) + (q . (v - y))) where x is VECTOR of X, y is VECTOR of V : x = y } as non empty Subset of ExtREAL by A4, A5, NUMBERS:31, XBOOLE_1:1;
A11: sup A <= inf B by A8, Th10;
A12: A <> {-infty }

proof

consider x being Element of A;
assume A = {-infty } ; :: thesis: contradiction
then ( x = -infty & x in REAL ) by A4, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

A is bounded_above

proof

consider b being Element of B;
reconsider b = b as Element of ExtREAL ;
b is UpperBound of A

proof

let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not x in A or x <= b )
thus ( not x in A or x <= b ) by A8; :: thesis: verum

end;

then reconsider b = b as UpperBound of A ;
take b ; :: according to SUPINF_1:def 11 :: thesis: b in REAL
thus b in REAL by A5, TARSKI:def 3; :: thesis: verum

end;

then reconsider r = sup A as Real by A12, XXREAL_2:57;
not v in X by A1, STRUCT_0:def 5;
then consider psi being linear-Functional of (X + (Lin {v})) such that
A13: psi | the carrier of X = fi and
A14: psi . x0 = r by Th34;
take psi ; :: thesis: ( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
thus psi | the carrier of X = fi by A13; :: thesis: for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v
let y be VECTOR of (X + (Lin {v})); :: thesis: for v being VECTOR of V st y = v holds
psi . y <= q . v
let u be VECTOR of V; :: thesis: ( y = u implies psi . y <= q . u )
assume A15: y = u ; :: thesis: psi . y <= q . u
y in X + (Lin {v}) by STRUCT_0:def 5;
then consider y1, y2' being VECTOR of V such that
A16: ( y1 in X & y2' in Lin {v} ) and
A17: y = y1 + y2' by RLSUB_2:5;
consider t being Real such that
A18: y2' = t * v by A16, RLVECT_4:11;
y1 in X + (Lin {v}) by A16, RLSUB_2:6;
then reconsider x = y1 as VECTOR of (X + (Lin {v})) by STRUCT_0:def 5;
reconsider x1 = x as VECTOR of X by A16, STRUCT_0:def 5;

per cases ( t = 0 or t > 0 or t < 0 ) ;

suppose t = 0 ; :: thesis: psi . y <= q . u

then y2' = 0. V by A18, RLVECT_1:23;
then A19: y = x1 by A17, RLVECT_1:10;
then fi . x1 <= q . u by A2, A15;
hence psi . y <= q . u by A13, A19, FUNCT_1:72; :: thesis: verum

end;

suppose A20: t > 0 ; :: thesis: psi . y <= q . u

y2' in X + (Lin {v}) by A16, RLSUB_2:6;
then reconsider y2 = y2' as VECTOR of (X + (Lin {v})) by STRUCT_0:def 5;
y2 = t * x0 by A18, RLSUB_1:22;
then A21: y = x + (t * x0) by A17, RLSUB_1:21;
A22: t " > 0 by A20;
A23: ((- t) " ) * x1 = ((- t) " ) * y1 by RLSUB_1:22;
then ((- t) " ) * x1 = ((- t) " ) * x by RLSUB_1:22;
then A24: fi . (((- t) " ) * x1) = psi . (((- t) " ) * x) by A13, FUNCT_1:72;
A25: t * ((t " ) * (q . u)) = (t * (t " )) * (q . u)
.= 1 * (q . u) by A20, XCMPLX_0:def 7
.= q . u ;
A26: psi . (x + (t * x0)) = (psi . x) + (psi . (t * x0)) by Def4
.= 1 * ((psi . x) + (t * (psi . x0))) by Def5
.= (t * (t " )) * ((psi . x) + (t * (psi . x0))) by A20, XCMPLX_0:def 7
.= t * (((t " ) * (psi . x)) + (((t " ) * t) * (psi . x0)))
.= t * (((t " ) * (psi . x)) + (1 * (psi . x0))) by A20, XCMPLX_0:def 7
.= t * ((psi . ((t " ) * x)) + r) by A14, Def5 ;
reconsider b = (psi . (((- t) " ) * x)) + (q . (v - (((- t) " ) * y1))) as R_eal by XBOOLE_0:def 3, XXREAL_0:def 4;
(psi . (((- t) " ) * x)) + (q . (v - (((- t) " ) * y1))) in B by A23, A24;
then inf B <= b by XXREAL_2:3;
then sup A <= b by A11, XXREAL_0:2;
then psi . (((- t) " ) * x) >= r - (q . (v - (((- t) " ) * y1))) by XREAL_1:22;
then A27: - (psi . (((- t) " ) * x)) <= - (r - (q . (v - (((- t) " ) * y1)))) by XREAL_1:26;
A28: - (psi . (((- t) " ) * x)) = (- 1) * (psi . (((- t) " ) * x))
.= psi . ((- 1) * (((- t) " ) * x)) by Def5
.= psi . (((- 1) * ((- t) " )) * x) by RLVECT_1:def 9
.= psi . (((- 1) * (- (t " ))) * x) by XCMPLX_1:224
.= psi . ((t " ) * x) ;
v - (((- t) " ) * y1) = v - ((- (t " )) * y1) by XCMPLX_1:224
.= v + (- (- ((t " ) * y1))) by RLVECT_4:6
.= v + ((t " ) * y1) by RLVECT_1:30 ;
then A29: psi . ((t " ) * x) <= (q . (v + ((t " ) * y1))) - r by A27, A28;
(t " ) * u = ((t " ) * y1) + ((t " ) * y2') by A15, A17, RLVECT_1:def 9
.= ((t " ) * y1) + (((t " ) * t) * v) by A18, RLVECT_1:def 9
.= ((t " ) * y1) + (1 * v) by A20, XCMPLX_0:def 7
.= v + ((t " ) * y1) by RLVECT_1:def 9 ;
then (psi . ((t " ) * x)) + r <= q . ((t " ) * u) by A29, XREAL_1:21;
then (psi . ((t " ) * x)) + r <= (t " ) * (q . u) by A22, Def6;
hence psi . y <= q . u by A20, A21, A25, A26, XREAL_1:66; :: thesis: verum

end;

suppose t < 0 ; :: thesis: psi . y <= q . u

then A30: - t > 0 by XREAL_1:60;
A31: - y2' = (- t) * v by A18, RLVECT_4:6;
A32: - y2' in Lin {v} by A16, RLSUB_1:30;
A33: y = y1 - (- y2') by A17, RLVECT_1:30;
- y2' in X + (Lin {v}) by A32, RLSUB_2:6;
then reconsider y2 = - y2' as VECTOR of (X + (Lin {v})) by STRUCT_0:def 5;
y2 = (- t) * x0 by A31, RLSUB_1:22;
then A34: y = x - ((- t) * x0) by A33, RLSUB_1:24;
A35: (- t) " > 0 by A30;
A36: ((- t) " ) * x1 = ((- t) " ) * y1 by RLSUB_1:22;
then ((- t) " ) * x1 = ((- t) " ) * x by RLSUB_1:22;
then A37: fi . (((- t) " ) * x1) = psi . (((- t) " ) * x) by A13, FUNCT_1:72;
A38: (- t) * (((- t) " ) * (q . u)) = ((- t) * ((- t) " )) * (q . u)
.= 1 * (q . u) by A30, XCMPLX_0:def 7
.= q . u ;
A39: psi . (x - ((- t) * x0)) = (psi . x) - (psi . ((- t) * x0)) by Th32
.= 1 * ((psi . x) - ((- t) * (psi . x0))) by Def5
.= ((- t) * ((- t) " )) * ((psi . x) - ((- t) * (psi . x0))) by A30, XCMPLX_0:def 7
.= (- t) * ((((- t) " ) * (psi . x)) - ((((- t) " ) * (- t)) * (psi . x0)))
.= (- t) * ((((- t) " ) * (psi . x)) - (1 * (psi . x0))) by A30, XCMPLX_0:def 7
.= (- t) * ((psi . (((- t) " ) * x)) - r) by A14, Def5 ;
reconsider a = (psi . (((- t) " ) * x)) - (q . ((((- t) " ) * y1) - v)) as R_eal by XBOOLE_0:def 3, XXREAL_0:def 4;
(psi . (((- t) " ) * x)) - (q . ((((- t) " ) * y1) - v)) in A by A36, A37;
then a <= sup A by XXREAL_2:4;
then A40: psi . (((- t) " ) * x) <= r + (q . ((((- t) " ) * y1) - v)) by XREAL_1:22;
((- t) " ) * u = (((- t) " ) * y1) - (((- t) " ) * (- y2')) by A15, A33, RLVECT_1:48
.= (((- t) " ) * y1) - ((((- t) " ) * (- t)) * v) by A31, RLVECT_1:def 9
.= (((- t) " ) * y1) - (1 * v) by A30, XCMPLX_0:def 7
.= (((- t) " ) * y1) - v by RLVECT_1:def 9 ;
then (psi . (((- t) " ) * x)) - r <= q . (((- t) " ) * u) by A40, XREAL_1:22;
then (psi . (((- t) " ) * x)) - r <= ((- t) " ) * (q . u) by A35, Def6;
hence psi . y <= q . u by A30, A34, A38, A39, XREAL_1:66; :: thesis: verum

end;

end;