Theorem 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 e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F o. G ) ) = ( ( N ` F ) x. ( N ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgninv.s	|- S = ( SymGrp ` D )
2		psgninv.n	|- N = ( pmSgn ` D )
3		psgninv.p	|- P = ( Base ` S )
4		eqid	|- ( +g ` S ) = ( +g ` S )
5	1 3 4	symgov	|- ( ( F e. P /\ G e. P ) -> ( F ( +g ` S ) G ) = ( F o. G ) )
6	5	3adant1	|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( F ( +g ` S ) G ) = ( F o. G ) )
7	6	fveq2d	|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( N ` ( F o. G ) ) )
8		eqid	|- ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
9	1 2 8	psgnghm2	|- ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
10		prex	|- { 1 , -u 1 } e. _V
11		eqid	|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
12		cnfldmul	|- x. = ( .r ` CCfld )
13	11 12	mgpplusg	|- x. = ( +g ` ( mulGrp ` CCfld ) )
14	8 13	ressplusg	|- ( { 1 , -u 1 } e. _V -> x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
15	10 14	ax-mp	|- x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
16	3 4 15	ghmlin	|- ( ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( ( N ` F ) x. ( N ` G ) ) )
17	9 16	syl3an1	|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( ( N ` F ) x. ( N ` G ) ) )
18	7 17	eqtr3d	|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F o. G ) ) = ( ( N ` F ) x. ( N ` G ) ) )