| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgnval.g |
|- G = ( SymGrp ` D ) |
| 2 |
|
psgnval.t |
|- T = ran ( pmTrsp ` D ) |
| 3 |
|
psgnval.n |
|- N = ( pmSgn ` D ) |
| 4 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
| 5 |
2 1 4
|
symgtrf |
|- T C_ ( Base ` G ) |
| 6 |
5
|
sseli |
|- ( P e. T -> P e. ( Base ` G ) ) |
| 7 |
4
|
gsumws1 |
|- ( P e. ( Base ` G ) -> ( G gsum <" P "> ) = P ) |
| 8 |
6 7
|
syl |
|- ( P e. T -> ( G gsum <" P "> ) = P ) |
| 9 |
8
|
fveq2d |
|- ( P e. T -> ( N ` ( G gsum <" P "> ) ) = ( N ` P ) ) |
| 10 |
1 4
|
elbasfv |
|- ( P e. ( Base ` G ) -> D e. _V ) |
| 11 |
6 10
|
syl |
|- ( P e. T -> D e. _V ) |
| 12 |
|
s1cl |
|- ( P e. T -> <" P "> e. Word T ) |
| 13 |
1 2 3
|
psgnvalii |
|- ( ( D e. _V /\ <" P "> e. Word T ) -> ( N ` ( G gsum <" P "> ) ) = ( -u 1 ^ ( # ` <" P "> ) ) ) |
| 14 |
11 12 13
|
syl2anc |
|- ( P e. T -> ( N ` ( G gsum <" P "> ) ) = ( -u 1 ^ ( # ` <" P "> ) ) ) |
| 15 |
|
s1len |
|- ( # ` <" P "> ) = 1 |
| 16 |
15
|
oveq2i |
|- ( -u 1 ^ ( # ` <" P "> ) ) = ( -u 1 ^ 1 ) |
| 17 |
|
neg1cn |
|- -u 1 e. CC |
| 18 |
|
exp1 |
|- ( -u 1 e. CC -> ( -u 1 ^ 1 ) = -u 1 ) |
| 19 |
17 18
|
ax-mp |
|- ( -u 1 ^ 1 ) = -u 1 |
| 20 |
16 19
|
eqtri |
|- ( -u 1 ^ ( # ` <" P "> ) ) = -u 1 |
| 21 |
14 20
|
eqtrdi |
|- ( P e. T -> ( N ` ( G gsum <" P "> ) ) = -u 1 ) |
| 22 |
9 21
|
eqtr3d |
|- ( P e. T -> ( N ` P ) = -u 1 ) |