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 ⊢∅∈Wordran⁡pmTrsp⁡∅
3 eqid ⊢0SymGrp⁡∅=0SymGrp⁡∅
4 3 gsum0 ⊢∑SymGrp⁡∅∅=0SymGrp⁡∅
5 eqid ⊢SymGrp⁡∅=SymGrp⁡∅
6 5 symgid ⊢∅∈V→I↾∅=0SymGrp⁡∅
7 1 6 ax-mp ⊢I↾∅=0SymGrp⁡∅
8 res0 ⊢I↾∅=∅
9 7 8 eqtr3i ⊢0SymGrp⁡∅=∅
10 9 a1i ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→0SymGrp⁡∅=∅
11 4 10 eqtr2id ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→∅=∑SymGrp⁡∅∅
12 11 fveq2d ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→pmSgn⁡∅⁡∅=pmSgn⁡∅⁡∑SymGrp⁡∅∅
13 eqid ⊢ran⁡pmTrsp⁡∅=ran⁡pmTrsp⁡∅
14 eqid ⊢pmSgn⁡∅=pmSgn⁡∅
15 5 13 14 psgnvalii ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→pmSgn⁡∅⁡∑SymGrp⁡∅∅=−1∅
16 hash0 ⊢∅=0
17 16 oveq2i ⊢−1∅=−10
18 neg1cn ⊢−1∈ℂ
19 exp0 ⊢−1∈ℂ→−10=1
20 18 19 ax-mp ⊢−10=1
21 17 20 eqtri ⊢−1∅=1
22 21 a1i ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→−1∅=1
23 12 15 22 3eqtrd ⊢∅∈V∧∅∈Wordran⁡pmTrsp⁡∅→pmSgn⁡∅⁡∅=1
24 1 2 23 mp2an ⊢pmSgn⁡∅⁡∅=1