let X be RealHilbertSpace; for M being Subspace of X
for x, x0 being Point of X
for d being Real st x0 in M & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )
let M be Subspace of X; for x, x0 being Point of X
for d being Real st x0 in M & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )
let x, x0 be Point of X; for d being Real st x0 in M & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds
( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )
let d be Real; ( x0 in M & ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) implies ( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal ) )
assume that
A2:
x0 in M
and
A3:
ex Y being non empty Subset of REAL st
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 )
; ( d = ||.(x - x0).|| iff for w being Point of X st w in M holds
w,x - x0 are_orthogonal )
consider Y being non empty Subset of REAL such that
A4:
( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 )
by A3;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Y holds
r0 <= r
then
r0 is LowerBound of Y
by XXREAL_2:def 2;
then A51:
Y is bounded_below
;
A6:
for y0 being Point of X st y0 in M holds
d <= ||.(x - y0).||
hereby ( ( for w being Point of X st w in M holds
w,x - x0 are_orthogonal ) implies d = ||.(x - x0).|| )
assume AS1:
d = ||.(x - x0).||
;
for w being Point of X st w in M holds
w,x - x0 are_orthogonal assume
ex
w being
Point of
X st
(
w in M & not
w,
x - x0 are_orthogonal )
;
contradictionthen consider w being
Point of
X such that B1:
(
w in M &
w .|. (x - x0) <> 0 )
;
set e =
w .|. (x - x0);
set r =
(w .|. (x - x0)) / (||.w.|| ^2);
set s =
||.w.|| ^2 ;
reconsider w0 =
x0 + (((w .|. (x - x0)) / (||.w.|| ^2)) * w) as
Point of
X ;
B21:
((w .|. (x - x0)) / (||.w.|| ^2)) * w in M
by B1, RUSUB_1:15;
per cases
( ||.w.|| ^2 = 0 or ||.w.|| ^2 <> 0 )
;
suppose CS2:
||.w.|| ^2 <> 0
;
contradictionC2:
||.(x - w0).|| ^2 =
||.((x - x0) - (((w .|. (x - x0)) / (||.w.|| ^2)) * w)).|| ^2
by RLVECT_1:27
.=
((||.(x - x0).|| ^2) - (2 * ((x - x0) .|. (((w .|. (x - x0)) / (||.w.|| ^2)) * w)))) + (||.(((w .|. (x - x0)) / (||.w.|| ^2)) * w).|| ^2)
by RUSUB_5:29
;
C3:
(x - x0) .|. (((w .|. (x - x0)) / (||.w.|| ^2)) * w) =
((w .|. (x - x0)) / (||.w.|| ^2)) * (w .|. (x - x0))
by BHSP_1:3
.=
((w .|. (x - x0)) * (w .|. (x - x0))) / (||.w.|| ^2)
by XCMPLX_1:74
.=
((w .|. (x - x0)) ^2) / (||.w.|| ^2)
by SQUARE_1:def 1
;
C4:
||.(((w .|. (x - x0)) / (||.w.|| ^2)) * w).|| ^2 =
(|.((w .|. (x - x0)) / (||.w.|| ^2)).| * ||.w.||) ^2
by BHSP_1:27
.=
(|.((w .|. (x - x0)) / (||.w.|| ^2)).| ^2) * (||.w.|| ^2)
by SQUARE_1:9
.=
(((w .|. (x - x0)) / (||.w.|| ^2)) ^2) * (||.w.|| ^2)
by COMPLEX1:75
.=
(((w .|. (x - x0)) * (1 / (||.w.|| ^2))) ^2) * (||.w.|| ^2)
by XCMPLX_1:99
.=
(((w .|. (x - x0)) ^2) * ((1 / (||.w.|| ^2)) ^2)) * (||.w.|| ^2)
by SQUARE_1:9
.=
((w .|. (x - x0)) ^2) * (((1 / (||.w.|| ^2)) ^2) * (||.w.|| ^2))
.=
((w .|. (x - x0)) ^2) * (((1 / (||.w.|| ^2)) * (1 / (||.w.|| ^2))) * (||.w.|| ^2))
by SQUARE_1:def 1
.=
((w .|. (x - x0)) ^2) * ((1 / (||.w.|| ^2)) * ((1 / (||.w.|| ^2)) * (||.w.|| ^2)))
.=
((w .|. (x - x0)) ^2) * ((1 / (||.w.|| ^2)) * 1)
by CS2, XCMPLX_1:106
.=
((w .|. (x - x0)) ^2) / (||.w.|| ^2)
by XCMPLX_1:99
;
C5:
||.(x - w0).|| ^2 = (||.(x - x0).|| ^2) - (((w .|. (x - x0)) ^2) / (||.w.|| ^2))
by C3, C4, C2;
C6:
0 < (w .|. (x - x0)) ^2
by B1, SQUARE_1:12;
0 <= ||.w.||
by BHSP_1:28;
then
0 <= ||.w.|| * ||.w.||
;
then
0 < ||.w.|| ^2
by CS2, SQUARE_1:def 1;
then C7:
||.(x - w0).|| ^2 < ||.(x - x0).|| ^2
by C5, XREAL_1:44, C6;
0 <= ||.(x - w0).|| * ||.(x - w0).||
by XREAL_1:63;
then
0 <= ||.(x - w0).|| ^2
by SQUARE_1:def 1;
then
sqrt (||.(x - w0).|| ^2) < sqrt (||.(x - x0).|| ^2)
by C7, SQUARE_1:27;
then C91:
||.(x - w0).|| < sqrt (||.(x - x0).|| ^2)
by BHSP_1:28, SQUARE_1:22;
d <= ||.(x - w0).||
by A6, B21, A2, RUSUB_1:14;
hence
contradiction
by C91, AS1, BHSP_1:28, SQUARE_1:22;
verum end; end;
end;
assume AS2:
for w being Point of X st w in M holds
w,x - x0 are_orthogonal
; d = ||.(x - x0).||
B1:
for y being Point of X st y in M holds
||.(x - x0).|| <= ||.(x - y).||
for s being Real st s in Y holds
||.(x - x0).|| <= s
then B2:
||.(x - x0).|| <= d
by A4, SEQ_4:43;
d <= ||.(x - x0).||
by A2, A6;
hence
d = ||.(x - x0).||
by B2, XXREAL_0:1; verum