psgnco

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

	Ref	Expression
Hypotheses	psgninv.s	$⊢ S = SymGrp (D)$
	psgninv.n	$⊢ N = pmSgn (D)$
	psgninv.p	$⊢ P = {Base}_{S}$
Assertion	psgnco	$⊢ (D \in Fin \land F \in P \land G \in P) \to N (F \circ G) = N (F) N (G)$

Step	Hyp	Ref	Expression
1		psgninv.s	$⊢ S = SymGrp (D)$
2		psgninv.n	$⊢ N = pmSgn (D)$
3		psgninv.p	$⊢ P = {Base}_{S}$
4		eqid	$⊢ +_{S} = +_{S}$
5	1 3 4	symgov	$⊢ (F \in P \land G \in P) \to F +_{S} G = F \circ G$
6	5	3adant1	$⊢ (D \in Fin \land F \in P \land G \in P) \to F +_{S} G = F \circ G$
7	6	fveq2d	$⊢ (D \in Fin \land F \in P \land G \in P) \to N (F +_{S} G) = N (F \circ G)$
8		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
9	1 2 8	psgnghm2	$⊢ D \in Fin \to N \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
10		prex	$⊢ \{1, - 1\} \in V$
11		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
12		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
13	11 12	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
14	8 13	ressplusg	$⊢ \{1, - 1\} \in V \to \times = +_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
15	10 14	ax-mp	$⊢ \times = +_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
16	3 4 15	ghmlin	$⊢ (N \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \land F \in P \land G \in P) \to N (F +_{S} G) = N (F) N (G)$
17	9 16	syl3an1	$⊢ (D \in Fin \land F \in P \land G \in P) \to N (F +_{S} G) = N (F) N (G)$
18	7 17	eqtr3d	$⊢ (D \in Fin \land F \in P \land G \in P) \to N (F \circ G) = N (F) N (G)$

Metamath Proof Explorer