This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ C ℋ
fh1.2 ⊢ B ∈ C ℋ
fh1.3 ⊢ C ∈ C ℋ
fh1.4 ⊢ A 𝐶 ℋ B
fh1.5 ⊢ A 𝐶 ℋ C
Assertion cm2mi ⊢ A 𝐶 ℋ B ∩ C

Proof

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