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	22	grpmndd	$⊢ φ \to H \in Mnd$
24	13	dmexd	$⊢ φ \to dom W \in V$
25		eqid	$⊢ 0_{H} = 0_{H}$
26	25	gsumz	$⊢ (H \in Mnd \land dom W \in V) \to \underset{a \in dom W}{\sum_{H}} 0_{H} = 0_{H}$
27	23 24 26	syl2anc	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} 0_{H} = 0_{H}$
28	8 9 5	unitgrpid	$⊢ Z \in Ring \to \underset{˙}{1} = 0_{H}$
29	20 28	syl	$⊢ φ \to \underset{˙}{1} = 0_{H}$
30	29	mpteq2dv	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) = (a \in dom W ⟼ 0_{H})$
31	30	oveq2d	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} = \underset{a \in dom W}{\sum_{H}} 0_{H}$
32	27 31 29	3eqtr4d	$⊢ φ \to \underset{a \in dom W}{\sum_{H}} \underset{˙}{1} = \underset{˙}{1}$
33	7 32	neeqtrrd	$⊢ φ \to A \neq \underset{a \in dom W}{\sum_{H}} \underset{˙}{1}$
34		zex	$⊢ ℤ \in V$
35	34	mptex	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
36	35	rnex	$⊢ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
37	36 11	dmmpti	$⊢ dom S = dom W$
38	37	a1i	$⊢ φ \to dom S = dom W$
39		eqid	$⊢ H dProj S = H dProj S$
40	12 15	eleqtrrd	$⊢ φ \to A \in (H DProd S)$
41		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)\}$
42	29	adantr	$⊢ (φ \land a \in dom W) \to \underset{˙}{1} = 0_{H}$
43	14 38	dprdf2	$⊢ φ \to S : dom W ⟶ SubGrp (H)$
44	43	ffvelrnda	$⊢ (φ \land a \in dom W) \to S (a) \in SubGrp (H)$
45	25	subg0cl	$⊢ S (a) \in SubGrp (H) \to 0_{H} \in S (a)$
46	44 45	syl	$⊢ (φ \land a \in dom W) \to 0_{H} \in S (a)$
47	42 46	eqeltrd	$⊢ (φ \land a \in dom W) \to \underset{˙}{1} \in S (a)$
48	5	fvexi	$⊢ \underset{˙}{1} \in V$
49	48	a1i	$⊢ φ \to \underset{˙}{1} \in V$
50	24 49	fczfsuppd	$⊢ φ \to {finSupp}_{\underset{˙}{1}} ((dom W \times \{\underset{˙}{1}\}))$
51		fconstmpt	$⊢ dom W \times \{\underset{˙}{1}\} = (a \in dom W ⟼ \underset{˙}{1})$
52	51	eqcomi	$⊢ (a \in dom W ⟼ \underset{˙}{1}) = dom W \times \{\underset{˙}{1}\}$
53	52	a1i	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) = dom W \times \{\underset{˙}{1}\}$
54	29	eqcomd	$⊢ φ \to 0_{H} = \underset{˙}{1}$
55	50 53 54	3brtr4d	$⊢ φ \to {finSupp}_{0_{H}} ((a \in dom W ⟼ \underset{˙}{1}))$
56	41 14 38 47 55	dprdwd	$⊢ φ \to (a \in dom W ⟼ \underset{˙}{1}) \in \{h \in \underset{i \in dom W}{⨉} S (i) \| {finSupp}_{0_{H}} (h)\}$
57	14 38 39 40 25 41 56	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})$
58	57	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})$
59	33 58	mpbid	$⊢ φ \to \neg \forall a \in dom W (H dProj S) (a) (A) = \underset{˙}{1}$
60		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}$
61	59 60	sylibr	$⊢ φ \to \exists a \in dom W \neg (H dProj S) (a) (A) = \underset{˙}{1}$
62		df-ne	$⊢ (H dProj S) (a) (A) \neq \underset{˙}{1} \leftrightarrow \neg (H dProj S) (a) (A) = \underset{˙}{1}$
63	6	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to N \in ℕ$
64	7	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to A \neq \underset{˙}{1}$
65	12	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to A \in U$
66	13	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to W \in Word U$
67	14	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to H dom DProd S$
68	15	adantr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to H DProd S = U$
69		eqid	$⊢ od (H) = od (H)$
70		eqid	$⊢ {(- 1)}^{\frac{2}{od (H) (W (a))}} = {(- 1)}^{\frac{2}{od (H) (W (a))}}$
71		simprl	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to a \in dom W$
72		simprr	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to (H dProj S) (a) (A) \neq \underset{˙}{1}$
73		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})))$
74	1 2 3 4 5 63 64 8 9 10 11 65 66 67 68 39 69 70 71 72 73	dchrptlem2	$⊢ (φ \land (a \in dom W \land (H dProj S) (a) (A) \neq \underset{˙}{1})) \to \exists x \in D x (A) \neq 1$
75	74	expr	$⊢ (φ \land a \in dom W) \to ((H dProj S) (a) (A) \neq \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
76	62 75	syl5bir	$⊢ (φ \land a \in dom W) \to (\neg (H dProj S) (a) (A) = \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
77	76	rexlimdva	$⊢ φ \to (\exists a \in dom W \neg (H dProj S) (a) (A) = \underset{˙}{1} \to \exists x \in D x (A) \neq 1)$
78	61 77	mpd	$⊢ φ \to \exists x \in D x (A) \neq 1$

Metamath Proof Explorer

Theorem dchrptlem3

Proof