Theorem psgnprfval1

Description: The permutation sign of the identity for a pair. (Contributed by AV, 11-Dec-2018)

	Ref	Expression
Hypotheses	psgnprfval.0	⊢ 𝐷 = { 1 , 2 }
	psgnprfval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnprfval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	psgnprfval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnprfval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnprfval1	⊢ ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 1

Proof

Step	Hyp	Ref	Expression
1		psgnprfval.0	⊢ 𝐷 = { 1 , 2 }
2		psgnprfval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3		psgnprfval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		psgnprfval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
5		psgnprfval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
6		prex	⊢ { 1 , 2 } ∈ V
7	1 6	eqeltri	⊢ 𝐷 ∈ V
8	2	symgid	⊢ ( 𝐷 ∈ V → ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 ) )
9	7 8	ax-mp	⊢ ( I ↾ 𝐷 ) = ( 0g ‘ 𝐺 )
10	9	gsum0	⊢ ( 𝐺 Σg ∅ ) = ( I ↾ 𝐷 )
11		reseq2	⊢ ( 𝐷 = { 1 , 2 } → ( I ↾ 𝐷 ) = ( 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	⊢ ( 𝐷 = { 1 , 2 } → ( I ↾ 𝐷 ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
17	1 16	ax-mp	⊢ ( I ↾ 𝐷 ) = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ }
18	10 17	eqtr2i	⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = ( 𝐺 Σg ∅ )
19	18	fveq2i	⊢ ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = ( 𝑁 ‘ ( 𝐺 Σg ∅ ) )
20		wrd0	⊢ ∅ ∈ Word 𝑇
21	2 4 5	psgnvalii	⊢ ( ( 𝐷 ∈ V ∧ ∅ ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg ∅ ) ) = ( - 1 ↑ ( ♯ ‘ ∅ ) ) )
22	7 20 21	mp2an	⊢ ( 𝑁 ‘ ( 𝐺 Σ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	⊢ ( 𝑁 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 1