Theorem psgnco

Description: Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	psgninv.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	psgninv.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
	psgninv.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
Assertion	psgnco	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝑁 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgninv.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		psgninv.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3		psgninv.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
4		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
5	1 3 4	symgov	⊢ ( ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝐹 ( +g ‘ 𝑆 ) 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
6	5	3adant1	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝐹 ( +g ‘ 𝑆 ) 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
7	6	fveq2d	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ( +g ‘ 𝑆 ) 𝐺 ) ) = ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) )
8		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
9	1 2 8	psgnghm2	⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
10		prex	⊢ { 1 , - 1 } ∈ V
11		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
12		cnfldmul	⊢ · = ( .r ‘ ℂfld )
13	11 12	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
14	8 13	ressplusg	⊢ ( { 1 , - 1 } ∈ V → · = ( +g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
15	10 14	ax-mp	⊢ · = ( +g ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
16	3 4 15	ghmlin	⊢ ( ( 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ( +g ‘ 𝑆 ) 𝐺 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝑁 ‘ 𝐺 ) ) )
17	9 16	syl3an1	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ( +g ‘ 𝑆 ) 𝐺 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝑁 ‘ 𝐺 ) ) )
18	7 17	eqtr3d	⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝑁 ‘ 𝐺 ) ) )