Metamath Proof Explorer


Theorem latjrot

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

Ref Expression
Hypotheses latjass.b B=BaseK
latjass.j ˙=joinK
Assertion latjrot KLatXBYBZBX˙Y˙Z=Z˙X˙Y

Proof

Step Hyp Ref Expression
1 latjass.b B=BaseK
2 latjass.j ˙=joinK
3 1 2 latj31 KLatXBYBZBX˙Y˙Z=Z˙Y˙X
4 simpl KLatXBYBZBKLat
5 simpr3 KLatXBYBZBZB
6 simpr2 KLatXBYBZBYB
7 simpr1 KLatXBYBZBXB
8 1 2 latj32 KLatZBYBXBZ˙Y˙X=Z˙X˙Y
9 4 5 6 7 8 syl13anc KLatXBYBZBZ˙Y˙X=Z˙X˙Y
10 3 9 eqtrd KLatXBYBZBX˙Y˙Z=Z˙X˙Y