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

Metamath Proof Explorer

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