Theorem shne0i

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

	Ref	Expression
Hypothesis	shne0.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shne0i	$$⊢A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		shne0.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		df-ne	$$⊢A\ne 0_{\mathscr{H}}\leftrightarrow \neg A=0_{\mathscr{H}}$$
3		df-rex	$$⊢\exists x\in A\neg x\in 0_{\mathscr{H}}\leftrightarrow \exists x\left(x\in A\wedge \neg x\in 0_{\mathscr{H}}\right)$$
4		nss	$$⊢\neg A\subseteq 0_{\mathscr{H}}\leftrightarrow \exists x\left(x\in A\wedge \neg x\in 0_{\mathscr{H}}\right)$$
5		shle0	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$
6	1 5	ax-mp	$$⊢A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}$$
7	6	notbii	$$⊢\neg A\subseteq 0_{\mathscr{H}}\leftrightarrow \neg A=0_{\mathscr{H}}$$
8	3 4 7	3bitr2ri	$$⊢\neg A=0_{\mathscr{H}}\leftrightarrow \exists x\in A\neg x\in 0_{\mathscr{H}}$$
9		elch0	$$⊢x\in 0_{\mathscr{H}}\leftrightarrow x=0_{ℎ}$$
10	9	necon3bbii	$$⊢\neg x\in 0_{\mathscr{H}}\leftrightarrow x\ne 0_{ℎ}$$
11	10	rexbii	$$⊢\exists x\in A\neg x\in 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}$$
12	2 8 11	3bitri	$$⊢A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}$$