Theorem elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
	cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	elcntzsn	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑋 ∈ ( 𝑍 ‘ { 𝑌 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
3		cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
4	1 2 3	cntzsnval	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } )
5	4	eleq2d	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑋 ∈ ( 𝑍 ‘ { 𝑌 } ) ↔ 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } ) )
6		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 + 𝑌 ) = ( 𝑋 + 𝑌 ) )
7		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑌 + 𝑥 ) = ( 𝑌 + 𝑋 ) )
8	6 7	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
9	8	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
10	5 9	bitrdi	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑋 ∈ ( 𝑍 ‘ { 𝑌 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) ) )