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 𝐴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 𝐴 𝐶 ( 𝐵𝐶 )