Theorem ch0pss

Description: The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	ch0pss	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}\subset A\leftrightarrow A\ne 0_{\mathscr{H}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-pss	$$⊢0_{\mathscr{H}}\subset A\leftrightarrow \left(0_{\mathscr{H}}\subseteq A\wedge 0_{\mathscr{H}}\ne A\right)$$
2		necom	$$⊢0_{\mathscr{H}}\ne A\leftrightarrow A\ne 0_{\mathscr{H}}$$
3		ch0le	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq A$$
4	3	biantrurd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}\ne A\leftrightarrow \left(0_{\mathscr{H}}\subseteq A\wedge 0_{\mathscr{H}}\ne A\right)\right)$$
5	2 4	bitr3id	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\ne 0_{\mathscr{H}}\leftrightarrow \left(0_{\mathscr{H}}\subseteq A\wedge 0_{\mathscr{H}}\ne A\right)\right)$$
6	1 5	bitr4id	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}\subset A\leftrightarrow A\ne 0_{\mathscr{H}}\right)$$