psgnghm2

Description: The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015)

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 ) )

Metamath Proof Explorer