Theorem chm0i

Description: Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ch0le.1	⊢ 𝐴 ∈ Cℋ
Assertion	chm0i	⊢ ( 𝐴 ∩ 0ℋ ) = 0ℋ

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	⊢ 𝐴 ∈ Cℋ
2		inss2	⊢ ( 𝐴 ∩ 0ℋ ) ⊆ 0ℋ
3	1	ch0lei	⊢ 0ℋ ⊆ 𝐴
4		ssid	⊢ 0ℋ ⊆ 0ℋ
5	3 4	ssini	⊢ 0ℋ ⊆ ( 𝐴 ∩ 0ℋ )
6	2 5	eqssi	⊢ ( 𝐴 ∩ 0ℋ ) = 0ℋ