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

Metamath Proof Explorer

Theorem chne0

Description: A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion chne0 ⊢ A ∈ C ℋ → A ≠ 0 ℋ ↔ ∃ x ∈ A x ≠ 0 ℎ

Proof

Step Hyp Ref Expression
1 neeq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ≠ 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ≠ 0 ℋ
2 rexeq ⊢ A = if A ∈ C ℋ A 0 ℋ → ∃ x ∈ A x ≠ 0 ℎ ↔ ∃ x ∈ if A ∈ C ℋ A 0 ℋ x ≠ 0 ℎ
3 1 2 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ≠ 0 ℋ ↔ ∃ x ∈ A x ≠ 0 ℎ ↔ if A ∈ C ℋ A 0 ℋ ≠ 0 ℋ ↔ ∃ x ∈ if A ∈ C ℋ A 0 ℋ x ≠ 0 ℎ
4 h0elch ⊢ 0 ℋ ∈ C ℋ
5 4 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
6 5 chne0i ⊢ if A ∈ C ℋ A 0 ℋ ≠ 0 ℋ ↔ ∃ x ∈ if A ∈ C ℋ A 0 ℋ x ≠ 0 ℎ
7 3 6 dedth ⊢ A ∈ C ℋ → A ≠ 0 ℋ ↔ ∃ x ∈ A x ≠ 0 ℎ