Metamath Proof Explorer

Theorem psgn0fv0

Description: The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019)

Ref Expression
Assertion psgn0fv0 ⊢ pmSgn ⁡ ∅ ⁡ ∅ = 1

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 wrd0 ⊢ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅
3 eqid ⊢ 0 SymGrp ⁡ ∅ = 0 SymGrp ⁡ ∅
4 3 gsum0 ⊢ ∑ SymGrp ⁡ ∅ ∅ = 0 SymGrp ⁡ ∅
5 eqid ⊢ SymGrp ⁡ ∅ = SymGrp ⁡ ∅
6 5 symgid ⊢ ∅ ∈ V → I ↾ ∅ = 0 SymGrp ⁡ ∅
7 1 6 ax-mp ⊢ I ↾ ∅ = 0 SymGrp ⁡ ∅
8 res0 ⊢ I ↾ ∅ = ∅
9 7 8 eqtr3i ⊢ 0 SymGrp ⁡ ∅ = ∅
10 9 a1i ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → 0 SymGrp ⁡ ∅ = ∅
11 4 10 syl5req ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → ∅ = ∑ SymGrp ⁡ ∅ ∅
12 11 fveq2d ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → pmSgn ⁡ ∅ ⁡ ∅ = pmSgn ⁡ ∅ ⁡ ∑ SymGrp ⁡ ∅ ∅
13 eqid ⊢ ran ⁡ pmTrsp ⁡ ∅ = ran ⁡ pmTrsp ⁡ ∅
14 eqid ⊢ pmSgn ⁡ ∅ = pmSgn ⁡ ∅
15 5 13 14 psgnvalii ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → pmSgn ⁡ ∅ ⁡ ∑ SymGrp ⁡ ∅ ∅ = − 1 ∅
16 hash0 ⊢ ∅ = 0
17 16 oveq2i ⊢ − 1 ∅ = − 1 0
18 neg1cn ⊢ − 1 ∈ ℂ
19 exp0 ⊢ − 1 ∈ ℂ → − 1 0 = 1
20 18 19 ax-mp ⊢ − 1 0 = 1
21 17 20 eqtri ⊢ − 1 ∅ = 1
22 21 a1i ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → − 1 ∅ = 1
23 12 15 22 3eqtrd ⊢ ∅ ∈ V ∧ ∅ ∈ Word ran ⁡ pmTrsp ⁡ ∅ → pmSgn ⁡ ∅ ⁡ ∅ = 1
24 1 2 23 mp2an ⊢ pmSgn ⁡ ∅ ⁡ ∅ = 1