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

then A51: Y is bounded_below ;

A6: for y0 being Point of X st y0 in M holds

d <= ||.(x - y0).||

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

||.(x - x0).|| <= s

d <= ||.(x - x0).|| by A2, A6;

hence d = ||.(x - x0).|| by B2, XXREAL_0:1; :: thesis: verum

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

then
r0 is LowerBound of Y
by XXREAL_2:def 2;
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;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

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;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

hereby :: thesis: ( ( for w being Point of X st w in M holds

w,x - x0 are_orthogonal ) implies d = ||.(x - x0).|| )

assume AS2:
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;

end;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 )
;

end;

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;then w = 0. X by BHSP_1:26;

hence contradiction by B1, BHSP_1:14; :: thesis: verum

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;.= ((||.(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

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

for s being Real st s in Y holds
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;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

||.(x - x0).|| <= s

proof

then B2:
||.(x - x0).|| <= d
by A4, SEQ_4:43;
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;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

d <= ||.(x - x0).|| by A2, A6;

hence d = ||.(x - x0).|| by B2, XXREAL_0:1; :: thesis: verum