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	syl5req	⊢ ( ( ∅ ∈ 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