Metamath Proof Explorer

Theorem psgnghm2

Description: The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnghm2.s ⊢ S = SymGrp ⁡ D
psgnghm2.n ⊢ N = pmSgn ⁡ D
psgnghm2.u ⊢ U = mulGrp ℂ fld ↾ 𝑠 1 − 1
Assertion psgnghm2 ⊢ D ∈ Fin → N ∈ S GrpHom U

Proof

Step Hyp Ref Expression
1 psgnghm2.s ⊢ S = SymGrp ⁡ D
2 psgnghm2.n ⊢ N = pmSgn ⁡ D
3 psgnghm2.u ⊢ U = mulGrp ℂ fld ↾ 𝑠 1 − 1
4 eqid ⊢ S ↾ 𝑠 dom ⁡ N = S ↾ 𝑠 dom ⁡ N
5 1 2 4 3 psgnghm ⊢ D ∈ Fin → N ∈ S ↾ 𝑠 dom ⁡ N GrpHom U
6 eqid ⊢ Base S = Base S
7 1 6 sygbasnfpfi ⊢ D ∈ Fin ∧ x ∈ Base S → dom ⁡ x ∖ I ∈ Fin
8 7 ralrimiva ⊢ D ∈ Fin → ∀ x ∈ Base S dom ⁡ x ∖ I ∈ Fin
9 rabid2 ⊢ Base S = x ∈ Base S | dom ⁡ x ∖ I ∈ Fin ↔ ∀ x ∈ Base S dom ⁡ x ∖ I ∈ Fin
10 8 9 sylibr ⊢ D ∈ Fin → Base S = x ∈ Base S | dom ⁡ x ∖ I ∈ Fin
11 eqid ⊢ x ∈ Base S | dom ⁡ x ∖ I ∈ Fin = x ∈ Base S | dom ⁡ x ∖ I ∈ Fin
12 1 6 11 2 psgnfn ⊢ N Fn x ∈ Base S | dom ⁡ x ∖ I ∈ Fin
13 12 fndmi ⊢ dom ⁡ N = x ∈ Base S | dom ⁡ x ∖ I ∈ Fin
14 10 13 eqtr4di ⊢ D ∈ Fin → Base S = dom ⁡ N
15 eqimss ⊢ Base S = dom ⁡ N → Base S ⊆ dom ⁡ N
16 1 fvexi ⊢ S ∈ V
17 2 fvexi ⊢ N ∈ V
18 17 dmex ⊢ dom ⁡ N ∈ V
19 4 6 ressid2 ⊢ Base S ⊆ dom ⁡ N ∧ S ∈ V ∧ dom ⁡ N ∈ V → S ↾ 𝑠 dom ⁡ N = S
20 16 18 19 mp3an23 ⊢ Base S ⊆ dom ⁡ N → S ↾ 𝑠 dom ⁡ N = S
21 14 15 20 3syl ⊢ D ∈ Fin → S ↾ 𝑠 dom ⁡ N = S
22 21 oveq1d ⊢ D ∈ Fin → S ↾ 𝑠 dom ⁡ N GrpHom U = S GrpHom U
23 5 22 eleqtrd ⊢ D ∈ Fin → N ∈ S GrpHom U