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