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 |