Metamath Proof Explorer


Theorem isnsg

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

Ref Expression
Hypotheses isnsg.1 X = Base G
isnsg.2 + ˙ = + G
Assertion isnsg S NrmSGrp G S SubGrp G x X y X x + ˙ y S y + ˙ x S

Proof

Step Hyp Ref Expression
1 isnsg.1 X = Base G
2 isnsg.2 + ˙ = + G
3 df-nsg NrmSGrp = g Grp s SubGrp g | [˙Base g / b]˙ [˙+ g / p]˙ x b y b x p y s y p x s
4 3 mptrcl S NrmSGrp G G Grp
5 subgrcl S SubGrp G G Grp
6 5 adantr S SubGrp G x X y X x + ˙ y S y + ˙ x S G Grp
7 fveq2 g = G SubGrp g = SubGrp G
8 fvexd g = G Base g V
9 fveq2 g = G Base g = Base G
10 9 1 eqtr4di g = G Base g = X
11 fvexd g = G b = X + g V
12 simpl g = G b = X g = G
13 12 fveq2d g = G b = X + g = + G
14 13 2 eqtr4di g = G b = X + g = + ˙
15 simplr g = G b = X p = + ˙ b = X
16 simpr g = G b = X p = + ˙ p = + ˙
17 16 oveqd g = G b = X p = + ˙ x p y = x + ˙ y
18 17 eleq1d g = G b = X p = + ˙ x p y s x + ˙ y s
19 16 oveqd g = G b = X p = + ˙ y p x = y + ˙ x
20 19 eleq1d g = G b = X p = + ˙ y p x s y + ˙ x s
21 18 20 bibi12d g = G b = X p = + ˙ x p y s y p x s x + ˙ y s y + ˙ x s
22 15 21 raleqbidv g = G b = X p = + ˙ y b x p y s y p x s y X x + ˙ y s y + ˙ x s
23 15 22 raleqbidv g = G b = X p = + ˙ x b y b x p y s y p x s x X y X x + ˙ y s y + ˙ x s
24 11 14 23 sbcied2 g = G b = X [˙+ g / p]˙ x b y b x p y s y p x s x X y X x + ˙ y s y + ˙ x s
25 8 10 24 sbcied2 g = G [˙Base g / b]˙ [˙+ g / p]˙ x b y b x p y s y p x s x X y X x + ˙ y s y + ˙ x s
26 7 25 rabeqbidv g = G s SubGrp g | [˙Base g / b]˙ [˙+ g / p]˙ x b y b x p y s y p x s = s SubGrp G | x X y X x + ˙ y s y + ˙ x s
27 fvex SubGrp G V
28 27 rabex s SubGrp G | x X y X x + ˙ y s y + ˙ x s V
29 26 3 28 fvmpt G Grp NrmSGrp G = s SubGrp G | x X y X x + ˙ y s y + ˙ x s
30 29 eleq2d G Grp S NrmSGrp G S s SubGrp G | x X y X x + ˙ y s y + ˙ x s
31 eleq2 s = S x + ˙ y s x + ˙ y S
32 eleq2 s = S y + ˙ x s y + ˙ x S
33 31 32 bibi12d s = S x + ˙ y s y + ˙ x s x + ˙ y S y + ˙ x S
34 33 2ralbidv s = S x X y X x + ˙ y s y + ˙ x s x X y X x + ˙ y S y + ˙ x S
35 34 elrab S s SubGrp G | x X y X x + ˙ y s y + ˙ x s S SubGrp G x X y X x + ˙ y S y + ˙ x S
36 30 35 bitrdi G Grp S NrmSGrp G S SubGrp G x X y X x + ˙ y S y + ˙ x S
37 4 6 36 pm5.21nii S NrmSGrp G S SubGrp G x X y X x + ˙ y S y + ˙ x S