let X be RealHilbertSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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

proof

let r be ExtReal; :: thesis: ( r in Y implies r0 <= r )
assume r in Y ; :: thesis: r0 <= r
then ex y being Point of X st
( r = ||.(x - y).|| & y in M ) by A4;
hence r0 <= r by BHSP_1:28; :: thesis: verum

end;

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).||

proof

let y0 be Point of X; :: thesis: ( y0 in M implies d <= ||.(x - y0).|| )
assume y0 in M ; :: thesis: d <= ||.(x - y0).||
then ||.(x - y0).|| in Y by A4;
hence d <= ||.(x - y0).|| by A51, A4, SEQ_4:def 2; :: thesis: verum

end;

hereby :: thesis: ( ( 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).|| ; :: thesis: 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 ) ; :: thesis: contradiction
then 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 C11: ||.w.|| ^2 = 0 ; :: thesis: contradiction

||.w.|| = 0 by C11, SQUARE_1:17, SQUARE_1:22, BHSP_1:28;
then w = 0. X by BHSP_1:26;
hence contradiction by B1, BHSP_1:14; :: thesis: verum

end;

suppose CS2: ||.w.|| ^2 <> 0 ; :: thesis: contradiction

C2: ||.(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; :: thesis: verum

end;

end;

end;

assume AS2: for w being Point of X st w in M holds
w,x - x0 are_orthogonal ; :: thesis: d = ||.(x - x0).||
B1: for y being Point of X st y in M holds
||.(x - x0).|| <= ||.(x - y).||

proof

let y be Point of X; :: thesis: ( y in M implies ||.(x - x0).|| <= ||.(x - y).|| )
assume y in M ; :: thesis: ||.(x - x0).|| <= ||.(x - y).||
then C1: x0 - y,x - x0 are_orthogonal by AS2, A2, RUSUB_1:17;
x - y = (x - y) + (0. X)
.= (x + (- y)) + ((- x0) + x0) by RLVECT_1:5
.= ((x + (- y)) + (- x0)) + x0 by RLVECT_1:def 3
.= ((x + (- x0)) + (- y)) + x0 by RLVECT_1:def 3
.= (x - x0) + (x0 - y) by RLVECT_1:def 3 ;
then ||.(x - y).|| ^2 = (||.(x - x0).|| ^2) + (||.(x0 - y).|| ^2) by C1, RUSUB_5:30;
then C2: (||.(x - y).|| ^2) - (||.(x0 - y).|| ^2) = ||.(x - x0).|| ^2 ;
0 <= ||.(x0 - y).|| * ||.(x0 - y).|| by XREAL_1:63;
then C31: 0 <= ||.(x0 - y).|| ^2 by SQUARE_1:def 1;
0 <= ||.(x - x0).|| * ||.(x - x0).|| by XREAL_1:63;
then 0 <= ||.(x - x0).|| ^2 by SQUARE_1:def 1;
then sqrt (||.(x - x0).|| ^2) <= sqrt (||.(x - y).|| ^2) by C31, C2, XREAL_1:43, SQUARE_1:26;
then ||.(x - x0).|| <= sqrt (||.(x - y).|| ^2) by BHSP_1:28, SQUARE_1:22;
hence ||.(x - x0).|| <= ||.(x - y).|| by BHSP_1:28, SQUARE_1:22; :: thesis: verum

end;

for s being Real st s in Y holds
||.(x - x0).|| <= s

proof

let s be Real; :: thesis: ( s in Y implies ||.(x - x0).|| <= s )
assume s in Y ; :: thesis: ||.(x - x0).|| <= s
then consider y0 being Point of X such that
C1: ( s = ||.(x - y0).|| & y0 in M ) by A4;
thus ||.(x - x0).|| <= s by B1, C1; :: thesis: verum

end;

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; :: thesis: verum