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
Assertion nsgbi S NrmSGrp G A X B X A + ˙ B S B + ˙ A S

Proof

Step Hyp Ref Expression
1 isnsg.1 X = Base G
2 isnsg.2 + ˙ = + G
3 1 2 isnsg S NrmSGrp G S SubGrp G x X y X x + ˙ y S y + ˙ x S
4 3 simprbi S NrmSGrp G x X y X x + ˙ y S y + ˙ x S
5 oveq1 x = A x + ˙ y = A + ˙ y
6 5 eleq1d x = A x + ˙ y S A + ˙ y S
7 oveq2 x = A y + ˙ x = y + ˙ A
8 7 eleq1d x = A y + ˙ x S y + ˙ A S
9 6 8 bibi12d x = A x + ˙ y S y + ˙ x S A + ˙ y S y + ˙ A S
10 oveq2 y = B A + ˙ y = A + ˙ B
11 10 eleq1d y = B A + ˙ y S A + ˙ B S
12 oveq1 y = B y + ˙ A = B + ˙ A
13 12 eleq1d y = B y + ˙ A S B + ˙ A S
14 11 13 bibi12d y = B A + ˙ y S y + ˙ A S A + ˙ B S B + ˙ A S
15 9 14 rspc2v A X B X x X y X x + ˙ y S y + ˙ x S A + ˙ B S B + ˙ A S
16 4 15 syl5com S NrmSGrp G A X B X A + ˙ B S B + ˙ A S
17 16 3impib S NrmSGrp G A X B X A + ˙ B S B + ˙ A S