| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgnprfval.0 |
|- D = { 1 , 2 } |
| 2 |
|
psgnprfval.g |
|- G = ( SymGrp ` D ) |
| 3 |
|
psgnprfval.b |
|- B = ( Base ` G ) |
| 4 |
|
psgnprfval.t |
|- T = ran ( pmTrsp ` D ) |
| 5 |
|
psgnprfval.n |
|- N = ( pmSgn ` D ) |
| 6 |
|
prex |
|- { 1 , 2 } e. _V |
| 7 |
1 6
|
eqeltri |
|- D e. _V |
| 8 |
2
|
symgid |
|- ( D e. _V -> ( _I |` D ) = ( 0g ` G ) ) |
| 9 |
7 8
|
ax-mp |
|- ( _I |` D ) = ( 0g ` G ) |
| 10 |
9
|
gsum0 |
|- ( G gsum (/) ) = ( _I |` D ) |
| 11 |
|
reseq2 |
|- ( D = { 1 , 2 } -> ( _I |` D ) = ( _I |` { 1 , 2 } ) ) |
| 12 |
|
1ex |
|- 1 e. _V |
| 13 |
|
2nn |
|- 2 e. NN |
| 14 |
|
residpr |
|- ( ( 1 e. _V /\ 2 e. NN ) -> ( _I |` { 1 , 2 } ) = { <. 1 , 1 >. , <. 2 , 2 >. } ) |
| 15 |
12 13 14
|
mp2an |
|- ( _I |` { 1 , 2 } ) = { <. 1 , 1 >. , <. 2 , 2 >. } |
| 16 |
11 15
|
eqtrdi |
|- ( D = { 1 , 2 } -> ( _I |` D ) = { <. 1 , 1 >. , <. 2 , 2 >. } ) |
| 17 |
1 16
|
ax-mp |
|- ( _I |` D ) = { <. 1 , 1 >. , <. 2 , 2 >. } |
| 18 |
10 17
|
eqtr2i |
|- { <. 1 , 1 >. , <. 2 , 2 >. } = ( G gsum (/) ) |
| 19 |
18
|
fveq2i |
|- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = ( N ` ( G gsum (/) ) ) |
| 20 |
|
wrd0 |
|- (/) e. Word T |
| 21 |
2 4 5
|
psgnvalii |
|- ( ( D e. _V /\ (/) e. Word T ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) ) |
| 22 |
7 20 21
|
mp2an |
|- ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) |
| 23 |
|
hash0 |
|- ( # ` (/) ) = 0 |
| 24 |
23
|
oveq2i |
|- ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 ) |
| 25 |
|
neg1cn |
|- -u 1 e. CC |
| 26 |
|
exp0 |
|- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 ) |
| 27 |
25 26
|
ax-mp |
|- ( -u 1 ^ 0 ) = 1 |
| 28 |
24 27
|
eqtri |
|- ( -u 1 ^ ( # ` (/) ) ) = 1 |
| 29 |
19 22 28
|
3eqtri |
|- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 1 |