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

Metamath Proof Explorer

Theorem psgnghm

Proof