Metamath Proof Explorer

Theorem latj4rot

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

Ref Expression
Hypotheses latjass.b ⊢B=BaseK
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=BaseK
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