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	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chne0i	$$⊢A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
3	2	shne0i	$$⊢A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}$$