Metamath Proof Explorer


Theorem cmtidN

Description: Any element commutes with itself. ( cmidi analog.) (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cmtid.b
|- B = ( Base ` K )
cmtid.c
|- C = ( cm ` K )
Assertion cmtidN
|- ( ( K e. OML /\ X e. B ) -> X C X )

Proof

Step Hyp Ref Expression
1 cmtid.b
 |-  B = ( Base ` K )
2 cmtid.c
 |-  C = ( cm ` K )
3 omllat
 |-  ( K e. OML -> K e. Lat )
4 eqid
 |-  ( le ` K ) = ( le ` K )
5 1 4 latref
 |-  ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) X )
6 3 5 sylan
 |-  ( ( K e. OML /\ X e. B ) -> X ( le ` K ) X )
7 1 4 2 lecmtN
 |-  ( ( K e. OML /\ X e. B /\ X e. B ) -> ( X ( le ` K ) X -> X C X ) )
8 7 3anidm23
 |-  ( ( K e. OML /\ X e. B ) -> ( X ( le ` K ) X -> X C X ) )
9 6 8 mpd
 |-  ( ( K e. OML /\ X e. B ) -> X C X )