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 ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
psgnran.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
Assertion psgnran ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )

Proof

Step Hyp Ref Expression
1 psgnran.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 psgnran.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
4 3 1 sygbasnfpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → dom ( 𝑄 ∖ I ) ∈ Fin )
5 4 ex ⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝑃 → dom ( 𝑄 ∖ I ) ∈ Fin ) )
6 5 pm4.71d ⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝑃 ↔ ( 𝑄 ∈ 𝑃 ∧ dom ( 𝑄 ∖ I ) ∈ Fin ) ) )
7 3 2 1 psgneldm ⊢ ( 𝑄 ∈ dom 𝑆 ↔ ( 𝑄 ∈ 𝑃 ∧ dom ( 𝑄 ∖ I ) ∈ Fin ) )
8 6 7 bitr4di ⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝑃 ↔ 𝑄 ∈ dom 𝑆 ) )
9 eqid ⊢ ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
10 3 9 2 psgnvali ⊢ ( 𝑄 ∈ dom 𝑆 → ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑤 ) ∧ ( 𝑆 ‘ 𝑄 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
11 lencl ⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) → ( ♯ ‘ 𝑤 ) ∈ ℕ0 )
12 11 nn0zd ⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) → ( ♯ ‘ 𝑤 ) ∈ ℤ )
13 m1expcl2 ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ { - 1 , 1 } )
14 prcom ⊢ { - 1 , 1 } = { 1 , - 1 }
15 13 14 eleqtrdi ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℤ → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ { 1 , - 1 } )
16 12 15 syl ⊢ ( 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ { 1 , - 1 } )
17 16 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ { 1 , - 1 } )
18 eleq1a ⊢ ( ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ∈ { 1 , - 1 } → ( ( 𝑆 ‘ 𝑄 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
19 17 18 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑄 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
20 19 adantld ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ) → ( ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑤 ) ∧ ( 𝑆 ‘ 𝑄 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
21 20 rexlimdva ⊢ ( 𝑁 ∈ Fin → ( ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑁 ) ( 𝑄 = ( ( SymGrp ‘ 𝑁 ) Σg 𝑤 ) ∧ ( 𝑆 ‘ 𝑄 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
22 10 21 syl5 ⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ dom 𝑆 → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
23 8 22 sylbid ⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝑃 → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } ) )
24 23 imp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )