Metamath Proof Explorer

Theorem latmrot

Description: Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012)

Ref Expression
Hypotheses olmass.b ⊢ B = Base K
olmass.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latmrot ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Z ∧ ˙ X ∧ ˙ Y

Proof

Step Hyp Ref Expression
1 olmass.b ⊢ B = Base K
2 olmass.m ⊢ ∧ ˙ = meet ⁡ K
3 ollat ⊢ K ∈ OL → K ∈ Lat
4 3 adantr ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
5 simpr1 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
6 simpr2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
7 1 2 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y ∈ B
8 4 5 6 7 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∈ B
9 simpr3 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
10 1 2 latmcom ⊢ K ∈ Lat ∧ X ∧ ˙ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Z ∧ ˙ X ∧ ˙ Y
11 4 8 9 10 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Z ∧ ˙ X ∧ ˙ Y
12 simpl ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ OL
13 1 2 latmassOLD ⊢ K ∈ OL ∧ Z ∈ B ∧ X ∈ B ∧ Y ∈ B → Z ∧ ˙ X ∧ ˙ Y = Z ∧ ˙ X ∧ ˙ Y
14 12 9 5 6 13 syl13anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∧ ˙ X ∧ ˙ Y = Z ∧ ˙ X ∧ ˙ Y
15 11 14 eqtr4d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Z ∧ ˙ X ∧ ˙ Y