let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for x, m0 being Point of X st m0 in M holds
( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 )
let M be Subspace of X; :: thesis: for x, m0 being Point of X st m0 in M holds
( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 )
let x, m0 be Point of X; :: thesis: ( m0 in M implies ( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 ) )
assume A1: m0 in M ; :: thesis: ( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 )
hence ( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) implies for m being Point of X st m in M holds
(x - m0) .|. m = 0 ) by Lm2; :: thesis: ( ( for m being Point of X st m in M holds
(x - m0) .|. m = 0 ) implies for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| )
assume A2: for m being Point of X st m in M holds
(x - m0) .|. m = 0 ; :: thesis: for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).||
let m2 be Point of X; :: thesis: ( m2 in M implies ||.(x - m0).|| <= ||.(x - m2).|| )
assume m2 in M ; :: thesis: ||.(x - m0).|| <= ||.(x - m2).||
then A4: (x - m0) .|. (m0 - m2) = 0 by A2, A1, RUSUB_1:17;
A5: (x - m0) + (m0 - m2) = ((x - m0) + m0) - m2 by RLVECT_1:28
.= x - m2 by RLVECT_4:1 ;
0 <= ||.(m0 - m2).|| ^2 by XREAL_1:63;
then (||.(x - m0).|| ^2) + 0 <= (||.(x - m0).|| ^2) + (||.(m0 - m2).|| ^2) by XREAL_1:7;
then ||.(x - m0).|| ^2 <= ||.(x - m2).|| ^2 by A5, BHSP_5:6, BHSP_1:def 3, A4;
hence ||.(x - m0).|| <= ||.(x - m2).|| by SQUARE_1:16, BHSP_1:28; :: thesis: verum