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

Metamath Proof Explorer

Theorem elnmz

Description: Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypothesis elnmz.1 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
Assertion elnmz 
|- ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
2 oveq2 
 |-  ( y = z -> ( x .+ y ) = ( x .+ z ) )
3 2 eleq1d 
 |-  ( y = z -> ( ( x .+ y ) e. S <-> ( x .+ z ) e. S ) )
4 oveq1 
 |-  ( y = z -> ( y .+ x ) = ( z .+ x ) )
5 4 eleq1d 
 |-  ( y = z -> ( ( y .+ x ) e. S <-> ( z .+ x ) e. S ) )
6 3 5 bibi12d 
 |-  ( y = z -> ( ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) ) )
7 6 cbvralvw 
 |-  ( A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) )
8 oveq1 
 |-  ( x = A -> ( x .+ z ) = ( A .+ z ) )
9 8 eleq1d 
 |-  ( x = A -> ( ( x .+ z ) e. S <-> ( A .+ z ) e. S ) )
10 oveq2 
 |-  ( x = A -> ( z .+ x ) = ( z .+ A ) )
11 10 eleq1d 
 |-  ( x = A -> ( ( z .+ x ) e. S <-> ( z .+ A ) e. S ) )
12 9 11 bibi12d 
 |-  ( x = A -> ( ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )
13 12 ralbidv 
 |-  ( x = A -> ( A. z e. X ( ( x .+ z ) e. S <-> ( z .+ x ) e. S ) <-> A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )
14 7 13 bitrid 
 |-  ( x = A -> ( A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )
15 14 1 elrab2 
 |-  ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )