Metamath Proof Explorer


Theorem hlatjidm

Description: Idempotence of join operation. Frequently-used special case of latjcom for atoms. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypotheses hlatjcom.j ˙=joinK
hlatjcom.a A=AtomsK
Assertion hlatjidm KHLXAX˙X=X

Proof

Step Hyp Ref Expression
1 hlatjcom.j ˙=joinK
2 hlatjcom.a A=AtomsK
3 hllat KHLKLat
4 eqid BaseK=BaseK
5 4 2 atbase XAXBaseK
6 4 1 latjidm KLatXBaseKX˙X=X
7 3 5 6 syl2an KHLXAX˙X=X