let X be RealHilbertSpace; for f being linear-Functional of X st f is Lipschitzian holds
ex y being Point of X st
for x being Point of X holds f . x = x .|. y
let f be linear-Functional of X; ( f is Lipschitzian implies ex y being Point of X st
for x being Point of X holds f . x = x .|. y )
assume AS:
f is Lipschitzian
; ex y being Point of X st
for x being Point of X holds f . x = x .|. y
set M = UKer f;
A1:
the carrier of (UKer f) = f " {0}
by defuker;
per cases
( the carrier of X = the carrier of (UKer f) or the carrier of X <> the carrier of (UKer f) )
;
suppose
the
carrier of
X <> the
carrier of
(UKer f)
;
ex y being Point of X st
for x being Point of X holds f . x = x .|. ythen
not the
carrier of
X c= the
carrier of
(UKer f)
by RUSUB_1:def 1;
then consider z being
object such that B1:
(
z in the
carrier of
X & not
z in the
carrier of
(UKer f) )
;
reconsider y =
z as
Point of
X by B1;
reconsider N = the
carrier of
(UKer f) as non
empty Subset of
X by A1;
consider y1,
z1 being
Point of
X such that C0:
(
y1 in UKer f &
z1 in Ort_Comp (UKer f) &
y = y1 + z1 )
by Th87A, A1, AS, Lm89A;
C1:
z1 <> 0. X
by C0, B1;
then
||.z1.|| <> 0
by BHSP_1:26;
then C2:
||.z1.|| ^2 > 0
by SQUARE_1:12;
not
z1 in UKer f
by C0, C1, Lm89B;
then
not
z1 in f " {0}
by defuker;
then
not
f . z1 in {0}
by FUNCT_2:38;
then C3:
f . z1 <> 0
by TARSKI:def 1;
set r =
(f . z1) / (||.z1.|| ^2);
reconsider y =
((f . z1) / (||.z1.|| ^2)) * z1 as
Point of
X ;
C4:
y in Ort_Comp (UKer f)
by C0, RUSUB_1:15;
C5:
for
x being
Point of
X holds
f . x = x .|. y
proof
let x be
Point of
X;
f . x = x .|. y
set s =
(f . x) / (f . z1);
reconsider y0 =
x - (((f . x) / (f . z1)) * z1) as
Point of
X ;
D1:
- (((f . x) / (f . z1)) * z1) =
(- 1) * (((f . x) / (f . z1)) * z1)
by RLVECT_1:16
.=
((- 1) * ((f . x) / (f . z1))) * z1
by RLVECT_1:def 7
;
f . y0 =
(f . x) + (f . (((- 1) * ((f . x) / (f . z1))) * z1))
by D1, HAHNBAN:def 2
.=
(f . x) + (((- 1) * ((f . x) / (f . z1))) * (f . z1))
by HAHNBAN:def 3
.=
(f . x) - (((f . x) / (f . z1)) * (f . z1))
.=
(f . x) - (f . x)
by C3, XCMPLX_1:87
.=
0
;
then
(
y0 in X &
f . y0 in {0} )
by TARSKI:def 1;
then
y0 in f " {0}
by FUNCT_2:38;
then D2:
y0 in UKer f
by defuker;
y in { v where v is VECTOR of X : for w being VECTOR of X st w in UKer f holds
w,v are_orthogonal }
by RUSUB_5:def 3, C4;
then consider v being
VECTOR of
X such that D3:
(
y = v & ( for
w being
VECTOR of
X st
w in UKer f holds
w,
v are_orthogonal ) )
;
D41:
y0,
y are_orthogonal
by D2, D3;
D6:
(x - (((f . x) / (f . z1)) * z1)) .|. (((f . z1) / (||.z1.|| ^2)) * z1) =
(x .|. (((f . z1) / (||.z1.|| ^2)) * z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1))
by BHSP_1:11
.=
(((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1))
by BHSP_1:3
.=
(((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - (((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1)))
by BHSP_1:def 2
;
D7:
((f . x) / (f . z1)) * ((f . z1) / (||.z1.|| ^2)) = (f . x) / (||.z1.|| ^2)
by C3, XCMPLX_1:98;
D8:
0 <= z1 .|. z1
by BHSP_1:def 2;
z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1) =
((f . z1) / (||.z1.|| ^2)) * (z1 .|. z1)
by BHSP_1:3
.=
((f . z1) / (||.z1.|| ^2)) * (||.z1.|| ^2)
by D8, SQUARE_1:def 2
;
then ((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1)) =
((f . x) / (||.z1.|| ^2)) * (||.z1.|| ^2)
by D7
.=
f . x
by C2, XCMPLX_1:87
;
hence
f . x = x .|. y
by BHSP_1:3, D6, D41;
verum
end; take
y
;
for x being Point of X holds f . x = x .|. ythus
for
x being
Point of
X holds
f . x = x .|. y
by C5;
verum end;