Metamath Proof Explorer


Theorem isnsg

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

Ref Expression
Hypotheses isnsg.1 𝑋 = ( Base ‘ 𝐺 )
isnsg.2 + = ( +g𝐺 )
Assertion isnsg ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isnsg.1 𝑋 = ( Base ‘ 𝐺 )
2 isnsg.2 + = ( +g𝐺 )
3 df-nsg NrmSGrp = ( 𝑔 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑔 ) ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑝 ]𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } )
4 3 mptrcl ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
6 5 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) → 𝐺 ∈ Grp )
7 fveq2 ( 𝑔 = 𝐺 → ( SubGrp ‘ 𝑔 ) = ( SubGrp ‘ 𝐺 ) )
8 fvexd ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) ∈ V )
9 fveq2 ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
10 9 1 eqtr4di ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑋 )
11 fvexd ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) → ( +g𝑔 ) ∈ V )
12 simpl ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) → 𝑔 = 𝐺 )
13 12 fveq2d ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) → ( +g𝑔 ) = ( +g𝐺 ) )
14 13 2 eqtr4di ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) → ( +g𝑔 ) = + )
15 simplr ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → 𝑏 = 𝑋 )
16 simpr ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → 𝑝 = + )
17 16 oveqd ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( 𝑥 𝑝 𝑦 ) = ( 𝑥 + 𝑦 ) )
18 17 eleq1d ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑠 ) )
19 16 oveqd ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( 𝑦 𝑝 𝑥 ) = ( 𝑦 + 𝑥 ) )
20 19 eleq1d ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) )
21 18 20 bibi12d ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ) )
22 15 21 raleqbidv ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( ∀ 𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) ↔ ∀ 𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ) )
23 15 22 raleqbidv ( ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) ∧ 𝑝 = + ) → ( ∀ 𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ) )
24 11 14 23 sbcied2 ( ( 𝑔 = 𝐺𝑏 = 𝑋 ) → ( [ ( +g𝑔 ) / 𝑝 ]𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ) )
25 8 10 24 sbcied2 ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑝 ]𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ) )
26 7 25 rabeqbidv ( 𝑔 = 𝐺 → { 𝑠 ∈ ( SubGrp ‘ 𝑔 ) ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑝 ]𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } = { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) } )
27 fvex ( SubGrp ‘ 𝐺 ) ∈ V
28 27 rabex { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) } ∈ V
29 26 3 28 fvmpt ( 𝐺 ∈ Grp → ( NrmSGrp ‘ 𝐺 ) = { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) } )
30 29 eleq2d ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑆 ∈ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) } ) )
31 eleq2 ( 𝑠 = 𝑆 → ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
32 eleq2 ( 𝑠 = 𝑆 → ( ( 𝑦 + 𝑥 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
33 31 32 bibi12d ( 𝑠 = 𝑆 → ( ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
34 33 2ralbidv ( 𝑠 = 𝑆 → ( ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) ↔ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
35 34 elrab ( 𝑆 ∈ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑠 ) } ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
36 30 35 bitrdi ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) ) )
37 4 6 36 pm5.21nii ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )