Step |
Hyp |
Ref |
Expression |
0 |
|
cnsg |
|- NrmSGrp |
1 |
|
vw |
|- w |
2 |
|
cgrp |
|- Grp |
3 |
|
vs |
|- s |
4 |
|
csubg |
|- SubGrp |
5 |
1
|
cv |
|- w |
6 |
5 4
|
cfv |
|- ( SubGrp ` w ) |
7 |
|
cbs |
|- Base |
8 |
5 7
|
cfv |
|- ( Base ` w ) |
9 |
|
vb |
|- b |
10 |
|
cplusg |
|- +g |
11 |
5 10
|
cfv |
|- ( +g ` w ) |
12 |
|
vp |
|- p |
13 |
|
vx |
|- x |
14 |
9
|
cv |
|- b |
15 |
|
vy |
|- y |
16 |
13
|
cv |
|- x |
17 |
12
|
cv |
|- p |
18 |
15
|
cv |
|- y |
19 |
16 18 17
|
co |
|- ( x p y ) |
20 |
3
|
cv |
|- s |
21 |
19 20
|
wcel |
|- ( x p y ) e. s |
22 |
18 16 17
|
co |
|- ( y p x ) |
23 |
22 20
|
wcel |
|- ( y p x ) e. s |
24 |
21 23
|
wb |
|- ( ( x p y ) e. s <-> ( y p x ) e. s ) |
25 |
24 15 14
|
wral |
|- A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) |
26 |
25 13 14
|
wral |
|- A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) |
27 |
26 12 11
|
wsbc |
|- [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) |
28 |
27 9 8
|
wsbc |
|- [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) |
29 |
28 3 6
|
crab |
|- { s e. ( SubGrp ` w ) | [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } |
30 |
1 2 29
|
cmpt |
|- ( w e. Grp |-> { s e. ( SubGrp ` w ) | [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } ) |
31 |
0 30
|
wceq |
|- NrmSGrp = ( w e. Grp |-> { s e. ( SubGrp ` w ) | [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } ) |