# 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}={\mathrm{Base}}_{{K}}$
cmtid.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
Assertion cmtidN ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\right)\to {X}{C}{X}$

### Proof

Step Hyp Ref Expression
1 cmtid.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cmtid.c ${⊢}{C}=\mathrm{cm}\left({K}\right)$
3 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 1 4 latref ${⊢}\left({K}\in \mathrm{Lat}\wedge {X}\in {B}\right)\to {X}{\le }_{{K}}{X}$
6 3 5 sylan ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\right)\to {X}{\le }_{{K}}{X}$
7 1 4 2 lecmtN ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\wedge {X}\in {B}\right)\to \left({X}{\le }_{{K}}{X}\to {X}{C}{X}\right)$
8 7 3anidm23 ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\right)\to \left({X}{\le }_{{K}}{X}\to {X}{C}{X}\right)$
9 6 8 mpd ${⊢}\left({K}\in \mathrm{OML}\wedge {X}\in {B}\right)\to {X}{C}{X}$