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 )