Theorem latmidm

Description: Lattice join is idempotent. ( inidm analog.) (Contributed by NM, 8-Nov-2011)

	Ref	Expression
Hypotheses	latmidm.b	|- B = ( Base ` K )
	latmidm.m	|- ./\ = ( meet ` K )
Assertion	latmidm	|- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) = X )

Proof

Step	Hyp	Ref	Expression
1		latmidm.b	|- B = ( Base ` K )
2		latmidm.m	|- ./\ = ( meet ` K )
3		eqid	|- ( le ` K ) = ( le ` K )
4		simpl	|- ( ( K e. Lat /\ X e. B ) -> K e. Lat )
5	1 2	latmcl	|- ( ( K e. Lat /\ X e. B /\ X e. B ) -> ( X ./\ X ) e. B )
6	5	3anidm23	|- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) e. B )
7		simpr	|- ( ( K e. Lat /\ X e. B ) -> X e. B )
8	1 3 2	latmle1	|- ( ( K e. Lat /\ X e. B /\ X e. B ) -> ( X ./\ X ) ( le ` K ) X )
9	8	3anidm23	|- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) ( le ` K ) X )
10	1 3	latref	|- ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) X )
11	1 3 2	latlem12	|- ( ( K e. Lat /\ ( X e. B /\ X e. B /\ X e. B ) ) -> ( ( X ( le ` K ) X /\ X ( le ` K ) X ) <-> X ( le ` K ) ( X ./\ X ) ) )
12	4 7 7 7 11	syl13anc	|- ( ( K e. Lat /\ X e. B ) -> ( ( X ( le ` K ) X /\ X ( le ` K ) X ) <-> X ( le ` K ) ( X ./\ X ) ) )
13	10 10 12	mpbi2and	|- ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) ( X ./\ X ) )
14	1 3 4 6 7 9 13	latasymd	|- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) = X )