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 ) |
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 ) |