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