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

Metamath Proof Explorer

Theorem nmzbi

Description: Defining property of 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 nmzbi 
|- ( ( A e. N /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ 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 1 elnmz 
 |-  ( A e. N <-> ( A e. X /\ A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) ) )
3 2 simprbi 
 |-  ( A e. N -> A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) )
4 oveq2 
 |-  ( z = B -> ( A .+ z ) = ( A .+ B ) )
5 4 eleq1d 
 |-  ( z = B -> ( ( A .+ z ) e. S <-> ( A .+ B ) e. S ) )
6 oveq1 
 |-  ( z = B -> ( z .+ A ) = ( B .+ A ) )
7 6 eleq1d 
 |-  ( z = B -> ( ( z .+ A ) e. S <-> ( B .+ A ) e. S ) )
8 5 7 bibi12d 
 |-  ( z = B -> ( ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) <-> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) ) )
9 8 rspccva 
 |-  ( ( A. z e. X ( ( A .+ z ) e. S <-> ( z .+ A ) e. S ) /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )
10 3 9 sylan 
 |-  ( ( A e. N /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )