Theorem cm2mi

Description: A lattice element that commutes with two others also commutes with their meet. Theorem 4.2 of Beran p. 49. (Contributed by NM, 11-May-2009) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fh1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	fh1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	fh1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	fh1.4	$$⊢A{𝐶}_{\mathscr{H}}B$$
	fh1.5	$$⊢A{𝐶}_{\mathscr{H}}C$$
Assertion	cm2mi	$$⊢A{𝐶}_{\mathscr{H}}\left(B\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fh1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		fh1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		fh1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		fh1.4	$$⊢A{𝐶}_{\mathscr{H}}B$$
5		fh1.5	$$⊢A{𝐶}_{\mathscr{H}}C$$
6	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	1 2 4	cmcm2ii	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(B\right)$$
9	1 3 5	cmcm2ii	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(C\right)$$
10	1 6 7 8 9	cm2ji	$$⊢A{𝐶}_{\mathscr{H}}\left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(C\right)\right)$$
11	2 3	chdmm1i	$$⊢\perp \left(B\cap C\right)=\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(C\right)$$
12	10 11	breqtrri	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(B\cap C\right)$$
13	2 3	chincli	$$⊢B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
14	1 13	cmcm2i	$$⊢A{𝐶}_{\mathscr{H}}\left(B\cap C\right)\leftrightarrow A{𝐶}_{\mathscr{H}}\perp \left(B\cap C\right)$$
15	12 14	mpbir	$$⊢A{𝐶}_{\mathscr{H}}\left(B\cap C\right)$$