Metamath Proof Explorer


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