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 ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )