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 = ( Base ` M )
	cntzun.z	|- Z = ( Cntz ` M )
	cntzsnid.1	|- .0. = ( 0g ` M )
Assertion	cntzsnid	|- ( M e. Mnd -> ( Z ` { .0. } ) = B )

Proof

Step	Hyp	Ref	Expression
1		cntzun.b	|- B = ( Base ` M )
2		cntzun.z	|- Z = ( Cntz ` M )
3		cntzsnid.1	|- .0. = ( 0g ` M )
4	1 3	mndidcl	|- ( M e. Mnd -> .0. e. B )
5		eqid	|- ( +g ` M ) = ( +g ` M )
6	1 5 2	elcntzsn	|- ( .0. e. B -> ( x e. ( Z ` { .0. } ) <-> ( x e. B /\ ( x ( +g ` M ) .0. ) = ( .0. ( +g ` M ) x ) ) ) )
7	4 6	syl	|- ( M e. Mnd -> ( x e. ( Z ` { .0. } ) <-> ( x e. B /\ ( x ( +g ` M ) .0. ) = ( .0. ( +g ` M ) x ) ) ) )
8	1 5 3	mndrid	|- ( ( M e. Mnd /\ x e. B ) -> ( x ( +g ` M ) .0. ) = x )
9	1 5 3	mndlid	|- ( ( M e. Mnd /\ x e. B ) -> ( .0. ( +g ` M ) x ) = x )
10	8 9	eqtr4d	|- ( ( M e. Mnd /\ x e. B ) -> ( x ( +g ` M ) .0. ) = ( .0. ( +g ` M ) x ) )
11	10	ex	|- ( M e. Mnd -> ( x e. B -> ( x ( +g ` M ) .0. ) = ( .0. ( +g ` M ) x ) ) )
12	11	pm4.71d	|- ( M e. Mnd -> ( x e. B <-> ( x e. B /\ ( x ( +g ` M ) .0. ) = ( .0. ( +g ` M ) x ) ) ) )
13	7 12	bitr4d	|- ( M e. Mnd -> ( x e. ( Z ` { .0. } ) <-> x e. B ) )
14	13	eqrdv	|- ( M e. Mnd -> ( Z ` { .0. } ) = B )