Theorem cntzsnid

Description: The centralizer of the identity element is the whole base set. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypotheses	cntzun.b	$$⊢B={\mathrm{Base}}_M$$
	cntzun.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
	cntzsnid.1	$$⊢\underset{\dot{}}{0}=0_M$$
Assertion	cntzsnid	$$⊢M\in \mathrm{Mnd}\to Z\left(\left\{\underset{\dot{}}{0}\right\}\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		cntzun.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzun.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		cntzsnid.1	$$⊢\underset{\dot{}}{0}=0_M$$
4	1 3	mndidcl	$$⊢M\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
5		eqid	$$⊢{+}_M={+}_M$$
6	1 5 2	elcntzsn	$$⊢\underset{\dot{}}{0}\in B\to \left(x\in Z\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(x\in B\wedge x{+}_M\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_{M}x\right)\right)$$
7	4 6	syl	$$⊢M\in \mathrm{Mnd}\to \left(x\in Z\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(x\in B\wedge x{+}_M\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_{M}x\right)\right)$$
8	1 5 3	mndrid	$$⊢\left(M\in \mathrm{Mnd}\wedge x\in B\right)\to x{+}_M\underset{\dot{}}{0}=x$$
9	1 5 3	mndlid	$$⊢\left(M\in \mathrm{Mnd}\wedge x\in B\right)\to \underset{\dot{}}{0}{+}_{M}x=x$$
10	8 9	eqtr4d	$$⊢\left(M\in \mathrm{Mnd}\wedge x\in B\right)\to x{+}_M\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_{M}x$$
11	10	ex	$$⊢M\in \mathrm{Mnd}\to \left(x\in B\to x{+}_M\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_{M}x\right)$$
12	11	pm4.71d	$$⊢M\in \mathrm{Mnd}\to \left(x\in B\leftrightarrow \left(x\in B\wedge x{+}_M\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_{M}x\right)\right)$$
13	7 12	bitr4d	$$⊢M\in \mathrm{Mnd}\to \left(x\in Z\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow x\in B\right)$$
14	13	eqrdv	$$⊢M\in \mathrm{Mnd}\to Z\left(\left\{\underset{\dot{}}{0}\right\}\right)=B$$