Theorem sscntz

Description: A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	|- B = ( Base ` M )
	cntzfval.p	|- .+ = ( +g ` M )
	cntzfval.z	|- Z = ( Cntz ` M )
Assertion	sscntz	|- ( ( S C_ B /\ T C_ B ) -> ( S C_ ( Z ` T ) <-> A. x e. S A. y e. T ( 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	cntzval	|- ( T C_ B -> ( Z ` T ) = { x e. B | A. y e. T ( x .+ y ) = ( y .+ x ) } )
5	4	sseq2d	|- ( T C_ B -> ( S C_ ( Z ` T ) <-> S C_ { x e. B | A. y e. T ( x .+ y ) = ( y .+ x ) } ) )
6		ssrab	|- ( S C_ { x e. B | A. y e. T ( x .+ y ) = ( y .+ x ) } <-> ( S C_ B /\ A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) )
7	5 6	bitrdi	|- ( T C_ B -> ( S C_ ( Z ` T ) <-> ( S C_ B /\ A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) ) )
8		ibar	|- ( S C_ B -> ( A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) <-> ( S C_ B /\ A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) ) )
9	8	bicomd	|- ( S C_ B -> ( ( S C_ B /\ A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) <-> A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) )
10	7 9	sylan9bbr	|- ( ( S C_ B /\ T C_ B ) -> ( S C_ ( Z ` T ) <-> A. x e. S A. y e. T ( x .+ y ) = ( y .+ x ) ) )