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 ⊢ V = Base W
pjth.s ⊢ ⊕ ˙ = LSSum ⁡ W
pjth.o ⊢ O = ocv ⁡ W
pjth.j ⊢ J = TopOpen ⁡ W
pjth.l ⊢ L = LSubSp ⁡ W
Assertion pjth ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ⊕ ˙ O ⁡ U = V

Proof

Step Hyp Ref Expression
1 pjth.v ⊢ V = Base W
2 pjth.s ⊢ ⊕ ˙ = LSSum ⁡ W
3 pjth.o ⊢ O = ocv ⁡ W
4 pjth.j ⊢ J = TopOpen ⁡ W
5 pjth.l ⊢ L = LSubSp ⁡ W
6 hlphl ⊢ W ∈ ℂHil → W ∈ PreHil
7 6 3ad2ant1 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → W ∈ PreHil
8 phllmod ⊢ W ∈ PreHil → W ∈ LMod
9 7 8 syl ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → W ∈ LMod
10 simp2 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ∈ L
11 1 5 lssss ⊢ U ∈ L → U ⊆ V
12 11 3ad2ant2 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ⊆ V
13 1 3 5 ocvlss ⊢ W ∈ PreHil ∧ U ⊆ V → O ⁡ U ∈ L
14 7 12 13 syl2anc ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → O ⁡ U ∈ L
15 5 2 lsmcl ⊢ W ∈ LMod ∧ U ∈ L ∧ O ⁡ U ∈ L → U ⊕ ˙ O ⁡ U ∈ L
16 9 10 14 15 syl3anc ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ⊕ ˙ O ⁡ U ∈ L
17 1 5 lssss ⊢ U ⊕ ˙ O ⁡ U ∈ L → U ⊕ ˙ O ⁡ U ⊆ V
18 16 17 syl ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ⊕ ˙ O ⁡ U ⊆ V
19 eqid ⊢ norm ⁡ W = norm ⁡ W
20 eqid ⊢ + W = + W
21 eqid ⊢ - W = - W
22 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
23 simpl1 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J ∧ x ∈ V → W ∈ ℂHil
24 simpl2 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J ∧ x ∈ V → U ∈ L
25 simpr ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J ∧ x ∈ V → x ∈ V
26 simpl3 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J ∧ x ∈ V → U ∈ Clsd ⁡ J
27 1 19 20 21 22 5 23 24 25 4 2 3 26 pjthlem2 ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J ∧ x ∈ V → x ∈ U ⊕ ˙ O ⁡ U
28 18 27 eqelssd ⊢ W ∈ ℂHil ∧ U ∈ L ∧ U ∈ Clsd ⁡ J → U ⊕ ˙ O ⁡ U = V