Theorem nsgbi

Description: Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	isnsg.1	|- X = ( Base ` G )
	isnsg.2	|- .+ = ( +g ` G )
Assertion	nsgbi	|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	|- X = ( Base ` G )
2		isnsg.2	|- .+ = ( +g ` G )
3	1 2	isnsg	|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) ) )
4	3	simprbi	|- ( S e. ( NrmSGrp ` G ) -> A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) )
5		oveq1	|- ( x = A -> ( x .+ y ) = ( A .+ y ) )
6	5	eleq1d	|- ( x = A -> ( ( x .+ y ) e. S <-> ( A .+ y ) e. S ) )
7		oveq2	|- ( x = A -> ( y .+ x ) = ( y .+ A ) )
8	7	eleq1d	|- ( x = A -> ( ( y .+ x ) e. S <-> ( y .+ A ) e. S ) )
9	6 8	bibi12d	|- ( x = A -> ( ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) <-> ( ( A .+ y ) e. S <-> ( y .+ A ) e. S ) ) )
10		oveq2	|- ( y = B -> ( A .+ y ) = ( A .+ B ) )
11	10	eleq1d	|- ( y = B -> ( ( A .+ y ) e. S <-> ( A .+ B ) e. S ) )
12		oveq1	|- ( y = B -> ( y .+ A ) = ( B .+ A ) )
13	12	eleq1d	|- ( y = B -> ( ( y .+ A ) e. S <-> ( B .+ A ) e. S ) )
14	11 13	bibi12d	|- ( y = B -> ( ( ( A .+ y ) e. S <-> ( y .+ A ) e. S ) <-> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) ) )
15	9 14	rspc2v	|- ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) ) )
16	4 15	syl5com	|- ( S e. ( NrmSGrp ` G ) -> ( ( A e. X /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) ) )
17	16	3impib	|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. X ) -> ( ( A .+ B ) e. S <-> ( B .+ A ) e. S ) )