Theorem ocval

Description: Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ocval	⊢ ( 𝐻 ⊆ ℋ → ( ⊥ ‘ 𝐻 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 } )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2	1	elpw2	⊢ ( 𝐻 ∈ 𝒫 ℋ ↔ 𝐻 ⊆ ℋ )
3		raleq	⊢ ( 𝑧 = 𝐻 → ( ∀ 𝑦 ∈ 𝑧 ( 𝑥 ·ih 𝑦 ) = 0 ↔ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 ) )
4	3	rabbidv	⊢ ( 𝑧 = 𝐻 → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝑧 ( 𝑥 ·ih 𝑦 ) = 0 } = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 } )
5		df-oc	⊢ ⊥ = ( 𝑧 ∈ 𝒫 ℋ ↦ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝑧 ( 𝑥 ·ih 𝑦 ) = 0 } )
6	1	rabex	⊢ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 } ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐻 ∈ 𝒫 ℋ → ( ⊥ ‘ 𝐻 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 } )
8	2 7	sylbir	⊢ ( 𝐻 ⊆ ℋ → ( ⊥ ‘ 𝐻 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ih 𝑦 ) = 0 } )