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 ` M )
	cntzi.z	|- Z = ( Cntz ` M )
Assertion	cntzi	|- ( ( X e. ( Z ` S ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step	Hyp	Ref	Expression
1		cntzi.p	|- .+ = ( +g ` M )
2		cntzi.z	|- Z = ( Cntz ` M )
3		eqid	|- ( Base ` M ) = ( Base ` M )
4	3 2	cntzrcl	|- ( X e. ( Z ` S ) -> ( M e. _V /\ S C_ ( Base ` M ) ) )
5	3 1 2	elcntz	|- ( S C_ ( Base ` M ) -> ( X e. ( Z ` S ) <-> ( X e. ( Base ` M ) /\ A. y e. S ( X .+ y ) = ( y .+ X ) ) ) )
6	4 5	simpl2im	|- ( X e. ( Z ` S ) -> ( X e. ( Z ` S ) <-> ( X e. ( Base ` M ) /\ A. y e. S ( X .+ y ) = ( y .+ X ) ) ) )
7	6	simplbda	|- ( ( X e. ( Z ` S ) /\ X e. ( Z ` S ) ) -> A. y e. S ( X .+ y ) = ( y .+ X ) )
8	7	anidms	|- ( X e. ( Z ` S ) -> A. y e. S ( X .+ y ) = ( y .+ X ) )
9		oveq2	|- ( y = Y -> ( X .+ y ) = ( X .+ Y ) )
10		oveq1	|- ( y = Y -> ( y .+ X ) = ( Y .+ X ) )
11	9 10	eqeq12d	|- ( y = Y -> ( ( X .+ y ) = ( y .+ X ) <-> ( X .+ Y ) = ( Y .+ X ) ) )
12	11	rspccva	|- ( ( A. y e. S ( X .+ y ) = ( y .+ X ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) )
13	8 12	sylan	|- ( ( X e. ( Z ` S ) /\ Y e. S ) -> ( X .+ Y ) = ( Y .+ X ) )