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ℎ )