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

Metamath Proof Explorer

Theorem cntzi

Description: Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses cntzi.p ⊢ + = ( +g ‘ 𝑀 )
cntzi.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzi ( ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cntzi.p ⊢ + = ( +g ‘ 𝑀 )
2 cntzi.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4 3 2 cntzrcl ⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑀 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) )
5 3 1 2 elcntz ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) ) ) )
6 4 5 simpl2im ⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) ) ) )
7 6 simplbda ⊢ ( ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ) → ∀ 𝑦 ∈ 𝑆 ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) )
8 7 anidms ⊢ ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) )
9 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
10 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 + 𝑋 ) = ( 𝑌 + 𝑋 ) )
11 9 10 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) ↔ ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) )
12 11 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 + 𝑦 ) = ( 𝑦 + 𝑋 ) ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
13 8 12 sylan ⊢ ( ( 𝑋 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )