Theorem psgnprfval2

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

	Ref	Expression
Hypotheses	psgnprfval.0	|- D = { 1 , 2 }
	psgnprfval.g	|- G = ( SymGrp ` D )
	psgnprfval.b	|- B = ( Base ` G )
	psgnprfval.t	|- T = ran ( pmTrsp ` D )
	psgnprfval.n	|- N = ( pmSgn ` D )
Assertion	psgnprfval2	|- ( N ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1

Proof

Step	Hyp	Ref	Expression
1		psgnprfval.0	|- D = { 1 , 2 }
2		psgnprfval.g	|- G = ( SymGrp ` D )
3		psgnprfval.b	|- B = ( Base ` G )
4		psgnprfval.t	|- T = ran ( pmTrsp ` D )
5		psgnprfval.n	|- N = ( pmSgn ` D )
6		prex	|- { <. 1 , 2 >. , <. 2 , 1 >. } e. _V
7	6	snid	|- { <. 1 , 2 >. , <. 2 , 1 >. } e. { { <. 1 , 2 >. , <. 2 , 1 >. } }
8	1	fveq2i	|- ( pmTrsp ` D ) = ( pmTrsp ` { 1 , 2 } )
9	8	rneqi	|- ran ( pmTrsp ` D ) = ran ( pmTrsp ` { 1 , 2 } )
10		pmtrprfvalrn	|- ran ( pmTrsp ` { 1 , 2 } ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }
11	9 10	eqtri	|- ran ( pmTrsp ` D ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }
12	7 11	eleqtrri	|- { <. 1 , 2 >. , <. 2 , 1 >. } e. ran ( pmTrsp ` D )
13	12 4	eleqtrri	|- { <. 1 , 2 >. , <. 2 , 1 >. } e. T
14	2 4 5	psgnpmtr	|- ( { <. 1 , 2 >. , <. 2 , 1 >. } e. T -> ( N ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1 )
15	13 14	ax-mp	|- ( N ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1