Theorem psgnprfval2

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

	Ref	Expression
Hypotheses	psgnprfval.0	⊢ 𝐷 = { 1 , 2 }
	psgnprfval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnprfval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	psgnprfval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnprfval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnprfval2	⊢ ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 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 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
7	6	snid	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
8	1	fveq2i	⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ { 1 , 2 } )
9	8	rneqi	⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ { 1 , 2 } )
10		pmtrprfvalrn	⊢ ran ( pmTrsp ‘ { 1 , 2 } ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
11	9 10	eqtri	⊢ ran ( pmTrsp ‘ 𝐷 ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
12	7 11	eleqtrri	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ran ( pmTrsp ‘ 𝐷 )
13	12 4	eleqtrri	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑇
14	2 4 5	psgnpmtr	⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑇 → ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1 )
15	13 14	ax-mp	⊢ ( 𝑁 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1