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 T N P = 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 Base G
6 5 sseli P T P Base G
7 4 gsumws1 P Base G G ⟨“ P ”⟩ = P
8 6 7 syl P T G ⟨“ P ”⟩ = P
9 8 fveq2d P T N G ⟨“ P ”⟩ = N P
10 1 4 elbasfv P Base G D V
11 6 10 syl P T D V
12 s1cl P T ⟨“ P ”⟩ Word T
13 1 2 3 psgnvalii D V ⟨“ P ”⟩ Word T N G ⟨“ P ”⟩ = 1 ⟨“ P ”⟩
14 11 12 13 syl2anc P T N G ⟨“ P ”⟩ = 1 ⟨“ P ”⟩
15 s1len ⟨“ P ”⟩ = 1
16 15 oveq2i 1 ⟨“ P ”⟩ = 1 1
17 neg1cn 1
18 exp1 1 1 1 = 1
19 17 18 ax-mp 1 1 = 1
20 16 19 eqtri 1 ⟨“ P ”⟩ = 1
21 14 20 eqtrdi P T N G ⟨“ P ”⟩ = 1
22 9 21 eqtr3d P T N P = 1