Theorem cntzsnval

Description: Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
	cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion	cntzsnval	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntzfval.p	⊢ + = ( +g ‘ 𝑀 )
3		cntzfval.z	⊢ 𝑍 = ( Cntz ‘ 𝑀 )
4		snssi	⊢ ( 𝑌 ∈ 𝐵 → { 𝑌 } ⊆ 𝐵 )
5	1 2 3	cntzval	⊢ ( { 𝑌 } ⊆ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ { 𝑌 } ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
6	4 5	syl	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ { 𝑌 } ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
7		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑌 ) )
8		oveq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 + 𝑥 ) = ( 𝑌 + 𝑥 ) )
9	7 8	eqeq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) ) )
10	9	ralsng	⊢ ( 𝑌 ∈ 𝐵 → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ↔ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) ) )
11	10	rabbidv	⊢ ( 𝑌 ∈ 𝐵 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ { 𝑌 } ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } )
12	6 11	eqtrd	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } )