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}}_{\mathscr{H}}\to \left(A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}\right)$$

Proof

Step	Hyp	Ref	Expression
1		neeq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A\ne 0_{\mathscr{H}}\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\right)$$
2		rexeq	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(\exists x\in Ax\ne 0_{ℎ}\leftrightarrow \exists x\in if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)x\ne 0_{ℎ}\right)$$
3	1 2	bibi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(\left(A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)x\ne 0_{ℎ}\right)\right)$$
4		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	chne0i	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)x\ne 0_{ℎ}$$
7	3 6	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in Ax\ne 0_{ℎ}\right)$$