let V be RealNormSpace; :: thesis: for x, m0 being Point of V
for M being non empty Subspace of V st not x in M & m0 in M holds
( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) )
let x, m0 be Point of V; :: thesis: for M being non empty Subspace of V st not x in M & m0 in M holds
( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) )
let M be non empty Subspace of V; :: thesis: ( not x in M & m0 in M implies ( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) ) )
assume that
A1: not x in M and
A2: m0 in M ; :: thesis: ( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) )
A3: ||.(x - m0).|| <> 0 by NORMSP_1:6, A1, A2;
consider L being non empty real-membered bounded_below set , U being non empty real-membered bounded_above set such that
A4: L = { ||.(x - m).|| where m is Point of V : m in M } and
U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } and
( inf L = sup U & sup U in U ) and
A5: ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) and
for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel by A1, Th21;

hereby :: thesis: ( ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) implies for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| )

assume A6: for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ; :: thesis: ex v being Point of (DualSp V) st
( v in Ort_Comp M & v <> 0. (DualSp V) & x - m0,v are_parallel )
A7: for r being Real st r in L holds
||.(x - m0).|| <= r

proof

let r be Real; :: thesis: ( r in L implies ||.(x - m0).|| <= r )
assume r in L ; :: thesis: ||.(x - m0).|| <= r
then consider m being Point of V such that
A8: ( r = ||.(x - m).|| & m in M ) by A4;
thus ||.(x - m0).|| <= r by A6, A8; :: thesis: verum

end;

for s being Real st 0 < s holds
ex r being Real st
( r in L & r < ||.(x - m0).|| + s )

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in L & r < ||.(x - m0).|| + s ) )
assume A9: 0 < s ; :: thesis: ex r being Real st
( r in L & r < ||.(x - m0).|| + s )
take r = ||.(x - m0).||; :: thesis: ( r in L & r < ||.(x - m0).|| + s )
thus r in L by A4, A2; :: thesis: r < ||.(x - m0).|| + s
||.(x - m0).|| + 0 < ||.(x - m0).|| + s by XREAL_1:8, A9;
hence r < ||.(x - m0).|| + s ; :: thesis: verum

end;

then A10P: ||.(x - m0).|| = lower_bound L by A7, SEQ_4:def 2;
then consider v being Point of (DualSp V) such that
A11: ( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) by A5, A3;
take v = v; :: thesis: ( v in Ort_Comp M & v <> 0. (DualSp V) & x - m0,v are_parallel )
thus v in Ort_Comp M by A11; :: thesis: ( v <> 0. (DualSp V) & x - m0,v are_parallel )
thus v <> 0. (DualSp V) by A11; :: thesis: x - m0,v are_parallel
(x - m0) .|. v = (x .|. v) - (m0 .|. v) by Th13
.= (inf L) - 0 by A11, A2, Th16
.= ||.(x - m0).|| * ||.v.|| by A10P, A11 ;
hence x - m0,v are_parallel ; :: thesis: verum

end;

given v being Point of (DualSp V) such that A13: ( v in Ort_Comp M & v <> 0. (DualSp V) & x - m0,v are_parallel ) ; :: thesis: for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).||
A14: ||.v.|| <> 0 by A13, NORMSP_0:def 5;
set p = (||.v.|| ") * v;
the carrier of (Ort_Comp M) = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by Def5;
then (||.v.|| ") * v in { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by STRUCT_0:def 5, A13, RLSUB_1:21;
then A16P: ex v0 being VECTOR of (DualSp V) st
( (||.v.|| ") * v = v0 & ( for w being VECTOR of V st w in M holds
w,v0 are_orthogonal ) ) ;
A17: ||.((||.v.|| ") * v).|| = |.(||.v.|| ").| * ||.v.|| by NORMSP_1:def 1
.= 1 by A14, XCMPLX_0:def 7 ;
A18P: (x - m0) .|. ((||.v.|| ") * v) = (||.v.|| ") * ((x - m0) .|. v) by DUALSP01:30
.= ||.(x - m0).|| * (|.(||.v.|| ").| * ||.v.||) by A13
.= ||.(x - m0).|| * ||.((||.v.|| ") * v).|| by NORMSP_1:def 1 ;
let m be Point of V; :: thesis: ( m in M implies ||.(x - m0).|| <= ||.(x - m).|| )
assume A19: m in M ; :: thesis: ||.(x - m0).|| <= ||.(x - m).||
A20: |.((x - m) .|. ((||.v.|| ") * v)).| <= ||.((||.v.|| ") * v).|| * ||.(x - m).|| by Th2;
m,(||.v.|| ") * v are_orthogonal by A16P, A19;
then A23P: x .|. ((||.v.|| ") * v) = (x .|. ((||.v.|| ") * v)) - (m .|. ((||.v.|| ") * v))
.= (x - m) .|. ((||.v.|| ") * v) by Th13 ;
A24: m0,(||.v.|| ") * v are_orthogonal by A16P, A2;
x .|. ((||.v.|| ") * v) = (x .|. ((||.v.|| ") * v)) - (m0 .|. ((||.v.|| ") * v)) by A24
.= ||.(x - m0).|| by A17, A18P, Th13 ;
hence ||.(x - m0).|| <= ||.(x - m).|| by A23P, A17, A20; :: thesis: verum