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

Metamath Proof Explorer

Theorem psgnran

Description: The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses psgnran.p 
|- P = ( Base ` ( SymGrp ` N ) )
psgnran.s 
|- S = ( pmSgn ` N )
Assertion psgnran 
|- ( ( N e. Fin /\ Q e. P ) -> ( S ` Q ) e. { 1 , -u 1 } )

Proof

Step Hyp Ref Expression
1 psgnran.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 psgnran.s 
 |-  S = ( pmSgn ` N )
3 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
4 3 1 sygbasnfpfi 
 |-  ( ( N e. Fin /\ Q e. P ) -> dom ( Q \ _I ) e. Fin )
5 4 ex 
 |-  ( N e. Fin -> ( Q e. P -> dom ( Q \ _I ) e. Fin ) )
6 5 pm4.71d 
 |-  ( N e. Fin -> ( Q e. P <-> ( Q e. P /\ dom ( Q \ _I ) e. Fin ) ) )
7 3 2 1 psgneldm 
 |-  ( Q e. dom S <-> ( Q e. P /\ dom ( Q \ _I ) e. Fin ) )
8 6 7 bitr4di 
 |-  ( N e. Fin -> ( Q e. P <-> Q e. dom S ) )
9 eqid 
 |-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
10 3 9 2 psgnvali 
 |-  ( Q e. dom S -> E. w e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum w ) /\ ( S ` Q ) = ( -u 1 ^ ( # ` w ) ) ) )
11 lencl 
 |-  ( w e. Word ran ( pmTrsp ` N ) -> ( # ` w ) e. NN0 )
12 11 nn0zd 
 |-  ( w e. Word ran ( pmTrsp ` N ) -> ( # ` w ) e. ZZ )
13 m1expcl2 
 |-  ( ( # ` w ) e. ZZ -> ( -u 1 ^ ( # ` w ) ) e. { -u 1 , 1 } )
14 prcom 
 |-  { -u 1 , 1 } = { 1 , -u 1 }
15 13 14 eleqtrdi 
 |-  ( ( # ` w ) e. ZZ -> ( -u 1 ^ ( # ` w ) ) e. { 1 , -u 1 } )
16 12 15 syl 
 |-  ( w e. Word ran ( pmTrsp ` N ) -> ( -u 1 ^ ( # ` w ) ) e. { 1 , -u 1 } )
17 16 adantl 
 |-  ( ( N e. Fin /\ w e. Word ran ( pmTrsp ` N ) ) -> ( -u 1 ^ ( # ` w ) ) e. { 1 , -u 1 } )
18 eleq1a 
 |-  ( ( -u 1 ^ ( # ` w ) ) e. { 1 , -u 1 } -> ( ( S ` Q ) = ( -u 1 ^ ( # ` w ) ) -> ( S ` Q ) e. { 1 , -u 1 } ) )
19 17 18 syl 
 |-  ( ( N e. Fin /\ w e. Word ran ( pmTrsp ` N ) ) -> ( ( S ` Q ) = ( -u 1 ^ ( # ` w ) ) -> ( S ` Q ) e. { 1 , -u 1 } ) )
20 19 adantld 
 |-  ( ( N e. Fin /\ w e. Word ran ( pmTrsp ` N ) ) -> ( ( Q = ( ( SymGrp ` N ) gsum w ) /\ ( S ` Q ) = ( -u 1 ^ ( # ` w ) ) ) -> ( S ` Q ) e. { 1 , -u 1 } ) )
21 20 rexlimdva 
 |-  ( N e. Fin -> ( E. w e. Word ran ( pmTrsp ` N ) ( Q = ( ( SymGrp ` N ) gsum w ) /\ ( S ` Q ) = ( -u 1 ^ ( # ` w ) ) ) -> ( S ` Q ) e. { 1 , -u 1 } ) )
22 10 21 syl5 
 |-  ( N e. Fin -> ( Q e. dom S -> ( S ` Q ) e. { 1 , -u 1 } ) )
23 8 22 sylbid 
 |-  ( N e. Fin -> ( Q e. P -> ( S ` Q ) e. { 1 , -u 1 } ) )
24 23 imp 
 |-  ( ( N e. Fin /\ Q e. P ) -> ( S ` Q ) e. { 1 , -u 1 } )