Metamath Proof Explorer


Theorem latmlej21

Description: Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012)

Ref Expression
Hypotheses latledi.b 𝐵 = ( Base ‘ 𝐾 )
latledi.l = ( le ‘ 𝐾 )
latledi.j = ( join ‘ 𝐾 )
latledi.m = ( meet ‘ 𝐾 )
Assertion latmlej21 ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑌 𝑋 ) ( 𝑋 𝑍 ) )

Proof

Step Hyp Ref Expression
1 latledi.b 𝐵 = ( Base ‘ 𝐾 )
2 latledi.l = ( le ‘ 𝐾 )
3 latledi.j = ( join ‘ 𝐾 )
4 latledi.m = ( meet ‘ 𝐾 )
5 1 4 latmcom ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )
6 5 3adant3r3 ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝑌 ) = ( 𝑌 𝑋 ) )
7 1 2 3 4 latmlej11 ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝑌 ) ( 𝑋 𝑍 ) )
8 6 7 eqbrtrrd ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑌 𝑋 ) ( 𝑋 𝑍 ) )