psgnghm

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

	Ref	Expression
Hypotheses	psgnghm.s	$⊢ S = SymGrp (D)$
	psgnghm.n	$⊢ N = pmSgn (D)$
	psgnghm.f	$⊢ F = S ↾_{𝑠} dom N$
	psgnghm.u	$⊢ U = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
Assertion	psgnghm	$⊢ D \in V \to N \in (F GrpHom U)$

Proof

Step	Hyp	Ref	Expression
1		psgnghm.s	$⊢ S = SymGrp (D)$
2		psgnghm.n	$⊢ N = pmSgn (D)$
3		psgnghm.f	$⊢ F = S ↾_{𝑠} dom N$
4		psgnghm.u	$⊢ U = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6		eqid	$⊢ \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\} = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
7	1 5 6 2	psgnfn	$⊢ N Fn \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
8	7	fndmi	$⊢ dom N = \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\}$
9	8	ssrab3	$⊢ dom N \subseteq {Base}_{S}$
10	3 5	ressbas2	$⊢ dom N \subseteq {Base}_{S} \to dom N = {Base}_{F}$
11	9 10	ax-mp	$⊢ dom N = {Base}_{F}$
12	4	cnmsgnbas	$⊢ \{1, - 1\} = {Base}_{U}$
13	11	fvexi	$⊢ dom N \in V$
14		eqid	$⊢ +_{S} = +_{S}$
15	3 14	ressplusg	$⊢ dom N \in V \to +_{S} = +_{F}$
16	13 15	ax-mp	$⊢ +_{S} = +_{F}$
17		prex	$⊢ \{1, - 1\} \in V$
18		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
19		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
20	18 19	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
21	4 20	ressplusg	$⊢ \{1, - 1\} \in V \to \times = +_{U}$
22	17 21	ax-mp	$⊢ \times = +_{U}$
23	1 2	psgndmsubg	$⊢ D \in V \to dom N \in SubGrp (S)$
24	3	subggrp	$⊢ dom N \in SubGrp (S) \to F \in Grp$
25	23 24	syl	$⊢ D \in V \to F \in Grp$
26	4	cnmsgngrp	$⊢ U \in Grp$
27	26	a1i	$⊢ D \in V \to U \in Grp$
28		fnfun	$⊢ N Fn \{x \in {Base}_{S} \| dom (x ∖ I) \in Fin\} \to Fun N$
29	7 28	ax-mp	$⊢ Fun N$
30		funfn	$⊢ Fun N \leftrightarrow N Fn dom N$
31	29 30	mpbi	$⊢ N Fn dom N$
32	31	a1i	$⊢ D \in V \to N Fn dom N$
33		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
34	1 33 2	psgnvali	$⊢ x \in dom N \to \exists z \in Word ran pmTrsp (D) (x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|})$
35		lencl	$⊢ z \in Word ran pmTrsp (D) \to \|z\| \in ℕ_{0}$
36	35	nn0zd	$⊢ z \in Word ran pmTrsp (D) \to \|z\| \in ℤ$
37		m1expcl2	$⊢ \|z\| \in ℤ \to {(- 1)}^{\|z\|} \in \{- 1, 1\}$
38		prcom	$⊢ \{- 1, 1\} = \{1, - 1\}$
39	37 38	eleqtrdi	$⊢ \|z\| \in ℤ \to {(- 1)}^{\|z\|} \in \{1, - 1\}$
40		eleq1a	$⊢ {(- 1)}^{\|z\|} \in \{1, - 1\} \to (N (x) = {(- 1)}^{\|z\|} \to N (x) \in \{1, - 1\})$
41	36 39 40	3syl	$⊢ z \in Word ran pmTrsp (D) \to (N (x) = {(- 1)}^{\|z\|} \to N (x) \in \{1, - 1\})$
42	41	adantld	$⊢ z \in Word ran pmTrsp (D) \to ((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \to N (x) \in \{1, - 1\})$
43	42	rexlimiv	$⊢ \exists z \in Word ran pmTrsp (D) (x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \to N (x) \in \{1, - 1\}$
44	43	a1i	$⊢ D \in V \to (\exists z \in Word ran pmTrsp (D) (x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \to N (x) \in \{1, - 1\})$
45	34 44	syl5	$⊢ D \in V \to (x \in dom N \to N (x) \in \{1, - 1\})$
46	45	ralrimiv	$⊢ D \in V \to \forall x \in dom N N (x) \in \{1, - 1\}$
47		ffnfv	$⊢ N : dom N ⟶ \{1, - 1\} \leftrightarrow (N Fn dom N \land \forall x \in dom N N (x) \in \{1, - 1\})$
48	32 46 47	sylanbrc	$⊢ D \in V \to N : dom N ⟶ \{1, - 1\}$
49		ccatcl	$⊢ (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D)) \to z ++ w \in Word ran pmTrsp (D)$
50	1 33 2	psgnvalii	$⊢ (D \in V \land z ++ w \in Word ran pmTrsp (D)) \to N (\sum_{S} (z ++ w)) = {(- 1)}^{\|z ++ w\|}$
51	49 50	sylan2	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to N (\sum_{S} (z ++ w)) = {(- 1)}^{\|z ++ w\|}$
52	1	symggrp	$⊢ D \in V \to S \in Grp$
53	52	grpmndd	$⊢ D \in V \to S \in Mnd$
54	33 1 5	symgtrf	$⊢ ran pmTrsp (D) \subseteq {Base}_{S}$
55		sswrd	$⊢ ran pmTrsp (D) \subseteq {Base}_{S} \to Word ran pmTrsp (D) \subseteq Word {Base}_{S}$
56	54 55	ax-mp	$⊢ Word ran pmTrsp (D) \subseteq Word {Base}_{S}$
57	56	sseli	$⊢ z \in Word ran pmTrsp (D) \to z \in Word {Base}_{S}$
58	56	sseli	$⊢ w \in Word ran pmTrsp (D) \to w \in Word {Base}_{S}$
59	5 14	gsumccat	$⊢ (S \in Mnd \land z \in Word {Base}_{S} \land w \in Word {Base}_{S}) \to \sum_{S} (z ++ w) = (\sum_{S}, z) +_{S} (\sum_{S}, w)$
60	53 57 58 59	syl3an	$⊢ (D \in V \land z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D)) \to \sum_{S} (z ++ w) = (\sum_{S}, z) +_{S} (\sum_{S}, w)$
61	60	3expb	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to \sum_{S} (z ++ w) = (\sum_{S}, z) +_{S} (\sum_{S}, w)$
62	61	fveq2d	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to N (\sum_{S} (z ++ w)) = N ((\sum_{S}, z) +_{S} (\sum_{S}, w))$
63		ccatlen	$⊢ (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D)) \to \|z ++ w\| = \|z\| + \|w\|$
64	63	adantl	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to \|z ++ w\| = \|z\| + \|w\|$
65	64	oveq2d	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to {(- 1)}^{\|z ++ w\|} = {(- 1)}^{\|z\| + \|w\|}$
66		neg1cn	$⊢ - 1 \in ℂ$
67	66	a1i	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to - 1 \in ℂ$
68		lencl	$⊢ w \in Word ran pmTrsp (D) \to \|w\| \in ℕ_{0}$
69	68	ad2antll	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to \|w\| \in ℕ_{0}$
70	35	ad2antrl	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to \|z\| \in ℕ_{0}$
71	67 69 70	expaddd	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to {(- 1)}^{\|z\| + \|w\|} = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|}$
72	65 71	eqtrd	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to {(- 1)}^{\|z ++ w\|} = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|}$
73	51 62 72	3eqtr3d	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to N ((\sum_{S}, z) +_{S} (\sum_{S}, w)) = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|}$
74		oveq12	$⊢ (x = \sum_{S} z \land y = \sum_{S} w) \to x +_{S} y = (\sum_{S}, z) +_{S} (\sum_{S}, w)$
75	74	fveq2d	$⊢ (x = \sum_{S} z \land y = \sum_{S} w) \to N (x +_{S} y) = N ((\sum_{S}, z) +_{S} (\sum_{S}, w))$
76		oveq12	$⊢ (N (x) = {(- 1)}^{\|z\|} \land N (y) = {(- 1)}^{\|w\|}) \to N (x) N (y) = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|}$
77	75 76	eqeqan12d	$⊢ ((x = \sum_{S} z \land y = \sum_{S} w) \land (N (x) = {(- 1)}^{\|z\|} \land N (y) = {(- 1)}^{\|w\|})) \to (N (x +_{S} y) = N (x) N (y) \leftrightarrow N ((\sum_{S}, z) +_{S} (\sum_{S}, w)) = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|})$
78	77	an4s	$⊢ ((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|})) \to (N (x +_{S} y) = N (x) N (y) \leftrightarrow N ((\sum_{S}, z) +_{S} (\sum_{S}, w)) = {(- 1)}^{\|z\|} {(- 1)}^{\|w\|})$
79	73 78	syl5ibrcom	$⊢ (D \in V \land (z \in Word ran pmTrsp (D) \land w \in Word ran pmTrsp (D))) \to (((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|})) \to N (x +_{S} y) = N (x) N (y))$
80	79	rexlimdvva	$⊢ D \in V \to (\exists z \in Word ran pmTrsp (D) \exists w \in Word ran pmTrsp (D) ((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|})) \to N (x +_{S} y) = N (x) N (y))$
81	1 33 2	psgnvali	$⊢ y \in dom N \to \exists w \in Word ran pmTrsp (D) (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|})$
82	34 81	anim12i	$⊢ (x \in dom N \land y \in dom N) \to (\exists z \in Word ran pmTrsp (D) (x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land \exists w \in Word ran pmTrsp (D) (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|}))$
83		reeanv	$⊢ \exists z \in Word ran pmTrsp (D) \exists w \in Word ran pmTrsp (D) ((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|})) \leftrightarrow (\exists z \in Word ran pmTrsp (D) (x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land \exists w \in Word ran pmTrsp (D) (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|}))$
84	82 83	sylibr	$⊢ (x \in dom N \land y \in dom N) \to \exists z \in Word ran pmTrsp (D) \exists w \in Word ran pmTrsp (D) ((x = \sum_{S} z \land N (x) = {(- 1)}^{\|z\|}) \land (y = \sum_{S} w \land N (y) = {(- 1)}^{\|w\|}))$
85	80 84	impel	$⊢ (D \in V \land (x \in dom N \land y \in dom N)) \to N (x +_{S} y) = N (x) N (y)$
86	11 12 16 22 25 27 48 85	isghmd	$⊢ D \in V \to N \in (F GrpHom U)$

Metamath Proof Explorer

Theorem psgnghm

Proof