dchrptlem2

	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$
	dchrpt.p	$⊢ P = H dProj S$
	dchrpt.o	$⊢ O = od (H)$
	dchrpt.t	$⊢ T = {(- 1)}^{\frac{2}{O (W (I))}}$
	dchrpt.i	$⊢ φ \to I \in dom W$
	dchrpt.4	$⊢ φ \to P (I) (A) \neq \underset{˙}{1}$
	dchrpt.5	$⊢ X = (u \in U ⟼ (ι h \| \exists m \in ℤ (P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m})))$
Assertion	dchrptlem2	$⊢ φ \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		dchrpt.p	$⊢ P = H dProj S$
17		dchrpt.o	$⊢ O = od (H)$
18		dchrpt.t	$⊢ T = {(- 1)}^{\frac{2}{O (W (I))}}$
19		dchrpt.i	$⊢ φ \to I \in dom W$
20		dchrpt.4	$⊢ φ \to P (I) (A) \neq \underset{˙}{1}$
21		dchrpt.5	$⊢ X = (u \in U ⟼ (ι h \| \exists m \in ℤ (P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m})))$
22		fveq2	$⊢ v = x \to X (v) = X (x)$
23		fveq2	$⊢ v = y \to X (v) = X (y)$
24		fveq2	$⊢ v = x \cdot_{Z} y \to X (v) = X (x \cdot_{Z} y)$
25		fveq2	$⊢ v = 1_{Z} \to X (v) = X (1_{Z})$
26		zex	$⊢ ℤ \in V$
27	26	mptex	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
28	27	rnex	$⊢ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) \in V$
29	28 11	dmmpti	$⊢ dom S = dom W$
30	29	a1i	$⊢ φ \to dom S = dom W$
31	14 30 16 19	dpjf	$⊢ φ \to P (I) : H DProd S ⟶ S (I)$
32	15	feq2d	$⊢ φ \to (P (I) : H DProd S ⟶ S (I) \leftrightarrow P (I) : U ⟶ S (I))$
33	31 32	mpbid	$⊢ φ \to P (I) : U ⟶ S (I)$
34	33	ffvelcdmda	$⊢ (φ \land v \in U) \to P (I) (v) \in S (I)$
35	19	adantr	$⊢ (φ \land v \in U) \to I \in dom W$
36		oveq1	$⊢ n = a \to n \underset{˙}{\cdot} W (k) = a \underset{˙}{\cdot} W (k)$
37	36	cbvmptv	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) = (a \in ℤ ⟼ a \underset{˙}{\cdot} W (k))$
38		fveq2	$⊢ k = I \to W (k) = W (I)$
39	38	oveq2d	$⊢ k = I \to a \underset{˙}{\cdot} W (k) = a \underset{˙}{\cdot} W (I)$
40	39	mpteq2dv	$⊢ k = I \to (a \in ℤ ⟼ a \underset{˙}{\cdot} W (k)) = (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
41	37 40	eqtrid	$⊢ k = I \to (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) = (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
42	41	rneqd	$⊢ k = I \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} W (k)) = ran (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
43	42 11 28	fvmpt3i	$⊢ I \in dom W \to S (I) = ran (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
44	35 43	syl	$⊢ (φ \land v \in U) \to S (I) = ran (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
45	34 44	eleqtrd	$⊢ (φ \land v \in U) \to P (I) (v) \in ran (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
46		eqid	$⊢ (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I)) = (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I))$
47		ovex	$⊢ a \underset{˙}{\cdot} W (I) \in V$
48	46 47	elrnmpti	$⊢ P (I) (v) \in ran (a \in ℤ ⟼ a \underset{˙}{\cdot} W (I)) \leftrightarrow \exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I)$
49	45 48	sylib	$⊢ (φ \land v \in U) \to \exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I)$
50	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to X (v) = T^{a}$
51		neg1cn	$⊢ - 1 \in ℂ$
52		2re	$⊢ 2 \in ℝ$
53	6	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
54	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
55		crngring	$⊢ Z \in CRing \to Z \in Ring$
56	53 54 55	3syl	$⊢ φ \to Z \in Ring$
57	8 9	unitgrp	$⊢ Z \in Ring \to H \in Grp$
58	56 57	syl	$⊢ φ \to H \in Grp$
59	2 4	znfi	$⊢ N \in ℕ \to B \in Fin$
60	6 59	syl	$⊢ φ \to B \in Fin$
61	4 8	unitss	$⊢ U \subseteq B$
62		ssfi	$⊢ (B \in Fin \land U \subseteq B) \to U \in Fin$
63	60 61 62	sylancl	$⊢ φ \to U \in Fin$
64		wrdf	$⊢ W \in Word U \to W : (0 ..^\|W\|) ⟶ U$
65	13 64	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ U$
66	65	fdmd	$⊢ φ \to dom W = (0 ..^\|W\|)$
67	19 66	eleqtrd	$⊢ φ \to I \in (0 ..^\|W\|)$
68	65 67	ffvelcdmd	$⊢ φ \to W (I) \in U$
69	8 9	unitgrpbas	$⊢ U = {Base}_{H}$
70	69 17	odcl2	$⊢ (H \in Grp \land U \in Fin \land W (I) \in U) \to O (W (I)) \in ℕ$
71	58 63 68 70	syl3anc	$⊢ φ \to O (W (I)) \in ℕ$
72		nndivre	$⊢ (2 \in ℝ \land O (W (I)) \in ℕ) \to \frac{2}{O (W (I))} \in ℝ$
73	52 71 72	sylancr	$⊢ φ \to \frac{2}{O (W (I))} \in ℝ$
74	73	recnd	$⊢ φ \to \frac{2}{O (W (I))} \in ℂ$
75		cxpcl	$⊢ (- 1 \in ℂ \land \frac{2}{O (W (I))} \in ℂ) \to {(- 1)}^{\frac{2}{O (W (I))}} \in ℂ$
76	51 74 75	sylancr	$⊢ φ \to {(- 1)}^{\frac{2}{O (W (I))}} \in ℂ$
77	18 76	eqeltrid	$⊢ φ \to T \in ℂ$
78	77	ad2antrr	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to T \in ℂ$
79	51	a1i	$⊢ φ \to - 1 \in ℂ$
80		neg1ne0	$⊢ - 1 \neq 0$
81	80	a1i	$⊢ φ \to - 1 \neq 0$
82	79 81 74	cxpne0d	$⊢ φ \to {(- 1)}^{\frac{2}{O (W (I))}} \neq 0$
83	18	neeq1i	$⊢ T \neq 0 \leftrightarrow {(- 1)}^{\frac{2}{O (W (I))}} \neq 0$
84	82 83	sylibr	$⊢ φ \to T \neq 0$
85	84	ad2antrr	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to T \neq 0$
86		simprl	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to a \in ℤ$
87	78 85 86	expclzd	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to T^{a} \in ℂ$
88	50 87	eqeltrd	$⊢ ((φ \land v \in U) \land (a \in ℤ \land P (I) (v) = a \underset{˙}{\cdot} W (I))) \to X (v) \in ℂ$
89	49 88	rexlimddv	$⊢ (φ \land v \in U) \to X (v) \in ℂ$
90		fveqeq2	$⊢ v = x \to (P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (x) = a \underset{˙}{\cdot} W (I))$
91	90	rexbidv	$⊢ v = x \to (\exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow \exists a \in ℤ P (I) (x) = a \underset{˙}{\cdot} W (I))$
92	49	ralrimiva	$⊢ φ \to \forall v \in U \exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I)$
93	92	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to \forall v \in U \exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I)$
94		simprl	$⊢ (φ \land (x \in U \land y \in U)) \to x \in U$
95	91 93 94	rspcdva	$⊢ (φ \land (x \in U \land y \in U)) \to \exists a \in ℤ P (I) (x) = a \underset{˙}{\cdot} W (I)$
96		fveqeq2	$⊢ v = y \to (P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (y) = a \underset{˙}{\cdot} W (I))$
97	96	rexbidv	$⊢ v = y \to (\exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow \exists a \in ℤ P (I) (y) = a \underset{˙}{\cdot} W (I))$
98		oveq1	$⊢ a = b \to a \underset{˙}{\cdot} W (I) = b \underset{˙}{\cdot} W (I)$
99	98	eqeq2d	$⊢ a = b \to (P (I) (y) = a \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (y) = b \underset{˙}{\cdot} W (I))$
100	99	cbvrexvw	$⊢ \exists a \in ℤ P (I) (y) = a \underset{˙}{\cdot} W (I) \leftrightarrow \exists b \in ℤ P (I) (y) = b \underset{˙}{\cdot} W (I)$
101	97 100	bitrdi	$⊢ v = y \to (\exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow \exists b \in ℤ P (I) (y) = b \underset{˙}{\cdot} W (I))$
102		simprr	$⊢ (φ \land (x \in U \land y \in U)) \to y \in U$
103	101 93 102	rspcdva	$⊢ (φ \land (x \in U \land y \in U)) \to \exists b \in ℤ P (I) (y) = b \underset{˙}{\cdot} W (I)$
104		reeanv	$⊢ \exists a \in ℤ \exists b \in ℤ (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)) \leftrightarrow (\exists a \in ℤ P (I) (x) = a \underset{˙}{\cdot} W (I) \land \exists b \in ℤ P (I) (y) = b \underset{˙}{\cdot} W (I))$
105	77	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to T \in ℂ$
106	84	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to T \neq 0$
107		simprll	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to a \in ℤ$
108		simprlr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to b \in ℤ$
109		expaddz	$⊢ ((T \in ℂ \land T \neq 0) \land (a \in ℤ \land b \in ℤ)) \to T^{a + b} = T^{a} T^{b}$
110	105 106 107 108 109	syl22anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to T^{a + b} = T^{a} T^{b}$
111		simpll	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to φ$
112	56	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to Z \in Ring$
113	94	adantr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to x \in U$
114	102	adantr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to y \in U$
115		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
116	8 115	unitmulcl	$⊢ (Z \in Ring \land x \in U \land y \in U) \to x \cdot_{Z} y \in U$
117	112 113 114 116	syl3anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to x \cdot_{Z} y \in U$
118	107 108	zaddcld	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to a + b \in ℤ$
119		simprrl	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) (x) = a \underset{˙}{\cdot} W (I)$
120		simprrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) (y) = b \underset{˙}{\cdot} W (I)$
121	119 120	oveq12d	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) (x) \cdot_{Z} P (I) (y) = (a \underset{˙}{\cdot} W (I)) \cdot_{Z} (b \underset{˙}{\cdot} W (I))$
122	14 30 16 19	dpjghm	$⊢ φ \to P (I) \in ((H ↾_{𝑠} (H DProd S)) GrpHom H)$
123	15	oveq2d	$⊢ φ \to H ↾_{𝑠} (H DProd S) = H ↾_{𝑠} U$
124	9	ovexi	$⊢ H \in V$
125	69	ressid	$⊢ H \in V \to H ↾_{𝑠} U = H$
126	124 125	ax-mp	$⊢ H ↾_{𝑠} U = H$
127	123 126	eqtrdi	$⊢ φ \to H ↾_{𝑠} (H DProd S) = H$
128	127	oveq1d	$⊢ φ \to (H ↾_{𝑠} (H DProd S)) GrpHom H = H GrpHom H$
129	122 128	eleqtrd	$⊢ φ \to P (I) \in (H GrpHom H)$
130	129	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) \in (H GrpHom H)$
131	8	fvexi	$⊢ U \in V$
132		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
133	132 115	mgpplusg	$⊢ \cdot_{Z} = +_{{mulGrp}_{Z}}$
134	9 133	ressplusg	$⊢ U \in V \to \cdot_{Z} = +_{H}$
135	131 134	ax-mp	$⊢ \cdot_{Z} = +_{H}$
136	69 135 135	ghmlin	$⊢ (P (I) \in (H GrpHom H) \land x \in U \land y \in U) \to P (I) (x \cdot_{Z} y) = P (I) (x) \cdot_{Z} P (I) (y)$
137	130 113 114 136	syl3anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) (x \cdot_{Z} y) = P (I) (x) \cdot_{Z} P (I) (y)$
138	58	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to H \in Grp$
139	68	ad2antrr	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to W (I) \in U$
140	69 10 135	mulgdir	$⊢ (H \in Grp \land (a \in ℤ \land b \in ℤ \land W (I) \in U)) \to (a + b) \underset{˙}{\cdot} W (I) = (a \underset{˙}{\cdot} W (I)) \cdot_{Z} (b \underset{˙}{\cdot} W (I))$
141	138 107 108 139 140	syl13anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to (a + b) \underset{˙}{\cdot} W (I) = (a \underset{˙}{\cdot} W (I)) \cdot_{Z} (b \underset{˙}{\cdot} W (I))$
142	121 137 141	3eqtr4d	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to P (I) (x \cdot_{Z} y) = (a + b) \underset{˙}{\cdot} W (I)$
143	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land x \cdot_{Z} y \in U) \land (a + b \in ℤ \land P (I) (x \cdot_{Z} y) = (a + b) \underset{˙}{\cdot} W (I))) \to X (x \cdot_{Z} y) = T^{a + b}$
144	111 117 118 142 143	syl22anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to X (x \cdot_{Z} y) = T^{a + b}$
145	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land x \in U) \land (a \in ℤ \land P (I) (x) = a \underset{˙}{\cdot} W (I))) \to X (x) = T^{a}$
146	111 113 107 119 145	syl22anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to X (x) = T^{a}$
147	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land y \in U) \land (b \in ℤ \land P (I) (y) = b \underset{˙}{\cdot} W (I))) \to X (y) = T^{b}$
148	111 114 108 120 147	syl22anc	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to X (y) = T^{b}$
149	146 148	oveq12d	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to X (x) X (y) = T^{a} T^{b}$
150	110 144 149	3eqtr4d	$⊢ ((φ \land (x \in U \land y \in U)) \land ((a \in ℤ \land b \in ℤ) \land (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)))) \to X (x \cdot_{Z} y) = X (x) X (y)$
151	150	expr	$⊢ ((φ \land (x \in U \land y \in U)) \land (a \in ℤ \land b \in ℤ)) \to ((P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)) \to X (x \cdot_{Z} y) = X (x) X (y))$
152	151	rexlimdvva	$⊢ (φ \land (x \in U \land y \in U)) \to (\exists a \in ℤ \exists b \in ℤ (P (I) (x) = a \underset{˙}{\cdot} W (I) \land P (I) (y) = b \underset{˙}{\cdot} W (I)) \to X (x \cdot_{Z} y) = X (x) X (y))$
153	104 152	biimtrrid	$⊢ (φ \land (x \in U \land y \in U)) \to ((\exists a \in ℤ P (I) (x) = a \underset{˙}{\cdot} W (I) \land \exists b \in ℤ P (I) (y) = b \underset{˙}{\cdot} W (I)) \to X (x \cdot_{Z} y) = X (x) X (y))$
154	95 103 153	mp2and	$⊢ (φ \land (x \in U \land y \in U)) \to X (x \cdot_{Z} y) = X (x) X (y)$
155		id	$⊢ φ \to φ$
156		eqid	$⊢ 1_{Z} = 1_{Z}$
157	8 156	1unit	$⊢ Z \in Ring \to 1_{Z} \in U$
158	56 157	syl	$⊢ φ \to 1_{Z} \in U$
159		0zd	$⊢ φ \to 0 \in ℤ$
160		eqid	$⊢ 0_{H} = 0_{H}$
161	160 160	ghmid	$⊢ P (I) \in (H GrpHom H) \to P (I) (0_{H}) = 0_{H}$
162	129 161	syl	$⊢ φ \to P (I) (0_{H}) = 0_{H}$
163	8 9 156	unitgrpid	$⊢ Z \in Ring \to 1_{Z} = 0_{H}$
164	56 163	syl	$⊢ φ \to 1_{Z} = 0_{H}$
165	164	fveq2d	$⊢ φ \to P (I) (1_{Z}) = P (I) (0_{H})$
166	69 160 10	mulg0	$⊢ W (I) \in U \to 0 \underset{˙}{\cdot} W (I) = 0_{H}$
167	68 166	syl	$⊢ φ \to 0 \underset{˙}{\cdot} W (I) = 0_{H}$
168	162 165 167	3eqtr4d	$⊢ φ \to P (I) (1_{Z}) = 0 \underset{˙}{\cdot} W (I)$
169	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land 1_{Z} \in U) \land (0 \in ℤ \land P (I) (1_{Z}) = 0 \underset{˙}{\cdot} W (I))) \to X (1_{Z}) = T^{0}$
170	155 158 159 168 169	syl22anc	$⊢ φ \to X (1_{Z}) = T^{0}$
171	77	exp0d	$⊢ φ \to T^{0} = 1$
172	170 171	eqtrd	$⊢ φ \to X (1_{Z}) = 1$
173	1 2 4 8 6 3 22 23 24 25 89 154 172	dchrelbasd	$⊢ φ \to (v \in B ⟼ if (v \in U, X (v), 0)) \in D$
174	61 12	sselid	$⊢ φ \to A \in B$
175		eleq1	$⊢ v = A \to (v \in U \leftrightarrow A \in U)$
176		fveq2	$⊢ v = A \to X (v) = X (A)$
177	175 176	ifbieq1d	$⊢ v = A \to if (v \in U, X (v), 0) = if (A \in U, X (A), 0)$
178		eqid	$⊢ (v \in B ⟼ if (v \in U, X (v), 0)) = (v \in B ⟼ if (v \in U, X (v), 0))$
179		fvex	$⊢ X (v) \in V$
180		c0ex	$⊢ 0 \in V$
181	179 180	ifex	$⊢ if (v \in U, X (v), 0) \in V$
182	177 178 181	fvmpt3i	$⊢ A \in B \to (v \in B ⟼ if (v \in U, X (v), 0)) (A) = if (A \in U, X (A), 0)$
183	174 182	syl	$⊢ φ \to (v \in B ⟼ if (v \in U, X (v), 0)) (A) = if (A \in U, X (A), 0)$
184	12	iftrued	$⊢ φ \to if (A \in U, X (A), 0) = X (A)$
185	183 184	eqtrd	$⊢ φ \to (v \in B ⟼ if (v \in U, X (v), 0)) (A) = X (A)$
186		fveqeq2	$⊢ v = A \to (P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (A) = a \underset{˙}{\cdot} W (I))$
187	186	rexbidv	$⊢ v = A \to (\exists a \in ℤ P (I) (v) = a \underset{˙}{\cdot} W (I) \leftrightarrow \exists a \in ℤ P (I) (A) = a \underset{˙}{\cdot} W (I))$
188	187 92 12	rspcdva	$⊢ φ \to \exists a \in ℤ P (I) (A) = a \underset{˙}{\cdot} W (I)$
189	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	dchrptlem1	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to X (A) = T^{a}$
190	18	oveq1i	$⊢ T^{a} = {({-1}^{\frac{2}{O (W (I))}})}^{a}$
191	189 190	eqtrdi	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to X (A) = {({-1}^{\frac{2}{O (W (I))}})}^{a}$
192	20	ad2antrr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to P (I) (A) \neq \underset{˙}{1}$
193	58	ad2antrr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to H \in Grp$
194	68	ad2antrr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to W (I) \in U$
195		simprl	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to a \in ℤ$
196	69 17 10 160	oddvds	$⊢ (H \in Grp \land W (I) \in U \land a \in ℤ) \to (O (W (I)) ∥ a \leftrightarrow a \underset{˙}{\cdot} W (I) = 0_{H})$
197	193 194 195 196	syl3anc	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to (O (W (I)) ∥ a \leftrightarrow a \underset{˙}{\cdot} W (I) = 0_{H})$
198	71	ad2antrr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to O (W (I)) \in ℕ$
199		root1eq1	$⊢ (O (W (I)) \in ℕ \land a \in ℤ) \to ({({-1}^{\frac{2}{O (W (I))}})}^{a} = 1 \leftrightarrow O (W (I)) ∥ a)$
200	198 195 199	syl2anc	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to ({({-1}^{\frac{2}{O (W (I))}})}^{a} = 1 \leftrightarrow O (W (I)) ∥ a)$
201		simprr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to P (I) (A) = a \underset{˙}{\cdot} W (I)$
202	5 164	eqtrid	$⊢ φ \to \underset{˙}{1} = 0_{H}$
203	202	ad2antrr	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to \underset{˙}{1} = 0_{H}$
204	201 203	eqeq12d	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to (P (I) (A) = \underset{˙}{1} \leftrightarrow a \underset{˙}{\cdot} W (I) = 0_{H})$
205	197 200 204	3bitr4d	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to ({({-1}^{\frac{2}{O (W (I))}})}^{a} = 1 \leftrightarrow P (I) (A) = \underset{˙}{1})$
206	205	necon3bid	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to ({({-1}^{\frac{2}{O (W (I))}})}^{a} \neq 1 \leftrightarrow P (I) (A) \neq \underset{˙}{1})$
207	192 206	mpbird	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to {({-1}^{\frac{2}{O (W (I))}})}^{a} \neq 1$
208	191 207	eqnetrd	$⊢ ((φ \land A \in U) \land (a \in ℤ \land P (I) (A) = a \underset{˙}{\cdot} W (I))) \to X (A) \neq 1$
209	208	rexlimdvaa	$⊢ (φ \land A \in U) \to (\exists a \in ℤ P (I) (A) = a \underset{˙}{\cdot} W (I) \to X (A) \neq 1)$
210	12 209	mpdan	$⊢ φ \to (\exists a \in ℤ P (I) (A) = a \underset{˙}{\cdot} W (I) \to X (A) \neq 1)$
211	188 210	mpd	$⊢ φ \to X (A) \neq 1$
212	185 211	eqnetrd	$⊢ φ \to (v \in B ⟼ if (v \in U, X (v), 0)) (A) \neq 1$
213		fveq1	$⊢ x = (v \in B ⟼ if (v \in U, X (v), 0)) \to x (A) = (v \in B ⟼ if (v \in U, X (v), 0)) (A)$
214	213	neeq1d	$⊢ x = (v \in B ⟼ if (v \in U, X (v), 0)) \to (x (A) \neq 1 \leftrightarrow (v \in B ⟼ if (v \in U, X (v), 0)) (A) \neq 1)$
215	214	rspcev	$⊢ ((v \in B ⟼ if (v \in U, X (v), 0)) \in D \land (v \in B ⟼ if (v \in U, X (v), 0)) (A) \neq 1) \to \exists x \in D x (A) \neq 1$
216	173 212 215	syl2anc	$⊢ φ \to \exists x \in D x (A) \neq 1$

Metamath Proof Explorer

Theorem dchrptlem2

Proof