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

Metamath Proof Explorer

Theorem pjpjhth

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
Assertion pjpjhth ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y

Proof

Step Hyp Ref Expression
1 axpjcl ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ∈ H
2 choccl ⊢ H ∈ C ℋ → ⊥ ⁡ H ∈ C ℋ
3 axpjcl ⊢ ⊥ ⁡ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ⊥ ⁡ H
4 2 3 sylan ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ⊥ ⁡ H
5 axpjpj ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A = proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
6 rspceov ⊢ proj ℎ ⁡ H ⁡ A ∈ H ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ⊥ ⁡ H ∧ A = proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
7 1 4 5 6 syl3anc ⊢ H ∈ C ℋ ∧ A ∈ ℋ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y