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

Metamath Proof Explorer

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 ⊢ H ⊆ ℋ → ⊥ ⁡ H = x ∈ ℋ | ∀ y ∈ H x ⋅ ih y = 0

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 elpw2 ⊢ H ∈ 𝒫 ℋ ↔ H ⊆ ℋ
3 raleq ⊢ z = H → ∀ y ∈ z x ⋅ ih y = 0 ↔ ∀ y ∈ H x ⋅ ih y = 0
4 3 rabbidv ⊢ z = H → x ∈ ℋ | ∀ y ∈ z x ⋅ ih y = 0 = x ∈ ℋ | ∀ y ∈ H x ⋅ ih y = 0
5 df-oc ⊢ ⊥ = z ∈ 𝒫 ℋ ⟼ x ∈ ℋ | ∀ y ∈ z x ⋅ ih y = 0
6 1 rabex ⊢ x ∈ ℋ | ∀ y ∈ H x ⋅ ih y = 0 ∈ V
7 4 5 6 fvmpt ⊢ H ∈ 𝒫 ℋ → ⊥ ⁡ H = x ∈ ℋ | ∀ y ∈ H x ⋅ ih y = 0
8 2 7 sylbir ⊢ H ⊆ ℋ → ⊥ ⁡ H = x ∈ ℋ | ∀ y ∈ H x ⋅ ih y = 0