cycpmco2lem4

	Ref	Expression
Hypotheses	cycpmco2.c	$⊢ M = toCyc (D)$
	cycpmco2.s	$⊢ S = SymGrp (D)$
	cycpmco2.d	$⊢ φ \to D \in V$
	cycpmco2.w	$⊢ φ \to W \in dom M$
	cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
	cycpmco2.j	$⊢ φ \to J \in ran W$
	cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
	cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
Assertion	cycpmco2lem4	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (U) (I)$

Proof

Step	Hyp	Ref	Expression
1		cycpmco2.c	$⊢ M = toCyc (D)$
2		cycpmco2.s	$⊢ S = SymGrp (D)$
3		cycpmco2.d	$⊢ φ \to D \in V$
4		cycpmco2.w	$⊢ φ \to W \in dom M$
5		cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
6		cycpmco2.j	$⊢ φ \to J \in ran W$
7		cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
8		cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
9	1 2 3 4 5 6 7 8	cycpmco2lem1	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (W) (J)$
10	3	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to D \in V$
11		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13	1 2 12	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
14	3 13	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
15	14	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
16	4 15	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
17	11 16	sselid	$⊢ φ \to W \in Word D$
18	5	eldifad	$⊢ φ \to I \in D$
19	18	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
20		splcl	$⊢ (W \in Word D \land ⟨“ I ”⟩ \in Word D) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
21	17 19 20	syl2anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
22	8 21	eqeltrid	$⊢ φ \to U \in Word D$
23	22	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to U \in Word D$
24	1 2 3 4 5 6 7 8	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$
25	24	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to U : dom U \underset{1-1}{⟶} D$
26		simpr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E \in (0 ..^\|W\|)$
27	1 2 3 4 5 6 7 8	cycpmco2lem3	$⊢ φ \to \|U\| - 1 = \|W\|$
28	27	oveq2d	$⊢ φ \to (0 ..^\|U\| - 1) = (0 ..^\|W\|)$
29	28	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (0 ..^\|U\| - 1) = (0 ..^\|W\|)$
30	26 29	eleqtrrd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E \in (0 ..^\|U\| - 1)$
31	1 10 23 25 30	cycpmfv1	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (U) (U (E)) = U (E + 1)$
32	1 2 3 4 5 6 7 8	cycpmco2lem2	$⊢ φ \to U (E) = I$
33	32	fveq2d	$⊢ φ \to M (U) (U (E)) = M (U) (I)$
34	33	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (U) (U (E)) = M (U) (I)$
35	17	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W \in Word D$
36		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
37	17 36	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
38		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
39	37 38	sylib	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
40	39	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to \|W\| \in (0 \dots \|W\|)$
41		swrdfv0	$⊢ (W \in Word D \land E \in (0 ..^\|W\|) \land \|W\| \in (0 \dots \|W\|)) \to (W substr ⟨E, \|W\|⟩) (0) = W (E)$
42	35 26 40 41	syl3anc	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (W substr ⟨E, \|W\|⟩) (0) = W (E)$
43		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
44	7 43	eqeltrid	$⊢ φ \to E \in V$
45		splval	$⊢ (W \in dom M \land (E \in V \land E \in V \land ⟨“ I ”⟩ \in Word D)) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
46	4 44 44 19 45	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
47	8 46	eqtrid	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
48	47	fveq1d	$⊢ φ \to U (E + 1) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E + 1)$
49	48	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to U (E + 1) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E + 1)$
50		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
51	17 50	syl	$⊢ φ \to W prefix E \in Word D$
52		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
53	51 19 52	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
54	53	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
55		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
56	17 55	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
57	56	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W substr ⟨E, \|W\|⟩ \in Word D$
58		1z	$⊢ 1 \in ℤ$
59		fzoaddel	$⊢ (E \in (0 ..^\|W\|) \land 1 \in ℤ) \to E + 1 \in (0 + 1 ..^\|W\| + 1)$
60	58 59	mpan2	$⊢ E \in (0 ..^\|W\|) \to E + 1 \in (0 + 1 ..^\|W\| + 1)$
61		elfzolt2b	$⊢ E + 1 \in (0 + 1 ..^\|W\| + 1) \to E + 1 \in (E + 1 ..^\|W\| + 1)$
62	60 61	syl	$⊢ E \in (0 ..^\|W\|) \to E + 1 \in (E + 1 ..^\|W\| + 1)$
63	62	adantl	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E + 1 \in (E + 1 ..^\|W\| + 1)$
64		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
65	51 64	syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
66		id	$⊢ w = W \to w = W$
67		dmeq	$⊢ w = W \to dom w = dom W$
68		eqidd	$⊢ w = W \to D = D$
69	66 67 68	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
70	69	elrab3	$⊢ W \in Word D \to (W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
71	70	biimpa	$⊢ (W \in Word D \land W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}) \to W : dom W \underset{1-1}{⟶} D$
72	17 16 71	syl2anc	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
73		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
74	72 73	syl	$⊢ φ \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
75		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
76	74 75	syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
77	76 6	ffvelcdmd	$⊢ φ \to W^{-1} (J) \in dom W$
78		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
79	17 78	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
80	77 79	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
81		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
82	80 81	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
83	7 82	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
84		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
85	17 83 84	syl2anc	$⊢ φ \to \|W prefix E\| = E$
86	85	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
87	65 86	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
88	87	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
89	47	fveq2d	$⊢ φ \to \|U\| = \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\|$
90		ccatlen	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D) \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
91	53 56 90	syl2anc	$⊢ φ \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
92		swrdlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
93	17 83 39 92	syl3anc	$⊢ φ \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
94	87 93	oveq12d	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = E + 1 + (\|W\| - E)$
95	89 91 94	3eqtrd	$⊢ φ \to \|U\| = E + 1 + (\|W\| - E)$
96		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
97	96 83	sselid	$⊢ φ \to E \in ℕ_{0}$
98	97	nn0zd	$⊢ φ \to E \in ℤ$
99	98	peano2zd	$⊢ φ \to E + 1 \in ℤ$
100	99	zcnd	$⊢ φ \to E + 1 \in ℂ$
101	37	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
102	97	nn0cnd	$⊢ φ \to E \in ℂ$
103	100 101 102	addsubassd	$⊢ φ \to (E + 1) + \|W\| - E = E + 1 + (\|W\| - E)$
104		1cnd	$⊢ φ \to 1 \in ℂ$
105	102 104 101	addassd	$⊢ φ \to E + 1 + \|W\| = E + 1 + \|W\|$
106	105	oveq1d	$⊢ φ \to (E + 1) + \|W\| - E = E + (1 + \|W\|) - E$
107	95 103 106	3eqtr2d	$⊢ φ \to \|U\| = E + (1 + \|W\|) - E$
108	104 101	addcld	$⊢ φ \to 1 + \|W\| \in ℂ$
109	102 108	pncan2d	$⊢ φ \to E + (1 + \|W\|) - E = 1 + \|W\|$
110	104 101	addcomd	$⊢ φ \to 1 + \|W\| = \|W\| + 1$
111	107 109 110	3eqtrd	$⊢ φ \to \|U\| = \|W\| + 1$
112	89 111 91	3eqtr3rd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = \|W\| + 1$
113	112	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = \|W\| + 1$
114	88 113	oveq12d	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (\|(W prefix E) ++ ⟨“ I ”⟩\| ..^\|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|) = (E + 1 ..^\|W\| + 1)$
115	63 114	eleqtrrd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E + 1 \in (\|(W prefix E) ++ ⟨“ I ”⟩\| ..^\|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|)$
116		ccatval2	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D \land E + 1 \in (\|(W prefix E) ++ ⟨“ I ”⟩\| ..^\|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|)) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E + 1) = (W substr ⟨E, \|W\|⟩) (E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\|)$
117	54 57 115 116	syl3anc	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (E + 1) = (W substr ⟨E, \|W\|⟩) (E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\|)$
118	87	oveq2d	$⊢ φ \to E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1 - (E + 1)$
119	100	subidd	$⊢ φ \to E + 1 - (E + 1) = 0$
120	118 119	eqtrd	$⊢ φ \to E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\| = 0$
121	120	fveq2d	$⊢ φ \to (W substr ⟨E, \|W\|⟩) (E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\|) = (W substr ⟨E, \|W\|⟩) (0)$
122	121	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to (W substr ⟨E, \|W\|⟩) (E + 1 - \|(W prefix E) ++ ⟨“ I ”⟩\|) = (W substr ⟨E, \|W\|⟩) (0)$
123	49 117 122	3eqtrd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to U (E + 1) = (W substr ⟨E, \|W\|⟩) (0)$
124	7	fveq2i	$⊢ W (E) = W (W^{-1} (J) + 1)$
125	124	a1i	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W (E) = W (W^{-1} (J) + 1)$
126	72	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W : dom W \underset{1-1}{⟶} D$
127	7	oveq1i	$⊢ E - 1 = W^{-1} (J) + 1 - 1$
128		elfzonn0	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) \in ℕ_{0}$
129	80 128	syl	$⊢ φ \to W^{-1} (J) \in ℕ_{0}$
130	129	nn0cnd	$⊢ φ \to W^{-1} (J) \in ℂ$
131	130 104	pncand	$⊢ φ \to W^{-1} (J) + 1 - 1 = W^{-1} (J)$
132	127 131	eqtr2id	$⊢ φ \to W^{-1} (J) = E - 1$
133	132	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W^{-1} (J) = E - 1$
134		nn0p1gt0	$⊢ W^{-1} (J) \in ℕ_{0} \to 0 < W^{-1} (J) + 1$
135	129 134	syl	$⊢ φ \to 0 < W^{-1} (J) + 1$
136	135 7	breqtrrdi	$⊢ φ \to 0 < E$
137	136	gt0ne0d	$⊢ φ \to E \neq 0$
138	137	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E \neq 0$
139		fzo1fzo0n0	$⊢ E \in (1 ..^\|W\|) \leftrightarrow (E \in (0 ..^\|W\|) \land E \neq 0)$
140	26 138 139	sylanbrc	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E \in (1 ..^\|W\|)$
141		elfzo1elm1fzo0	$⊢ E \in (1 ..^\|W\|) \to E - 1 \in (0 ..^\|W\| - 1)$
142	140 141	syl	$⊢ (φ \land E \in (0 ..^\|W\|)) \to E - 1 \in (0 ..^\|W\| - 1)$
143	133 142	eqeltrd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to W^{-1} (J) \in (0 ..^\|W\| - 1)$
144	1 10 35 126 143	cycpmfv1	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (W) (W (W^{-1} (J))) = W (W^{-1} (J) + 1)$
145		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
146	72 145	syl	$⊢ φ \to W : dom W \underset{1-1 onto}{⟶} ran W$
147		f1ocnvfv2	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land J \in ran W) \to W (W^{-1} (J)) = J$
148	146 6 147	syl2anc	$⊢ φ \to W (W^{-1} (J)) = J$
149	148	fveq2d	$⊢ φ \to M (W) (W (W^{-1} (J))) = M (W) (J)$
150	149	adantr	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (W) (W (W^{-1} (J))) = M (W) (J)$
151	125 144 150	3eqtr2rd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (W) (J) = W (E)$
152	42 123 151	3eqtr4d	$⊢ (φ \land E \in (0 ..^\|W\|)) \to U (E + 1) = M (W) (J)$
153	31 34 152	3eqtr3rd	$⊢ (φ \land E \in (0 ..^\|W\|)) \to M (W) (J) = M (U) (I)$
154	149	adantr	$⊢ (φ \land E = \|W\|) \to M (W) (W (W^{-1} (J))) = M (W) (J)$
155	3	adantr	$⊢ (φ \land E = \|W\|) \to D \in V$
156	17	adantr	$⊢ (φ \land E = \|W\|) \to W \in Word D$
157	72	adantr	$⊢ (φ \land E = \|W\|) \to W : dom W \underset{1-1}{⟶} D$
158	136	adantr	$⊢ (φ \land E = \|W\|) \to 0 < E$
159		simpr	$⊢ (φ \land E = \|W\|) \to E = \|W\|$
160	158 159	breqtrd	$⊢ (φ \land E = \|W\|) \to 0 < \|W\|$
161		oveq1	$⊢ E = \|W\| \to E - 1 = \|W\| - 1$
162	132 161	sylan9eq	$⊢ (φ \land E = \|W\|) \to W^{-1} (J) = \|W\| - 1$
163	1 155 156 157 160 162	cycpmfv2	$⊢ (φ \land E = \|W\|) \to M (W) (W (W^{-1} (J))) = W (0)$
164	154 163	eqtr3d	$⊢ (φ \land E = \|W\|) \to M (W) (J) = W (0)$
165	22	adantr	$⊢ (φ \land E = \|W\|) \to U \in Word D$
166	24	adantr	$⊢ (φ \land E = \|W\|) \to U : dom U \underset{1-1}{⟶} D$
167		nn0p1gt0	$⊢ \|W\| \in ℕ_{0} \to 0 < \|W\| + 1$
168	37 167	syl	$⊢ φ \to 0 < \|W\| + 1$
169	168 111	breqtrrd	$⊢ φ \to 0 < \|U\|$
170	169	adantr	$⊢ (φ \land E = \|W\|) \to 0 < \|U\|$
171	27	adantr	$⊢ (φ \land E = \|W\|) \to \|U\| - 1 = \|W\|$
172	159 171	eqtr4d	$⊢ (φ \land E = \|W\|) \to E = \|U\| - 1$
173	1 155 165 166 170 172	cycpmfv2	$⊢ (φ \land E = \|W\|) \to M (U) (U (E)) = U (0)$
174	47	fveq1d	$⊢ φ \to U (0) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0)$
175	174	adantr	$⊢ (φ \land E = \|W\|) \to U (0) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0)$
176		nn0p1nn	$⊢ E \in ℕ_{0} \to E + 1 \in ℕ$
177	97 176	syl	$⊢ φ \to E + 1 \in ℕ$
178		lbfzo0	$⊢ 0 \in (0 ..^E + 1) \leftrightarrow E + 1 \in ℕ$
179	177 178	sylibr	$⊢ φ \to 0 \in (0 ..^E + 1)$
180	87	oveq2d	$⊢ φ \to (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|) = (0 ..^E + 1)$
181	179 180	eleqtrrd	$⊢ φ \to 0 \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)$
182		ccatval1	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D \land 0 \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = ((W prefix E) ++ ⟨“ I ”⟩) (0)$
183	53 56 181 182	syl3anc	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = ((W prefix E) ++ ⟨“ I ”⟩) (0)$
184		nn0p1nn	$⊢ W^{-1} (J) \in ℕ_{0} \to W^{-1} (J) + 1 \in ℕ$
185	129 184	syl	$⊢ φ \to W^{-1} (J) + 1 \in ℕ$
186	7 185	eqeltrid	$⊢ φ \to E \in ℕ$
187		lbfzo0	$⊢ 0 \in (0 ..^E) \leftrightarrow E \in ℕ$
188	186 187	sylibr	$⊢ φ \to 0 \in (0 ..^E)$
189	85	oveq2d	$⊢ φ \to (0 ..^\|W prefix E\|) = (0 ..^E)$
190	188 189	eleqtrrd	$⊢ φ \to 0 \in (0 ..^\|W prefix E\|)$
191		ccatval1	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D \land 0 \in (0 ..^\|W prefix E\|)) \to ((W prefix E) ++ ⟨“ I ”⟩) (0) = (W prefix E) (0)$
192	51 19 190 191	syl3anc	$⊢ φ \to ((W prefix E) ++ ⟨“ I ”⟩) (0) = (W prefix E) (0)$
193		fzne1	$⊢ (E \in (0 \dots \|W\|) \land E \neq 0) \to E \in (0 + 1 \dots \|W\|)$
194	83 137 193	syl2anc	$⊢ φ \to E \in (0 + 1 \dots \|W\|)$
195		0p1e1	$⊢ 0 + 1 = 1$
196	195	oveq1i	$⊢ (0 + 1 \dots \|W\|) = (1 \dots \|W\|)$
197	194 196	eleqtrdi	$⊢ φ \to E \in (1 \dots \|W\|)$
198		pfxfv0	$⊢ (W \in Word D \land E \in (1 \dots \|W\|)) \to (W prefix E) (0) = W (0)$
199	17 197 198	syl2anc	$⊢ φ \to (W prefix E) (0) = W (0)$
200	183 192 199	3eqtrd	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = W (0)$
201	200	adantr	$⊢ (φ \land E = \|W\|) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = W (0)$
202	173 175 201	3eqtrd	$⊢ (φ \land E = \|W\|) \to M (U) (U (E)) = W (0)$
203	33	adantr	$⊢ (φ \land E = \|W\|) \to M (U) (U (E)) = M (U) (I)$
204	164 202 203	3eqtr2d	$⊢ (φ \land E = \|W\|) \to M (W) (J) = M (U) (I)$
205		elfzr	$⊢ E \in (0 \dots \|W\|) \to (E \in (0 ..^\|W\|) \lor E = \|W\|)$
206	83 205	syl	$⊢ φ \to (E \in (0 ..^\|W\|) \lor E = \|W\|)$
207	153 204 206	mpjaodan	$⊢ φ \to M (W) (J) = M (U) (I)$
208	9 207	eqtrd	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (U) (I)$

Metamath Proof Explorer

Theorem cycpmco2lem4

Proof