dchrptlem3

	Ref	Expression
Hypotheses	dchrpt.g	$⊢ G = DChr (N)$
	dchrpt.z	$⊢ Z = ℤ / N ℤ$
	dchrpt.d	$⊢ D = {Base}_{G}$
	dchrpt.b	$⊢ B = {Base}_{Z}$
	dchrpt.1	$⊢ \underset{˙}{1} = 1_{Z}$
	dchrpt.n	$⊢ φ \to N \in ℕ$
	dchrpt.n1	$⊢ φ \to A \neq \underset{˙}{1}$
	dchrpt.u	$⊢ U = Unit (Z)$
	dchrpt.h	$⊢ H = {mulGrp}_{Z} ↾_{𝑠} U$
	dchrpt.m	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
	dchrpt.s	$⊢ S = (k \in dom W ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)))$
	dchrpt.au	$⊢ φ \to A \in U$
	dchrpt.w	$⊢ φ \to W \in Word U$
	dchrpt.2	$⊢ φ \to H dom DProd S$
	dchrpt.3	$⊢ φ \to H DProd S = U$
Assertion	dchrptlem3	$⊢ φ \to \exists x \in D x (A) \neq 1$

Proof

Step	Hyp	Ref	Expression
1		dchrpt.g	$⊢ G = DChr (N)$
2		dchrpt.z	$⊢ Z = ℤ / N ℤ$
3		dchrpt.d	$⊢ D = {Base}_{G}$
4		dchrpt.b	$⊢ B = {Base}_{Z}$
5		dchrpt.1	$⊢ \underset{˙}{1} = 1_{Z}$
6		dchrpt.n	$⊢ φ \to N \in ℕ$
7		dchrpt.n1	$⊢ φ \to A \neq \underset{˙}{1}$
8		dchrpt.u	$⊢ U = Unit (Z)$
9		dchrpt.h	$⊢ H = {mulGrp}_{Z} ↾_{𝑠} U$
10		dchrpt.m	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
11		dchrpt.s	$⊢ S = (k \in dom W ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)))$
12		dchrpt.au	$⊢ φ \to A \in U$
13		dchrpt.w	$⊢ φ \to W \in Word U$
14		dchrpt.2	$⊢ φ \to H dom DProd S$
15		dchrpt.3	$⊢ φ \to H DProd S = U$
16	6	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
17	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
18	16 17	syl	$⊢ φ \to Z \in CRing$
19		crngring	$⊢ Z \in CRing \to Z \in Ring$
20	18 19	syl	$⊢ φ \to Z \in Ring$
21	8 9	unitgrp	$⊢ Z \in Ring \to H \in Grp$
22	20 21	syl	$⊢ φ \to H \in Grp$
23		grpmnd	$⊢ H \in Grp \to H \in Mnd$
24	22 23	syl	$⊢ φ \to H \in Mnd$
25	13	dmexd	$⊢ φ \to dom W \in V$
26		eqid	$⊢ 0_{H} = 0_{H}$
27	26	gsumz	$⊢ (H \in Mnd \land dom W \in V) \to \underset{a \in dom W}{\sum_{H}} 0_{H} = 0_{H}$
28	24 25 27	syl2anc	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} 0_{H} = 0_{H}$
29	8 9 5	unitgrpid	$⊢ Z \in Ring \to \underset{˙}{1} = 0_{H}$
30	20 29	syl	$⊢ φ \to \underset{˙}{1} = 0_{H}$
31	30	mpteq2dv	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) = (a \in dom W ⟼ 0_{H})$
32	31	oveq2d	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} = \underset{a \in dom W}{\sum_{H}} 0_{H}$
33	28 32 30	3eqtr4d	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} = \underset{˙}{1}$
34	7 33	neeqtrrd	$⊢ φ \to A \neq \underset{a \in dom W}{\sum_{H}} \underset{˙}{1}$
35		zex	$⊢ ℤ \in V$
36	35	mptex	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
37	36	rnex	$⊢ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
38	37 11	dmmpti	$⊢ dom S = dom W$
39	38	a1i	$⊢ φ \to dom S = dom W$
40		eqid	$⊢ H dProj S = H dProj S$
41	12 15	eleqtrrd	$⊢ φ \to A \in (H DProd S)$
42		eqid	$⊢ \{h \in \underset{i \in dom W}{⨉} S (i) \| {finSupp}_{0_{H}} (h)\} = \{h \in \underset{i \in dom W}{⨉} S (i) \| {finSupp}_{0_{H}} (h)\}$
43	30	adantr	$⊢ (φ \land a \in dom W) \to \underset{˙}{1} = 0_{H}$
44	14 39	dprdf2	$⊢ φ \to S : dom W ⟶ SubGrp (H)$
45	44	ffvelrnda	$⊢ (φ \land a \in dom W) \to S (a) \in SubGrp (H)$
46	26	subg0cl	$⊢ S (a) \in SubGrp (H) \to 0_{H} \in S (a)$
47	45 46	syl	$⊢ (φ \land a \in dom W) \to 0_{H} \in S (a)$
48	43 47	eqeltrd	$⊢ (φ \land a \in dom W) \to \underset{˙}{1} \in S (a)$
49	5	fvexi	$⊢ \underset{˙}{1} \in V$
50	49	a1i	$⊢ φ \to \underset{˙}{1} \in V$
51	25 50	fczfsuppd	$⊢ φ \to {finSupp}_{\underset{˙}{1}} ((dom W \times \{\underset{˙}{1}\}))$
52		fconstmpt	$⊢ dom W \times \{\underset{˙}{1}\} = (a \in dom W ⟼ \underset{˙}{1})$
53	52	eqcomi	$⊢ (a \in dom W ⟼ \underset{˙}{1}) = dom W \times \{\underset{˙}{1}\}$
54	53	a1i	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) = dom W \times \{\underset{˙}{1}\}$
55	30	eqcomd	$⊢ φ \to 0_{H} = \underset{˙}{1}$
56	51 54 55	3brtr4d	$⊢ φ \to {finSupp}_{0_{H}} ((a \in dom W ⟼ \underset{˙}{1}))$
57	42 14 39 48 56	dprdwd	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) \in \{h \in \underset{i \in dom W}{⨉} S (i) \| {finSupp}_{0_{H}} (h)\}$
58	14 39 40 41 26 42 57	dpjeq	$⊢ φ \to (A = \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} \leftrightarrow \forall a \in dom W (H dProj S) (a) (A) = \underset{˙}{1})$
59	58	necon3abid	$⊢ φ \to (A \neq \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} \leftrightarrow \neg \forall a \in dom W (H dProj S) (a) (A) = \underset{˙}{1})$
60	34 59	mpbid	$⊢ φ \to \neg \forall a \in dom W (H dProj S) (a) (A) = \underset{˙}{1}$
61		rexnal	$⊢ \exists a \in dom W \neg (H dProj S) (a) (A) = \underset{˙}{1} \leftrightarrow \neg \forall a \in dom W (H dProj S) (a) (A) = \underset{˙}{1}$
62	60 61	sylibr	$⊢ φ \to \exists a \in dom W \neg (H dProj S) (a) (A) = \underset{˙}{1}$
63		df-ne	$⊢ (H dProj S) (a) (A) \neq \underset{˙}{1} \leftrightarrow \neg (H dProj S) (a) (A) = \underset{˙}{1}$
64	6	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to N \in ℕ$
65	7	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to A \neq \underset{˙}{1}$
66	12	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to A \in U$
67	13	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to W \in Word U$
68	14	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to H dom DProd S$
69	15	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to H DProd S = U$
70		eqid	$⊢ od (H) = od (H)$
71		eqid	$⊢ {(- 1)}^{\frac{2}{od (H) (W (a))}} = {(- 1)}^{\frac{2}{od (H) (W (a))}}$
72		simprl	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to a \in dom W$
73		simprr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to (H dProj S) (a) (A) \neq \underset{˙}{1}$
74		eqid	$⊢ (u \in U ⟼ (ι h \| \exists m \in ℤ ((H dProj S) (a) (u) = m \underset{˙}{\cdot} W (a) \land h = {({-1}^{\frac{2}{od (H) (W (a))}})}^{m}))) = (u \in U ⟼ (ι h \| \exists m \in ℤ ((H dProj S) (a) (u) = m \underset{˙}{\cdot} W (a) \land h = {({-1}^{\frac{2}{od (H) (W (a))}})}^{m})))$
75	1 2 3 4 5 64 65 8 9 10 11 66 67 68 69 40 70 71 72 73 74	dchrptlem2	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to \exists x \in D x (A) \neq 1$
76	75	expr	$⊢ (φ \land a \in dom W) \to ((H dProj S) (a) (A) \neq \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
77	63 76	syl5bir	$⊢ (φ \land a \in dom W) \to (\neg (H dProj S) (a) (A) = \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
78	77	rexlimdva	$⊢ φ \to (\exists a \in dom W \neg (H dProj S) (a) (A) = \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
79	62 78	mpd	$⊢ φ \to \exists x \in D x (A) \neq 1$

Metamath Proof Explorer

Theorem dchrptlem3

Proof