let X be RealHilbertSpace; for M being strict Subspace of X st X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
M = Ort_Comp (Ort_Comp M)
let M be strict Subspace of X; ( X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) implies M = Ort_Comp (Ort_Comp M) )
assume A1:
( X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) )
; M = Ort_Comp (Ort_Comp M)
reconsider N = the carrier of M as Subset of X by RUSUB_1:def 1;
reconsider N = N as non empty Subset of X ;
N is Subset of (Ort_Comp (Ort_Comp N))
by Th23;
then
N c= the carrier of (Ort_Comp (Ort_Comp N))
;
then
N c= the carrier of (Ort_Comp (Ort_Comp M))
by Lm6;
then A2:
M is Subspace of Ort_Comp (Ort_Comp M)
by RUSUB_1:22;
the carrier of (Ort_Comp (Ort_Comp M)) c= N
proof
let z be
object ;
TARSKI:def 3 ( not z in the carrier of (Ort_Comp (Ort_Comp M)) or z in N )
assume A3:
z in the
carrier of
(Ort_Comp (Ort_Comp M))
;
z in N
the
carrier of
(Ort_Comp (Ort_Comp M)) c= the
carrier of
X
by RUSUB_1:def 1;
then reconsider x =
z as
Point of
X by A3;
X is_the_direct_sum_of M,
Ort_Comp M
by Th25, A1;
then A4:
the
carrier of
X = { (v + u) where v, u is VECTOR of X : ( v in M & u in Ort_Comp M ) }
by RUSUB_2:def 1;
x in the
carrier of
X
;
then consider m,
n being
Point of
X such that A5:
(
x = m + n &
m in M &
n in Ort_Comp M )
by A4;
A6:
x - m = n
by RLVECT_4:1, A5;
A7:
x in Ort_Comp (Ort_Comp M)
by A3, STRUCT_0:def 5;
m in Ort_Comp (Ort_Comp M)
by A5, A2, RUSUB_1:2;
then A8:
n in Ort_Comp (Ort_Comp M)
by A6, RUSUB_1:17, A7;
reconsider K = the
carrier of
(Ort_Comp M) as non
empty Subset of
X by RUSUB_1:def 1;
A9:
n in K
by A5, STRUCT_0:def 5;
n in Ort_Comp K
by A8, Lm6;
then
n in the
carrier of
(Ort_Comp K)
by STRUCT_0:def 5;
then
n in Ort_CompSet K
by Lm5;
then
n .|. n = 0
by Def1, A9;
then
||.n.|| = 0
;
then
n = 0. X
by BHSP_1:26;
hence
z in N
by A5, STRUCT_0:def 5;
verum
end;
then
Ort_Comp (Ort_Comp M) is Subspace of M
by RUSUB_1:22;
hence
M = Ort_Comp (Ort_Comp M)
by RUSUB_1:20, A2; verum