This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )