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

Metamath Proof Explorer

Theorem cm2ji

Description: A lattice element that commutes with two others also commutes with their join. 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 cm2ji 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 )

Proof

Step Hyp Ref Expression
1 fh1.1 ⊢ 𝐴 ∈ Cℋ
2 fh1.2 ⊢ 𝐵 ∈ Cℋ
3 fh1.3 ⊢ 𝐶 ∈ Cℋ
4 fh1.4 ⊢ 𝐴 𝐶ℋ 𝐵
5 fh1.5 ⊢ 𝐴 𝐶ℋ 𝐶
6 1 2 3 3pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
7 4 5 pm3.2i ⊢ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 )
8 cm2j ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶 ) ) → 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 ) )
9 6 7 8 mp2an ⊢ 𝐴 𝐶ℋ ( 𝐵 ∨ℋ 𝐶 )