Metamath Proof Explorer

Theorem latj4rot

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

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

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ B = Base K
2 latjass.j ⊢ ∨ ˙ = join ⁡ K
3 simp1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → K ∈ Lat
4 simp3l ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Z ∈ B
5 simp3r ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → W ∈ B
6 1 2 latjcom ⊢ K ∈ Lat ∧ Z ∈ B ∧ W ∈ B → Z ∨ ˙ W = W ∨ ˙ Z
7 3 4 5 6 syl3anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → Z ∨ ˙ W = W ∨ ˙ Z
8 7 oveq2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ Y ∨ ˙ Z ∨ ˙ W = X ∨ ˙ Y ∨ ˙ W ∨ ˙ Z
9 5 4 jca ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → W ∈ B ∧ Z ∈ B
10 1 2 latj4 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ W ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ W ∨ ˙ Z = X ∨ ˙ W ∨ ˙ Y ∨ ˙ Z
11 9 10 syld3an3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ Y ∨ ˙ W ∨ ˙ Z = X ∨ ˙ W ∨ ˙ Y ∨ ˙ Z
12 simp2l ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∈ B
13 1 2 latjcom ⊢ K ∈ Lat ∧ X ∈ B ∧ W ∈ B → X ∨ ˙ W = W ∨ ˙ X
14 3 12 5 13 syl3anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ W = W ∨ ˙ X
15 14 oveq1d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ W ∨ ˙ Y ∨ ˙ Z = W ∨ ˙ X ∨ ˙ Y ∨ ˙ Z
16 8 11 15 3eqtrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ W ∈ B → X ∨ ˙ Y ∨ ˙ Z ∨ ˙ W = W ∨ ˙ X ∨ ˙ Y ∨ ˙ Z