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

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 ⊢ ( 0g ‘ ( SymGrp ‘ ∅ ) ) = ( 0g ‘ ( SymGrp ‘ ∅ ) )
4 3 gsum0 ⊢ ( ( SymGrp ‘ ∅ ) Σg ∅ ) = ( 0g ‘ ( SymGrp ‘ ∅ ) )
5 eqid ⊢ ( SymGrp ‘ ∅ ) = ( SymGrp ‘ ∅ )
6 5 symgid ⊢ ( ∅ ∈ V → ( I ↾ ∅ ) = ( 0g ‘ ( SymGrp ‘ ∅ ) ) )
7 1 6 ax-mp ⊢ ( I ↾ ∅ ) = ( 0g ‘ ( SymGrp ‘ ∅ ) )
8 res0 ⊢ ( I ↾ ∅ ) = ∅
9 7 8 eqtr3i ⊢ ( 0g ‘ ( SymGrp ‘ ∅ ) ) = ∅
10 9 a1i ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ Word ran ( pmTrsp ‘ ∅ ) ) → ( 0g ‘ ( SymGrp ‘ ∅ ) ) = ∅ )
11 4 10 eqtr2id ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ Word ran ( pmTrsp ‘ ∅ ) ) → ∅ = ( ( SymGrp ‘ ∅ ) Σg ∅ ) )
12 11 fveq2d ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ Word ran ( pmTrsp ‘ ∅ ) ) → ( ( pmSgn ‘ ∅ ) ‘ ∅ ) = ( ( pmSgn ‘ ∅ ) ‘ ( ( SymGrp ‘ ∅ ) Σg ∅ ) ) )
13 eqid ⊢ ran ( pmTrsp ‘ ∅ ) = ran ( pmTrsp ‘ ∅ )
14 eqid ⊢ ( pmSgn ‘ ∅ ) = ( pmSgn ‘ ∅ )
15 5 13 14 psgnvalii ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ Word ran ( pmTrsp ‘ ∅ ) ) → ( ( pmSgn ‘ ∅ ) ‘ ( ( SymGrp ‘ ∅ ) Σg ∅ ) ) = ( - 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