Metamath Proof Explorer


Theorem latmlej12

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 latmlej12 ( ( 𝐾 ∈ Lat ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝑌 ) ( 𝑍 𝑋 ) )

Proof

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