let X be RealUnitarySpace; for M being Subspace of X
for x, m0 being Point of X st m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) holds
for m being Point of X st m in M holds
(x - m0) .|. m = 0
let M be Subspace of X; for x, m0 being Point of X st m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) holds
for m being Point of X st m in M holds
(x - m0) .|. m = 0
let x, m0 be Point of X; ( m0 in M & ( 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 )
assume that
A1:
m0 in M
and
A2:
for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).||
; for m being Point of X st m in M holds
(x - m0) .|. m = 0
given m1 being Point of X such that A3:
( m1 in M & (x - m0) .|. m1 <> 0 )
; contradiction
A4p:
m1 <> 0. X
by A3, BHSP_1:15;
then A4:
||.m1.|| <> 0
by BHSP_1:26;
set m2 = (1 / ||.m1.||) * m1;
set a = ||.m1.||;
set delta = (x - m0) .|. ((1 / ||.m1.||) * m1);
(x - m0) .|. ((1 / ||.m1.||) * m1) = (1 / ||.m1.||) * ((x - m0) .|. m1)
by BHSP_1:3;
then A7:
0 < ((x - m0) .|. ((1 / ||.m1.||) * m1)) ^2
by SQUARE_1:12, A3, A4;
A8: ((1 / ||.m1.||) * m1) .|. ((1 / ||.m1.||) * m1) =
(1 / ||.m1.||) * (m1 .|. ((1 / ||.m1.||) * m1))
by BHSP_1:def 2
.=
(1 / ||.m1.||) * ((1 / ||.m1.||) * (m1 .|. m1))
by BHSP_1:3
.=
(1 / ||.m1.||) * ((1 / ||.m1.||) * (||.m1.|| ^2))
by Lm1
.=
(1 / ||.m1.||) * (((1 / ||.m1.||) * ||.m1.||) * ||.m1.||)
.=
(1 / ||.m1.||) * (1 * ||.m1.||)
by A4p, XCMPLX_1:87, BHSP_1:26
.=
1
by A4p, XCMPLX_1:87, BHSP_1:26
;
A9:
(1 / ||.m1.||) * m1 in M
by A3, RUSUB_1:15;
set m3 = m0 + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1));
A10p:
((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1) in M
by RUSUB_1:15, A9;
A11:
x - (m0 + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) = (x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))
by RLVECT_1:27;
A12: ||.(x - (m0 + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))).|| ^2 =
((x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) .|. ((x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))
by A11, Lm1
.=
(((x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) .|. (x - m0)) - (((x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))
by BHSP_1:12
.=
(((x - m0) .|. (x - m0)) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (x - m0))) - (((x - m0) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))
by BHSP_1:11
.=
(((x - m0) .|. (x - m0)) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (x - m0))) - (((x - m0) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))))
by BHSP_1:11
.=
(((x - m0) .|. (x - m0)) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (x - m0))) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((x - m0) .|. ((1 / ||.m1.||) * m1))) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))))
by BHSP_1:3
.=
(((x - m0) .|. (x - m0)) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * (((1 / ||.m1.||) * m1) .|. (x - m0)))) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((x - m0) .|. ((1 / ||.m1.||) * m1))) - ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1))))
by BHSP_1:3
.=
((((x - m0) .|. (x - m0)) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * (((1 / ||.m1.||) * m1) .|. (x - m0)))) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * (((1 / ||.m1.||) * m1) .|. (x - m0)))) + ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))
.=
(((x - m0) .|. (x - m0)) - ((2 * ((x - m0) .|. ((1 / ||.m1.||) * m1))) * (((1 / ||.m1.||) * m1) .|. (x - m0)))) + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)) .|. ((1 / ||.m1.||) * m1)))
by BHSP_1:3
.=
(((x - m0) .|. (x - m0)) - ((2 * ((x - m0) .|. ((1 / ||.m1.||) * m1))) * ((x - m0) .|. ((1 / ||.m1.||) * m1)))) + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * (((x - m0) .|. ((1 / ||.m1.||) * m1)) * (((1 / ||.m1.||) * m1) .|. ((1 / ||.m1.||) * m1))))
by BHSP_1:3
.=
((x - m0) .|. (x - m0)) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((x - m0) .|. ((1 / ||.m1.||) * m1)))
by A8
;
((x - m0) .|. (x - m0)) - (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((x - m0) .|. ((1 / ||.m1.||) * m1))) < ((x - m0) .|. (x - m0)) - 0
by A7, XREAL_1:15;
then A13:
||.(x - (m0 + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))).|| ^2 < ||.(x - m0).|| ^2
by Lm1, A12;
A14:
||.(x - m0).|| <= ||.(x - (m0 + (((x - m0) .|. ((1 / ||.m1.||) * m1)) * ((1 / ||.m1.||) * m1)))).||
by A2, A10p, A1, RUSUB_1:14;
0 <= ||.(x - m0).||
by BHSP_1:28;
hence
contradiction
by A13, A14, SQUARE_1:15; verum