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

Metamath Proof Explorer

Theorem lecmtN

Description: Ordered elements commute. ( lecmi analog.) (Contributed by NM, 10-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses lecmt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lecmt.l ⊢ ≤ = ( le ‘ 𝐾 )
lecmt.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion lecmtN ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑋 𝐶 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lecmt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lecmt.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lecmt.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
4 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
5 4 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
6 simp2 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
9 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
10 1 9 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
11 8 6 10 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
12 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
13 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
14 1 13 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 )
15 5 11 12 14 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 )
16 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
17 1 2 16 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑋 )
18 5 6 15 17 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑋 )
19 1 16 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ∈ 𝐵 )
20 5 6 15 19 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ∈ 𝐵 )
21 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑌 ) )
22 5 20 6 12 21 syl13anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑌 ) )
23 18 22 mpand ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑌 ) )
24 1 2 13 16 9 3 cmtbr4N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( meet ‘ 𝐾 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) 𝑌 ) ) ≤ 𝑌 ) )
25 23 24 sylibrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑋 𝐶 𝑌 ) )