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	⊢ 𝐴 ∈ ℋ
	pjpjhth.2	⊢ 𝐻 ∈ C_ℋ
Assertion	pjpjhthi	⊢ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +_ℎ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		pjpjhth.1	⊢ 𝐴 ∈ ℋ
2		pjpjhth.2	⊢ 𝐻 ∈ C_ℋ
3		pjpjhth	⊢ ( ( 𝐻 ∈ C_ℋ ∧ 𝐴 ∈ ℋ ) → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +_ℎ 𝑦 ) )
4	2 1 3	mp2an	⊢ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +_ℎ 𝑦 )