Theorem psgnprfval1

Description: The permutation sign of the identity for a pair. (Contributed by AV, 11-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	psgnprfval1	|- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 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 } e. _V
7	1 6	eqeltri	|- D e. _V
8	2	symgid	|- ( D e. _V -> ( _I |` D ) = ( 0g ` G ) )
9	7 8	ax-mp	|- ( _I |` D ) = ( 0g ` G )
10	9	gsum0	|- ( G gsum (/) ) = ( _I |` D )
11		reseq2	|- ( D = { 1 , 2 } -> ( _I |` D ) = ( _I |` { 1 , 2 } ) )
12		1ex	|- 1 e. _V
13		2nn	|- 2 e. NN
14		residpr	|- ( ( 1 e. _V /\ 2 e. NN ) -> ( _I |` { 1 , 2 } ) = { <. 1 , 1 >. , <. 2 , 2 >. } )
15	12 13 14	mp2an	|- ( _I |` { 1 , 2 } ) = { <. 1 , 1 >. , <. 2 , 2 >. }
16	11 15	eqtrdi	|- ( D = { 1 , 2 } -> ( _I |` D ) = { <. 1 , 1 >. , <. 2 , 2 >. } )
17	1 16	ax-mp	|- ( _I |` D ) = { <. 1 , 1 >. , <. 2 , 2 >. }
18	10 17	eqtr2i	|- { <. 1 , 1 >. , <. 2 , 2 >. } = ( G gsum (/) )
19	18	fveq2i	|- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = ( N ` ( G gsum (/) ) )
20		wrd0	|- (/) e. Word T
21	2 4 5	psgnvalii	|- ( ( D e. _V /\ (/) e. Word T ) -> ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) ) )
22	7 20 21	mp2an	|- ( N ` ( G gsum (/) ) ) = ( -u 1 ^ ( # ` (/) ) )
23		hash0	|- ( # ` (/) ) = 0
24	23	oveq2i	|- ( -u 1 ^ ( # ` (/) ) ) = ( -u 1 ^ 0 )
25		neg1cn	|- -u 1 e. CC
26		exp0	|- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
27	25 26	ax-mp	|- ( -u 1 ^ 0 ) = 1
28	24 27	eqtri	|- ( -u 1 ^ ( # ` (/) ) ) = 1
29	19 22 28	3eqtri	|- ( N ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 1