dchrptlem1

	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	dchrptlem1	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to X (C) = T^{M}$

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		fveqeq2	$⊢ u = C \to (P (I) (u) = m \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (C) = m \underset{˙}{\cdot} W (I))$
23	22	anbi1d	$⊢ u = C \to ((P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \leftrightarrow (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
24	23	rexbidv	$⊢ u = C \to (\exists m \in ℤ (P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \leftrightarrow \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
25	24	iotabidv	$⊢ u = C \to (ι h \| \exists m \in ℤ (P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m})) = (ι h \| \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
26		iotaex	$⊢ (ι h \| \exists m \in ℤ (P (I) (u) = m \underset{˙}{\cdot} W (I) \land h = T^{m})) \in V$
27	25 21 26	fvmpt3i	$⊢ C \in U \to X (C) = (ι h \| \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
28	27	ad2antlr	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to X (C) = (ι h \| \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
29		ovex	$⊢ T^{M} \in V$
30		simpr	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to P (I) (C) = m \underset{˙}{\cdot} W (I)$
31		simpllr	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))$
32	31	simprd	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to P (I) (C) = M \underset{˙}{\cdot} W (I)$
33	30 32	eqtr3d	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I)$
34		simp-4l	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to φ$
35		simplr	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to m \in ℤ$
36	31	simpld	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to M \in ℤ$
37	6	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
38	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
39		crngring	$⊢ Z \in CRing \to Z \in Ring$
40	8 9	unitgrp	$⊢ Z \in Ring \to H \in Grp$
41	37 38 39 40	4syl	$⊢ φ \to H \in Grp$
42	41	adantr	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to H \in Grp$
43		wrdf	$⊢ W \in Word U \to W : (0 ..^\|W\|) ⟶ U$
44	13 43	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ U$
45	44	fdmd	$⊢ φ \to dom W = (0 ..^\|W\|)$
46	19 45	eleqtrd	$⊢ φ \to I \in (0 ..^\|W\|)$
47	44 46	ffvelrnd	$⊢ φ \to W (I) \in U$
48	47	adantr	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to W (I) \in U$
49		simprl	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to m \in ℤ$
50		simprr	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to M \in ℤ$
51	8 9	unitgrpbas	$⊢ U = {Base}_{H}$
52		eqid	$⊢ 0_{H} = 0_{H}$
53	51 17 10 52	odcong	$⊢ (H \in Grp \land W (I) \in U \land (m \in ℤ \land M \in ℤ)) \to (O (W (I)) ∥ (m - M) \leftrightarrow m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I))$
54	42 48 49 50 53	syl112anc	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to (O (W (I)) ∥ (m - M) \leftrightarrow m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I))$
55		neg1cn	$⊢ - 1 \in ℂ$
56		2re	$⊢ 2 \in ℝ$
57	2 4	znfi	$⊢ N \in ℕ \to B \in Fin$
58	6 57	syl	$⊢ φ \to B \in Fin$
59	4 8	unitss	$⊢ U \subseteq B$
60		ssfi	$⊢ (B \in Fin \land U \subseteq B) \to U \in Fin$
61	58 59 60	sylancl	$⊢ φ \to U \in Fin$
62	51 17	odcl2	$⊢ (H \in Grp \land U \in Fin \land W (I) \in U) \to O (W (I)) \in ℕ$
63	41 61 47 62	syl3anc	$⊢ φ \to O (W (I)) \in ℕ$
64	63	ad2antrr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to O (W (I)) \in ℕ$
65		nndivre	$⊢ (2 \in ℝ \land O (W (I)) \in ℕ) \to \frac{2}{O (W (I))} \in ℝ$
66	56 64 65	sylancr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to \frac{2}{O (W (I))} \in ℝ$
67	66	recnd	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to \frac{2}{O (W (I))} \in ℂ$
68		cxpcl	$⊢ (- 1 \in ℂ \land \frac{2}{O (W (I))} \in ℂ) \to {(- 1)}^{\frac{2}{O (W (I))}} \in ℂ$
69	55 67 68	sylancr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to {(- 1)}^{\frac{2}{O (W (I))}} \in ℂ$
70	18 69	eqeltrid	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T \in ℂ$
71	55	a1i	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to - 1 \in ℂ$
72		neg1ne0	$⊢ - 1 \neq 0$
73	72	a1i	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to - 1 \neq 0$
74	71 73 67	cxpne0d	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to {(- 1)}^{\frac{2}{O (W (I))}} \neq 0$
75	18	neeq1i	$⊢ T \neq 0 \leftrightarrow {(- 1)}^{\frac{2}{O (W (I))}} \neq 0$
76	74 75	sylibr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T \neq 0$
77		zsubcl	$⊢ (m \in ℤ \land M \in ℤ) \to m - M \in ℤ$
78	77	ad2antlr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to m - M \in ℤ$
79	50	adantr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to M \in ℤ$
80		expaddz	$⊢ ((T \in ℂ \land T \neq 0) \land (m - M \in ℤ \land M \in ℤ)) \to T^{m - M + M} = T^{m - M} T^{M}$
81	70 76 78 79 80	syl22anc	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m - M + M} = T^{m - M} T^{M}$
82	49	adantr	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to m \in ℤ$
83	82	zcnd	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to m \in ℂ$
84	79	zcnd	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to M \in ℂ$
85	83 84	npcand	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to m - M + M = m$
86	85	oveq2d	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m - M + M} = T^{m}$
87	18	oveq1i	$⊢ T^{m - M} = {({-1}^{\frac{2}{O (W (I))}})}^{m - M}$
88		root1eq1	$⊢ (O (W (I)) \in ℕ \land m - M \in ℤ) \to ({({-1}^{\frac{2}{O (W (I))}})}^{m - M} = 1 \leftrightarrow O (W (I)) ∥ (m - M))$
89	63 77 88	syl2an	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to ({({-1}^{\frac{2}{O (W (I))}})}^{m - M} = 1 \leftrightarrow O (W (I)) ∥ (m - M))$
90	89	biimpar	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to {({-1}^{\frac{2}{O (W (I))}})}^{m - M} = 1$
91	87 90	eqtrid	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m - M} = 1$
92	91	oveq1d	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m - M} T^{M} = 1 T^{M}$
93	70 76 79	expclzd	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{M} \in ℂ$
94	93	mulid2d	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to 1 T^{M} = T^{M}$
95	92 94	eqtrd	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m - M} T^{M} = T^{M}$
96	81 86 95	3eqtr3d	$⊢ ((φ \land (m \in ℤ \land M \in ℤ)) \land O (W (I)) ∥ (m - M)) \to T^{m} = T^{M}$
97	96	ex	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to (O (W (I)) ∥ (m - M) \to T^{m} = T^{M})$
98	54 97	sylbird	$⊢ (φ \land (m \in ℤ \land M \in ℤ)) \to (m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I) \to T^{m} = T^{M})$
99	34 35 36 98	syl12anc	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to (m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I) \to T^{m} = T^{M})$
100	33 99	mpd	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to T^{m} = T^{M}$
101	100	eqeq2d	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to (h = T^{m} \leftrightarrow h = T^{M})$
102	101	biimpd	$⊢ ((((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \land P (I) (C) = m \underset{˙}{\cdot} W (I)) \to (h = T^{m} \to h = T^{M})$
103	102	expimpd	$⊢ (((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land m \in ℤ) \to ((P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \to h = T^{M})$
104	103	rexlimdva	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to (\exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \to h = T^{M})$
105		oveq1	$⊢ m = M \to m \underset{˙}{\cdot} W (I) = M \underset{˙}{\cdot} W (I)$
106	105	eqeq2d	$⊢ m = M \to (P (I) (C) = m \underset{˙}{\cdot} W (I) \leftrightarrow P (I) (C) = M \underset{˙}{\cdot} W (I))$
107		oveq2	$⊢ m = M \to T^{m} = T^{M}$
108	107	eqeq2d	$⊢ m = M \to (h = T^{m} \leftrightarrow h = T^{M})$
109	106 108	anbi12d	$⊢ m = M \to ((P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \leftrightarrow (P (I) (C) = M \underset{˙}{\cdot} W (I) \land h = T^{M}))$
110	109	rspcev	$⊢ (M \in ℤ \land (P (I) (C) = M \underset{˙}{\cdot} W (I) \land h = T^{M})) \to \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m})$
111	110	expr	$⊢ (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I)) \to (h = T^{M} \to \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
112	111	adantl	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to (h = T^{M} \to \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}))$
113	104 112	impbid	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to (\exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \leftrightarrow h = T^{M})$
114	113	adantr	$⊢ (((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land T^{M} \in V) \to (\exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m}) \leftrightarrow h = T^{M})$
115	114	iota5	$⊢ (((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \land T^{M} \in V) \to (ι h \| \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m})) = T^{M}$
116	29 115	mpan2	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to (ι h \| \exists m \in ℤ (P (I) (C) = m \underset{˙}{\cdot} W (I) \land h = T^{m})) = T^{M}$
117	28 116	eqtrd	$⊢ ((φ \land C \in U) \land (M \in ℤ \land P (I) (C) = M \underset{˙}{\cdot} W (I))) \to X (C) = T^{M}$

Metamath Proof Explorer

Theorem dchrptlem1

Proof