# 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}=\mathrm{SymGrp}\left({D}\right)$
psgnghm2.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
psgnghm2.u ${⊢}{U}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}$
Assertion psgnghm2 ${⊢}{D}\in \mathrm{Fin}\to {N}\in \left({S}\mathrm{GrpHom}{U}\right)$

### Proof

Step Hyp Ref Expression
1 psgnghm2.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
2 psgnghm2.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
3 psgnghm2.u ${⊢}{U}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left\{1,-1\right\}$
4 eqid ${⊢}{S}{↾}_{𝑠}\mathrm{dom}{N}={S}{↾}_{𝑠}\mathrm{dom}{N}$
5 1 2 4 3 psgnghm ${⊢}{D}\in \mathrm{Fin}\to {N}\in \left(\left({S}{↾}_{𝑠}\mathrm{dom}{N}\right)\mathrm{GrpHom}{U}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
7 1 6 sygbasnfpfi ${⊢}\left({D}\in \mathrm{Fin}\wedge {x}\in {\mathrm{Base}}_{{S}}\right)\to \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
8 7 ralrimiva ${⊢}{D}\in \mathrm{Fin}\to \forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
9 rabid2 ${⊢}{\mathrm{Base}}_{{S}}=\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}↔\forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
10 8 9 sylibr ${⊢}{D}\in \mathrm{Fin}\to {\mathrm{Base}}_{{S}}=\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
11 eqid ${⊢}\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}=\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
12 1 6 11 2 psgnfn ${⊢}{N}Fn\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
13 fndm ${⊢}{N}Fn\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}\to \mathrm{dom}{N}=\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
14 12 13 ax-mp ${⊢}\mathrm{dom}{N}=\left\{{x}\in {\mathrm{Base}}_{{S}}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
15 10 14 syl6eqr ${⊢}{D}\in \mathrm{Fin}\to {\mathrm{Base}}_{{S}}=\mathrm{dom}{N}$
16 eqimss ${⊢}{\mathrm{Base}}_{{S}}=\mathrm{dom}{N}\to {\mathrm{Base}}_{{S}}\subseteq \mathrm{dom}{N}$
17 1 fvexi ${⊢}{S}\in \mathrm{V}$
18 2 fvexi ${⊢}{N}\in \mathrm{V}$
19 18 dmex ${⊢}\mathrm{dom}{N}\in \mathrm{V}$
20 4 6 ressid2 ${⊢}\left({\mathrm{Base}}_{{S}}\subseteq \mathrm{dom}{N}\wedge {S}\in \mathrm{V}\wedge \mathrm{dom}{N}\in \mathrm{V}\right)\to {S}{↾}_{𝑠}\mathrm{dom}{N}={S}$
21 17 19 20 mp3an23 ${⊢}{\mathrm{Base}}_{{S}}\subseteq \mathrm{dom}{N}\to {S}{↾}_{𝑠}\mathrm{dom}{N}={S}$
22 15 16 21 3syl ${⊢}{D}\in \mathrm{Fin}\to {S}{↾}_{𝑠}\mathrm{dom}{N}={S}$
23 22 oveq1d ${⊢}{D}\in \mathrm{Fin}\to \left({S}{↾}_{𝑠}\mathrm{dom}{N}\right)\mathrm{GrpHom}{U}={S}\mathrm{GrpHom}{U}$
24 5 23 eleqtrd ${⊢}{D}\in \mathrm{Fin}\to {N}\in \left({S}\mathrm{GrpHom}{U}\right)$