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	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	psgnghm2.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
	psgnghm2.u	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
Assertion	psgnghm2	⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		psgnghm2.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		psgnghm2.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3		psgnghm2.u	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
4		eqid	⊢ ( 𝑆 ↾s dom 𝑁 ) = ( 𝑆 ↾s dom 𝑁 )
5	1 2 4 3	psgnghm	⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( ( 𝑆 ↾s dom 𝑁 ) GrpHom 𝑈 ) )
6		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7	1 6	sygbasnfpfi	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → dom ( 𝑥 ∖ I ) ∈ Fin )
8	7	ralrimiva	⊢ ( 𝐷 ∈ Fin → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) dom ( 𝑥 ∖ I ) ∈ Fin )
9		rabid2	⊢ ( ( Base ‘ 𝑆 ) = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) dom ( 𝑥 ∖ I ) ∈ Fin )
10	8 9	sylibr	⊢ ( 𝐷 ∈ Fin → ( Base ‘ 𝑆 ) = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
11		eqid	⊢ { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
12	1 6 11 2	psgnfn	⊢ 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
13	12	fndmi	⊢ dom 𝑁 = { 𝑥 ∈ ( Base ‘ 𝑆 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin }
14	10 13	eqtr4di	⊢ ( 𝐷 ∈ Fin → ( Base ‘ 𝑆 ) = dom 𝑁 )
15		eqimss	⊢ ( ( Base ‘ 𝑆 ) = dom 𝑁 → ( Base ‘ 𝑆 ) ⊆ dom 𝑁 )
16	1	fvexi	⊢ 𝑆 ∈ V
17	2	fvexi	⊢ 𝑁 ∈ V
18	17	dmex	⊢ dom 𝑁 ∈ V
19	4 6	ressid2	⊢ ( ( ( Base ‘ 𝑆 ) ⊆ dom 𝑁 ∧ 𝑆 ∈ V ∧ dom 𝑁 ∈ V ) → ( 𝑆 ↾s dom 𝑁 ) = 𝑆 )
20	16 18 19	mp3an23	⊢ ( ( Base ‘ 𝑆 ) ⊆ dom 𝑁 → ( 𝑆 ↾s dom 𝑁 ) = 𝑆 )
21	14 15 20	3syl	⊢ ( 𝐷 ∈ Fin → ( 𝑆 ↾s dom 𝑁 ) = 𝑆 )
22	21	oveq1d	⊢ ( 𝐷 ∈ Fin → ( ( 𝑆 ↾s dom 𝑁 ) GrpHom 𝑈 ) = ( 𝑆 GrpHom 𝑈 ) )
23	5 22	eleqtrd	⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom 𝑈 ) )