This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjpjhthi

Description: Projection Theorem: Any Hilbert space vector A can be decomposed 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, 6-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjpjhth.1 ⊢ A ∈ ℋ
pjpjhth.2 ⊢ H ∈ C ℋ
Assertion pjpjhthi ⊢ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y

Proof

Step Hyp Ref Expression
1 pjpjhth.1 ⊢ A ∈ ℋ
2 pjpjhth.2 ⊢ H ∈ C ℋ
3 pjpjhth ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
4 2 1 3 mp2an ⊢ ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y