This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ) → ( 𝑁 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( 𝑁 ‘ 𝐺 ) ) )