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 fndm N Fn x Base S | dom x I Fin dom N = x Base S | dom x I Fin
14 12 13 ax-mp dom N = x Base S | dom x I Fin
15 10 14 syl6eqr D Fin Base S = dom N
16 eqimss Base S = dom N Base S dom N
17 1 fvexi S V
18 2 fvexi N V
19 18 dmex dom N V
20 4 6 ressid2 Base S dom N S V dom N V S 𝑠 dom N = S
21 17 19 20 mp3an23 Base S dom N S 𝑠 dom N = S
22 15 16 21 3syl D Fin S 𝑠 dom N = S
23 22 oveq1d D Fin S 𝑠 dom N GrpHom U = S GrpHom U
24 5 23 eleqtrd D Fin N S GrpHom U