This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑍 ‘ { 𝑌 } ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 + 𝑌 ) = ( 𝑌 + 𝑥 ) } )