Metamath Proof Explorer


Theorem psgnpmtr

Description: All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015)

Ref Expression
Hypotheses psgnval.g
|- G = ( SymGrp ` D )
psgnval.t
|- T = ran ( pmTrsp ` D )
psgnval.n
|- N = ( pmSgn ` D )
Assertion psgnpmtr
|- ( P e. T -> ( N ` P ) = -u 1 )

Proof

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 )