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