Metamath Proof Explorer

Theorem psgnprfval

Description: The permutation sign function 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 psgnprfval 
|- ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )

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 id 
 |-  ( X e. B -> X e. B )
7 elpri 
 |-  ( X e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> ( X = { <. 1 , 1 >. , <. 2 , 2 >. } \/ X = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
8 prfi 
 |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. Fin
9 eleq1 
 |-  ( X = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( X e. Fin <-> { <. 1 , 1 >. , <. 2 , 2 >. } e. Fin ) )
10 8 9 mpbiri 
 |-  ( X = { <. 1 , 1 >. , <. 2 , 2 >. } -> X e. Fin )
11 prfi 
 |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. Fin
12 eleq1 
 |-  ( X = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( X e. Fin <-> { <. 1 , 2 >. , <. 2 , 1 >. } e. Fin ) )
13 11 12 mpbiri 
 |-  ( X = { <. 1 , 2 >. , <. 2 , 1 >. } -> X e. Fin )
14 10 13 jaoi 
 |-  ( ( X = { <. 1 , 1 >. , <. 2 , 2 >. } \/ X = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> X e. Fin )
15 diffi 
 |-  ( X e. Fin -> ( X \ _I ) e. Fin )
16 14 15 syl 
 |-  ( ( X = { <. 1 , 1 >. , <. 2 , 2 >. } \/ X = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( X \ _I ) e. Fin )
17 dmfi 
 |-  ( ( X \ _I ) e. Fin -> dom ( X \ _I ) e. Fin )
18 7 16 17 3syl 
 |-  ( X e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> dom ( X \ _I ) e. Fin )
19 1ex 
 |-  1 e. _V
20 2nn 
 |-  2 e. NN
21 2 3 1 symg2bas 
 |-  ( ( 1 e. _V /\ 2 e. NN ) -> B = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )
22 19 20 21 mp2an 
 |-  B = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }
23 18 22 eleq2s 
 |-  ( X e. B -> dom ( X \ _I ) e. Fin )
24 2 5 3 psgneldm 
 |-  ( X e. dom N <-> ( X e. B /\ dom ( X \ _I ) e. Fin ) )
25 6 23 24 sylanbrc 
 |-  ( X e. B -> X e. dom N )
26 2 4 5 psgnval 
 |-  ( X e. dom N -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
27 25 26 syl 
 |-  ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
28 6 27 syl 
 |-  ( X e. B -> ( N ` X ) = ( iota s E. w e. Word T ( X = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )