Theorem cm0

Description: The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	cm0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}{𝐶}_{\mathscr{H}}A$$

Proof

Step	Hyp	Ref	Expression
1		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	choccli	$$⊢\perp \left(0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
3		chjcl	$$⊢\left(\perp \left(0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
4	2 3	mpan	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
5		chm0	$$⊢\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$
6	4 5	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$
7		chm0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$
8	6 7	eqtr4d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)\cap 0_{\mathscr{H}}=A\cap 0_{\mathscr{H}}$$
9		incom	$$⊢0_{\mathscr{H}}\cap \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)=\left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)\cap 0_{\mathscr{H}}$$
10		incom	$$⊢0_{\mathscr{H}}\cap A=A\cap 0_{\mathscr{H}}$$
11	8 9 10	3eqtr4g	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}\cap \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)=0_{\mathscr{H}}\cap A$$
12		cmbr3	$$⊢\left(0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}{𝐶}_{\mathscr{H}}A\leftrightarrow 0_{\mathscr{H}}\cap \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)=0_{\mathscr{H}}\cap A\right)$$
13	1 12	mpan	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}{𝐶}_{\mathscr{H}}A\leftrightarrow 0_{\mathscr{H}}\cap \left(\perp \left(0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right)=0_{\mathscr{H}}\cap A\right)$$
14	11 13	mpbird	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}{𝐶}_{\mathscr{H}}A$$