Metamath Proof Explorer


Theorem latjjdi

Description: Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 latjass.b B=BaseK
2 latjass.j ˙=joinK
3 simpr1 KLatXBYBZBXB
4 1 2 latjidm KLatXBX˙X=X
5 3 4 syldan KLatXBYBZBX˙X=X
6 5 oveq1d KLatXBYBZBX˙X˙Y˙Z=X˙Y˙Z
7 simpl KLatXBYBZBKLat
8 simpr2 KLatXBYBZBYB
9 simpr3 KLatXBYBZBZB
10 1 2 latj4 KLatXBXBYBZBX˙X˙Y˙Z=X˙Y˙X˙Z
11 7 3 3 8 9 10 syl122anc KLatXBYBZBX˙X˙Y˙Z=X˙Y˙X˙Z
12 6 11 eqtr3d KLatXBYBZBX˙Y˙Z=X˙Y˙X˙Z