Metamath Proof Explorer

Theorem pjth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102 (existence part). (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014)

Ref Expression
Hypotheses pjth.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
pjth.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
pjth.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
pjth.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
pjth.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion pjth ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 pjth.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 pjth.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 pjth.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
4 pjth.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
5 pjth.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
6 hlphl ⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )
7 6 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑊 ∈ PreHil )
8 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
9 7 8 syl ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑊 ∈ LMod )
10 simp2 ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ 𝐿 )
11 1 5 lssss ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉 )
12 11 3ad2ant2 ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ⊆ 𝑉 )
13 1 3 5 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑈 ) ∈ 𝐿 )
14 7 12 13 syl2anc ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑂 ‘ 𝑈 ) ∈ 𝐿 )
15 5 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ ( 𝑂 ‘ 𝑈 ) ∈ 𝐿 ) → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) ∈ 𝐿 )
16 9 10 14 15 syl3anc ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) ∈ 𝐿 )
17 1 5 lssss ⊢ ( ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) ∈ 𝐿 → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) ⊆ 𝑉 )
18 16 17 syl ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) ⊆ 𝑉 )
19 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
20 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
21 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
22 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
23 simpl1 ⊢ ( ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ ℂHil )
24 simpl2 ⊢ ( ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑈 ∈ 𝐿 )
25 simpr ⊢ ( ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
26 simpl3 ⊢ ( ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
27 1 19 20 21 22 5 23 24 25 4 2 3 26 pjthlem2 ⊢ ( ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) )
28 18 27 eqelssd ⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ⊕ ( 𝑂 ‘ 𝑈 ) ) = 𝑉 )