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 ⊢ B = Base K
lecmt.l ⊢ ≤ ˙ = ≤ K
lecmt.c ⊢ C = cm ⁡ K
Assertion lecmtN ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → X C Y

Proof

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