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 ) |