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	|- S = ( SymGrp ` D )
	psgnghm2.n	|- N = ( pmSgn ` D )
	psgnghm2.u	|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
Assertion	psgnghm2	|- ( D e. Fin -> N e. ( S GrpHom U ) )

Proof

Step	Hyp	Ref	Expression
1		psgnghm2.s	|- S = ( SymGrp ` D )
2		psgnghm2.n	|- N = ( pmSgn ` D )
3		psgnghm2.u	|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
4		eqid	|- ( S |`s dom N ) = ( S |`s dom N )
5	1 2 4 3	psgnghm	|- ( D e. Fin -> N e. ( ( S |`s dom N ) GrpHom U ) )
6		eqid	|- ( Base ` S ) = ( Base ` S )
7	1 6	sygbasnfpfi	|- ( ( D e. Fin /\ x e. ( Base ` S ) ) -> dom ( x \ _I ) e. Fin )
8	7	ralrimiva	|- ( D e. Fin -> A. x e. ( Base ` S ) dom ( x \ _I ) e. Fin )
9		rabid2	|- ( ( Base ` S ) = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin } <-> A. x e. ( Base ` S ) dom ( x \ _I ) e. Fin )
10	8 9	sylibr	|- ( D e. Fin -> ( Base ` S ) = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin } )
11		eqid	|- { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin } = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
12	1 6 11 2	psgnfn	|- N Fn { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
13	12	fndmi	|- dom N = { x e. ( Base ` S ) | dom ( x \ _I ) e. Fin }
14	10 13	eqtr4di	|- ( D e. Fin -> ( Base ` S ) = dom N )
15		eqimss	|- ( ( Base ` S ) = dom N -> ( Base ` S ) C_ dom N )
16	1	fvexi	|- S e. _V
17	2	fvexi	|- N e. _V
18	17	dmex	|- dom N e. _V
19	4 6	ressid2	|- ( ( ( Base ` S ) C_ dom N /\ S e. _V /\ dom N e. _V ) -> ( S |`s dom N ) = S )
20	16 18 19	mp3an23	|- ( ( Base ` S ) C_ dom N -> ( S |`s dom N ) = S )
21	14 15 20	3syl	|- ( D e. Fin -> ( S |`s dom N ) = S )
22	21	oveq1d	|- ( D e. Fin -> ( ( S |`s dom N ) GrpHom U ) = ( S GrpHom U ) )
23	5 22	eleqtrd	|- ( D e. Fin -> N e. ( S GrpHom U ) )