Theorem elcntz

Description: Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015)

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

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	cntzval	|- ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
5	4	eleq2d	|- ( S C_ B -> ( A e. ( Z ` S ) <-> A e. { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } ) )
6		oveq1	|- ( x = A -> ( x .+ y ) = ( A .+ y ) )
7		oveq2	|- ( x = A -> ( y .+ x ) = ( y .+ A ) )
8	6 7	eqeq12d	|- ( x = A -> ( ( x .+ y ) = ( y .+ x ) <-> ( A .+ y ) = ( y .+ A ) ) )
9	8	ralbidv	|- ( x = A -> ( A. y e. S ( x .+ y ) = ( y .+ x ) <-> A. y e. S ( A .+ y ) = ( y .+ A ) ) )
10	9	elrab	|- ( A e. { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } <-> ( A e. B /\ A. y e. S ( A .+ y ) = ( y .+ A ) ) )
11	5 10	bitrdi	|- ( S C_ B -> ( A e. ( Z ` S ) <-> ( A e. B /\ A. y e. S ( A .+ y ) = ( y .+ A ) ) ) )