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}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
4		eqid	$⊢ S ↾_{𝑠} dom N = S ↾_{𝑠} dom N$
5	1 2 4 3	psgnghm	$⊢ D \in Fin \to N \in ((S ↾_{𝑠} dom N) GrpHom U)$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7	1 6	sygbasnfpfi	$⊢ (D \in Fin \land x \in {Base}_{S}) \to dom (x ∖ I) \in Fin$
8	7	ralrimiva	$⊢ D \in Fin \to \forall x \in {Base}_{S} dom (x ∖ I) \in Fin$
9		rabid2	$⊢ {Base}_{S} = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\} \leftrightarrow \forall x \in {Base}_{S} dom (x ∖ I) \in Fin$
10	8 9	sylibr	$⊢ D \in Fin \to {Base}_{S} = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
11		eqid	$⊢ \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\} = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
12	1 6 11 2	psgnfn	$⊢ N Fn \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
13	12	fndmi	$⊢ dom N = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
14	10 13	eqtr4di	$⊢ D \in Fin \to {Base}_{S} = dom N$
15		eqimss	$⊢ {Base}_{S} = dom N \to {Base}_{S} \subseteq dom N$
16	1	fvexi	$⊢ S \in V$
17	2	fvexi	$⊢ N \in V$
18	17	dmex	$⊢ dom N \in V$
19	4 6	ressid2	$⊢ ({Base}_{S} \subseteq dom N \land S \in V \land dom N \in V) \to S ↾_{𝑠} dom N = S$
20	16 18 19	mp3an23	$⊢ {Base}_{S} \subseteq dom N \to S ↾_{𝑠} dom N = S$
21	14 15 20	3syl	$⊢ D \in Fin \to S ↾_{𝑠} dom N = S$
22	21	oveq1d	$⊢ D \in Fin \to (S ↾_{𝑠} dom N) GrpHom U = S GrpHom U$
23	5 22	eleqtrd	$⊢ D \in Fin \to N \in (S GrpHom U)$

Metamath Proof Explorer