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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzun.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
	cntzsnid.1	⊢ 0 = ( 0g ‘ 𝑀 )
Assertion	cntzsnid	⊢ ( 𝑀 ∈ Mnd → ( 𝑍 ‘ { 0 } ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cntzun.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzun.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3		cntzsnid.1	⊢ 0 = ( 0g ‘ 𝑀 )
4	1 3	mndidcl	⊢ ( 𝑀 ∈ Mnd → 0 ∈ 𝐵 )
5		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
6	1 5 2	elcntzsn	⊢ ( 0 ∈ 𝐵 → ( 𝑥 ∈ ( 𝑍 ‘ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = ( 0 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
7	4 6	syl	⊢ ( 𝑀 ∈ Mnd → ( 𝑥 ∈ ( 𝑍 ‘ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = ( 0 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
8	1 5 3	mndrid	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = 𝑥 )
9	1 5 3	mndlid	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
10	8 9	eqtr4d	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = ( 0 ( +g ‘ 𝑀 ) 𝑥 ) )
11	10	ex	⊢ ( 𝑀 ∈ Mnd → ( 𝑥 ∈ 𝐵 → ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = ( 0 ( +g ‘ 𝑀 ) 𝑥 ) ) )
12	11	pm4.71d	⊢ ( 𝑀 ∈ Mnd → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ( +g ‘ 𝑀 ) 0 ) = ( 0 ( +g ‘ 𝑀 ) 𝑥 ) ) ) )
13	7 12	bitr4d	⊢ ( 𝑀 ∈ Mnd → ( 𝑥 ∈ ( 𝑍 ‘ { 0 } ) ↔ 𝑥 ∈ 𝐵 ) )
14	13	eqrdv	⊢ ( 𝑀 ∈ Mnd → ( 𝑍 ‘ { 0 } ) = 𝐵 )