Step |
Hyp |
Ref |
Expression |
0 |
|
cnsg |
⊢ NrmSGrp |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cgrp |
⊢ Grp |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
csubg |
⊢ SubGrp |
5 |
1
|
cv |
⊢ 𝑤 |
6 |
5 4
|
cfv |
⊢ ( SubGrp ‘ 𝑤 ) |
7 |
|
cbs |
⊢ Base |
8 |
5 7
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
9 |
|
vb |
⊢ 𝑏 |
10 |
|
cplusg |
⊢ +g |
11 |
5 10
|
cfv |
⊢ ( +g ‘ 𝑤 ) |
12 |
|
vp |
⊢ 𝑝 |
13 |
|
vx |
⊢ 𝑥 |
14 |
9
|
cv |
⊢ 𝑏 |
15 |
|
vy |
⊢ 𝑦 |
16 |
13
|
cv |
⊢ 𝑥 |
17 |
12
|
cv |
⊢ 𝑝 |
18 |
15
|
cv |
⊢ 𝑦 |
19 |
16 18 17
|
co |
⊢ ( 𝑥 𝑝 𝑦 ) |
20 |
3
|
cv |
⊢ 𝑠 |
21 |
19 20
|
wcel |
⊢ ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 |
22 |
18 16 17
|
co |
⊢ ( 𝑦 𝑝 𝑥 ) |
23 |
22 20
|
wcel |
⊢ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 |
24 |
21 23
|
wb |
⊢ ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) |
25 |
24 15 14
|
wral |
⊢ ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) |
26 |
25 13 14
|
wral |
⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) |
27 |
26 12 11
|
wsbc |
⊢ [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) |
28 |
27 9 8
|
wsbc |
⊢ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) |
29 |
28 3 6
|
crab |
⊢ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } |
30 |
1 2 29
|
cmpt |
⊢ ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } ) |
31 |
0 30
|
wceq |
⊢ NrmSGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } ) |