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∈⊥⁡HA=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∈⊥⁡HA=x+ℎy
7 1 4 5 6 syl3anc ⊢H∈Cℋ∧A∈ℋ→∃x∈H∃y∈⊥⁡HA=x+ℎy