Theorem cntri

Description: Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	cntri.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	cntri.p	⊢ + = ( +g ‘ 𝑀 )
	cntri.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
Assertion	cntri	⊢ ( ( 𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cntri.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		cntri.p	⊢ + = ( +g ‘ 𝑀 )
3		cntri.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
4		eqid	⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
5	1 4	cntrval	⊢ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )
6	3 5	eqtr4i	⊢ 𝑍 = ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 )
7	6	eleq2i	⊢ ( 𝑋 ∈ 𝑍 ↔ 𝑋 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) )
8	2 4	cntzi	⊢ ( ( 𝑋 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
9	7 8	sylanb	⊢ ( ( 𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )