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