Metamath Proof Explorer


Theorem chne0i

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

Ref Expression
Hypothesis ch0le.1 𝐴C
Assertion chne0i ( 𝐴 ≠ 0 ↔ ∃ 𝑥𝐴 𝑥 ≠ 0 )

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 1 chshii 𝐴S
3 2 shne0i ( 𝐴 ≠ 0 ↔ ∃ 𝑥𝐴 𝑥 ≠ 0 )