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	⊢ 𝐴 ∈ Cℋ
	fh1.2	⊢ 𝐵 ∈ Cℋ
	fh1.3	⊢ 𝐶 ∈ Cℋ
	fh1.4	⊢ 𝐴 𝐶ℋ 𝐵
	fh1.5	⊢ 𝐴 𝐶ℋ 𝐶
Assertion	cm2mi	⊢ 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fh1.1	⊢ 𝐴 ∈ Cℋ
2		fh1.2	⊢ 𝐵 ∈ Cℋ
3		fh1.3	⊢ 𝐶 ∈ Cℋ
4		fh1.4	⊢ 𝐴 𝐶ℋ 𝐵
5		fh1.5	⊢ 𝐴 𝐶ℋ 𝐶
6	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
7	3	choccli	⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
8	1 2 4	cmcm2ii	⊢ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 )
9	1 3 5	cmcm2ii	⊢ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐶 )
10	1 6 7 8 9	cm2ji	⊢ 𝐴 𝐶ℋ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐶 ) )
11	2 3	chdmm1i	⊢ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐶 ) )
12	10 11	breqtrri	⊢ 𝐴 𝐶ℋ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) )
13	2 3	chincli	⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ
14	1 13	cmcm2i	⊢ ( 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 ) ↔ 𝐴 𝐶ℋ ( ⊥ ‘ ( 𝐵 ∩ 𝐶 ) ) )
15	12 14	mpbir	⊢ 𝐴 𝐶ℋ ( 𝐵 ∩ 𝐶 )