This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psgnprfval2

Description: The permutation sign of the transposition for a pair. (Contributed by AV, 10-Dec-2018)

Ref Expression
Hypotheses psgnprfval.0 ⊢ D = 1 2
psgnprfval.g ⊢ G = SymGrp ⁡ D
psgnprfval.b ⊢ B = Base G
psgnprfval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnprfval.n ⊢ N = pmSgn ⁡ D
Assertion psgnprfval2 ⊢ N ⁡ 1 2 2 1 = − 1

Proof

Step Hyp Ref Expression
1 psgnprfval.0 ⊢ D = 1 2
2 psgnprfval.g ⊢ G = SymGrp ⁡ D
3 psgnprfval.b ⊢ B = Base G
4 psgnprfval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
5 psgnprfval.n ⊢ N = pmSgn ⁡ D
6 prex ⊢ 1 2 2 1 ∈ V
7 6 snid ⊢ 1 2 2 1 ∈ 1 2 2 1
8 1 fveq2i ⊢ pmTrsp ⁡ D = pmTrsp ⁡ 1 2
9 8 rneqi ⊢ ran ⁡ pmTrsp ⁡ D = ran ⁡ pmTrsp ⁡ 1 2
10 pmtrprfvalrn ⊢ ran ⁡ pmTrsp ⁡ 1 2 = 1 2 2 1
11 9 10 eqtri ⊢ ran ⁡ pmTrsp ⁡ D = 1 2 2 1
12 7 11 eleqtrri ⊢ 1 2 2 1 ∈ ran ⁡ pmTrsp ⁡ D
13 12 4 eleqtrri ⊢ 1 2 2 1 ∈ T
14 2 4 5 psgnpmtr ⊢ 1 2 2 1 ∈ T → N ⁡ 1 2 2 1 = − 1
15 13 14 ax-mp ⊢ N ⁡ 1 2 2 1 = − 1