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	⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ⊊ 𝐴 ↔ 𝐴 ≠ 0ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		df-pss	⊢ ( 0ℋ ⊊ 𝐴 ↔ ( 0ℋ ⊆ 𝐴 ∧ 0ℋ ≠ 𝐴 ) )
2		necom	⊢ ( 0ℋ ≠ 𝐴 ↔ 𝐴 ≠ 0ℋ )
3		ch0le	⊢ ( 𝐴 ∈ Cℋ → 0ℋ ⊆ 𝐴 )
4	3	biantrurd	⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ≠ 𝐴 ↔ ( 0ℋ ⊆ 𝐴 ∧ 0ℋ ≠ 𝐴 ) ) )
5	2 4	bitr3id	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ≠ 0ℋ ↔ ( 0ℋ ⊆ 𝐴 ∧ 0ℋ ≠ 𝐴 ) ) )
6	1 5	bitr4id	⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ⊊ 𝐴 ↔ 𝐴 ≠ 0ℋ ) )