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

Metamath Proof Explorer

Theorem elch0

Description: Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001) (New usage is discouraged.)

Ref Expression
Assertion elch0 ⊢ A ∈ 0 ℋ ↔ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 df-ch0 ⊢ 0 ℋ = 0 ℎ
2 1 eleq2i ⊢ A ∈ 0 ℋ ↔ A ∈ 0 ℎ
3 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
4 3 elexi ⊢ 0 ℎ ∈ V
5 4 elsn2 ⊢ A ∈ 0 ℎ ↔ A = 0 ℎ
6 2 5 bitri ⊢ A ∈ 0 ℋ ↔ A = 0 ℎ