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

Metamath Proof Explorer

Theorem psgnprfval1

Description: The permutation sign of the identity for a pair. (Contributed by AV, 11-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 psgnprfval1 ⊢ N ⁡ 1 1 2 2 = 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 ∈ V
7 1 6 eqeltri ⊢ D ∈ V
8 2 symgid ⊢ D ∈ V → I ↾ D = 0 G
9 7 8 ax-mp ⊢ I ↾ D = 0 G
10 9 gsum0 ⊢ ∑ G ∅ = I ↾ D
11 reseq2 ⊢ D = 1 2 → I ↾ D = I ↾ 1 2
12 1ex ⊢ 1 ∈ V
13 2nn ⊢ 2 ∈ ℕ
14 residpr ⊢ 1 ∈ V ∧ 2 ∈ ℕ → I ↾ 1 2 = 1 1 2 2
15 12 13 14 mp2an ⊢ I ↾ 1 2 = 1 1 2 2
16 11 15 eqtrdi ⊢ D = 1 2 → I ↾ D = 1 1 2 2
17 1 16 ax-mp ⊢ I ↾ D = 1 1 2 2
18 10 17 eqtr2i ⊢ 1 1 2 2 = ∑ G ∅
19 18 fveq2i ⊢ N ⁡ 1 1 2 2 = N ⁡ ∑ G ∅
20 wrd0 ⊢ ∅ ∈ Word T
21 2 4 5 psgnvalii ⊢ D ∈ V ∧ ∅ ∈ Word T → N ⁡ ∑ G ∅ = − 1 ∅
22 7 20 21 mp2an ⊢ N ⁡ ∑ G ∅ = − 1 ∅
23 hash0 ⊢ ∅ = 0
24 23 oveq2i ⊢ − 1 ∅ = − 1 0
25 neg1cn ⊢ − 1 ∈ ℂ
26 exp0 ⊢ − 1 ∈ ℂ → − 1 0 = 1
27 25 26 ax-mp ⊢ − 1 0 = 1
28 24 27 eqtri ⊢ − 1 ∅ = 1
29 19 22 28 3eqtri ⊢ N ⁡ 1 1 2 2 = 1