Theorem cntzel

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

	Ref	Expression
Hypotheses	cntzfval.b	|- B = ( Base ` M )
	cntzfval.p	|- .+ = ( +g ` M )
	cntzfval.z	|- Z = ( Cntz ` M )
Assertion	cntzel	|- ( ( S C_ B /\ X e. B ) -> ( X e. ( Z ` S ) <-> A. y e. S ( X .+ y ) = ( y .+ X ) ) )

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	|- B = ( Base ` M )
2		cntzfval.p	|- .+ = ( +g ` M )
3		cntzfval.z	|- Z = ( Cntz ` M )
4	1 2 3	elcntz	|- ( S C_ B -> ( X e. ( Z ` S ) <-> ( X e. B /\ A. y e. S ( X .+ y ) = ( y .+ X ) ) ) )
5	4	baibd	|- ( ( S C_ B /\ X e. B ) -> ( X e. ( Z ` S ) <-> A. y e. S ( X .+ y ) = ( y .+ X ) ) )