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

Metamath Proof Explorer

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