# 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}\in {\mathbf{C}}_{ℋ}\to \left({A}\ne {0}_{ℋ}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}\right)$

### Proof

Step Hyp Ref Expression
1 neeq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}\ne {0}_{ℋ}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\ne {0}_{ℋ}\right)$
2 rexeq ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}↔\exists {x}\in if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}\right)$
3 1 2 bibi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(\left({A}\ne {0}_{ℋ}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\ne {0}_{ℋ}↔\exists {x}\in if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}\right)\right)$
4 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
5 4 elimel ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
6 5 chne0i ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\ne {0}_{ℋ}↔\exists {x}\in if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}$
7 3 6 dedth ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left({A}\ne {0}_{ℋ}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{ℎ}\right)$