Metamath Proof Explorer

Theorem latjrot

Description: Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012)

Ref Expression
Hypotheses latjass.b ⊢ B = Base K
latjass.j ⊢ ∨ ˙ = join ⁡ K
Assertion latjrot ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = Z ∨ ˙ X ∨ ˙ Y

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ B = Base K
2 latjass.j ⊢ ∨ ˙ = join ⁡ K
3 1 2 latj31 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = Z ∨ ˙ Y ∨ ˙ X
4 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
5 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
6 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
7 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
8 1 2 latj32 ⊢ K ∈ Lat ∧ Z ∈ B ∧ Y ∈ B ∧ X ∈ B → Z ∨ ˙ Y ∨ ˙ X = Z ∨ ˙ X ∨ ˙ Y
9 4 5 6 7 8 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∨ ˙ Y ∨ ˙ X = Z ∨ ˙ X ∨ ˙ Y
10 3 9 eqtrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = Z ∨ ˙ X ∨ ˙ Y