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

Metamath Proof Explorer

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