This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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