cycpmco2lem5

	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 ”⟩⟩$
	cycpmco2lem.1	$⊢ φ \to K \in ran W$
	cycpmco2lem5.1	$⊢ φ \to U^{-1} (K) = \|U\| - 1$
Assertion	cycpmco2lem5	$⊢ φ \to M (U) (K) = M (W) (K)$

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		cycpmco2lem.1	$⊢ φ \to K \in ran W$
10		cycpmco2lem5.1	$⊢ φ \to U^{-1} (K) = \|U\| - 1$
11	9	adantr	$⊢ (φ \land \|W\| = E) \to K \in ran W$
12		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
13	7 12	eqeltrid	$⊢ φ \to E \in V$
14	5	eldifad	$⊢ φ \to I \in D$
15	14	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
16		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\|⟩)$
17	4 13 13 15 16	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
18	8 17	syl5eq	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
19	18	fveq2d	$⊢ φ \to \|U\| = \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\|$
20		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
21		eqid	$⊢ {Base}_{S} = {Base}_{S}$
22	1 2 21	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
23	3 22	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
24	23	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
25	4 24	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
26	20 25	sselid	$⊢ φ \to W \in Word D$
27		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
28	26 27	syl	$⊢ φ \to W prefix E \in Word D$
29		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
30	28 15 29	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
31		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
32	26 31	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
33		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\|⟩\|$
34	30 32 33	syl2anc	$⊢ φ \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
35		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
36	28 35	syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
37		id	$⊢ w = W \to w = W$
38		dmeq	$⊢ w = W \to dom w = dom W$
39		eqidd	$⊢ w = W \to D = D$
40	37 38 39	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
41	40	elrab	$⊢ W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
42	25 41	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
43	42	simprd	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
44		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
45	43 44	syl	$⊢ φ \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
46		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
47	45 46	syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
48	47 6	ffvelrnd	$⊢ φ \to W^{-1} (J) \in dom W$
49		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
50	26 49	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
51	48 50	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
52		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
53	51 52	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
54	7 53	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
55		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
56	26 54 55	syl2anc	$⊢ φ \to \|W prefix E\| = E$
57	56	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
58	36 57	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
59		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
60	26 59	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
61		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
62	60 61	sylib	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
63		swrdlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
64	26 54 62 63	syl3anc	$⊢ φ \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
65	58 64	oveq12d	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = E + 1 + (\|W\| - E)$
66	19 34 65	3eqtrd	$⊢ φ \to \|U\| = E + 1 + (\|W\| - E)$
67		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
68	67 54	sselid	$⊢ φ \to E \in ℕ_{0}$
69	68	nn0zd	$⊢ φ \to E \in ℤ$
70	69	peano2zd	$⊢ φ \to E + 1 \in ℤ$
71	70	zcnd	$⊢ φ \to E + 1 \in ℂ$
72	60	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
73	68	nn0cnd	$⊢ φ \to E \in ℂ$
74	71 72 73	addsubassd	$⊢ φ \to (E + 1) + \|W\| - E = E + 1 + (\|W\| - E)$
75		1cnd	$⊢ φ \to 1 \in ℂ$
76	73 75 72	addassd	$⊢ φ \to E + 1 + \|W\| = E + 1 + \|W\|$
77	76	oveq1d	$⊢ φ \to (E + 1) + \|W\| - E = E + (1 + \|W\|) - E$
78	66 74 77	3eqtr2d	$⊢ φ \to \|U\| = E + (1 + \|W\|) - E$
79	75 72	addcld	$⊢ φ \to 1 + \|W\| \in ℂ$
80	73 79	pncan2d	$⊢ φ \to E + (1 + \|W\|) - E = 1 + \|W\|$
81	75 72	addcomd	$⊢ φ \to 1 + \|W\| = \|W\| + 1$
82	78 80 81	3eqtrd	$⊢ φ \to \|U\| = \|W\| + 1$
83		oveq1	$⊢ \|W\| = E \to \|W\| + 1 = E + 1$
84	82 83	sylan9eq	$⊢ (φ \land \|W\| = E) \to \|U\| = E + 1$
85	84	oveq1d	$⊢ (φ \land \|W\| = E) \to \|U\| - 1 = E + 1 - 1$
86	73 75	pncand	$⊢ φ \to E + 1 - 1 = E$
87	86	adantr	$⊢ (φ \land \|W\| = E) \to E + 1 - 1 = E$
88	85 87	eqtrd	$⊢ (φ \land \|W\| = E) \to \|U\| - 1 = E$
89	88	fveq2d	$⊢ (φ \land \|W\| = E) \to U (\|U\| - 1) = U (E)$
90	10	fveq2d	$⊢ φ \to U (U^{-1} (K)) = U (\|U\| - 1)$
91	1 2 3 4 5 6 7 8	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$
92		f1f1orn	$⊢ U : dom U \underset{1-1}{⟶} D \to U : dom U \underset{1-1 onto}{⟶} ran U$
93	91 92	syl	$⊢ φ \to U : dom U \underset{1-1 onto}{⟶} ran U$
94		ssun1	$⊢ ran W \subseteq ran W \cup \{I\}$
95	1 2 3 4 5 6 7 8	cycpmco2rn	$⊢ φ \to ran U = ran W \cup \{I\}$
96	94 95	sseqtrrid	$⊢ φ \to ran W \subseteq ran U$
97	96	sselda	$⊢ (φ \land K \in ran W) \to K \in ran U$
98		f1ocnvfv2	$⊢ (U : dom U \underset{1-1 onto}{⟶} ran U \land K \in ran U) \to U (U^{-1} (K)) = K$
99	93 97 98	syl2an2r	$⊢ (φ \land K \in ran W) \to U (U^{-1} (K)) = K$
100	9 99	mpdan	$⊢ φ \to U (U^{-1} (K)) = K$
101	90 100	eqtr3d	$⊢ φ \to U (\|U\| - 1) = K$
102	101	adantr	$⊢ (φ \land \|W\| = E) \to U (\|U\| - 1) = K$
103	1 2 3 4 5 6 7 8	cycpmco2lem2	$⊢ φ \to U (E) = I$
104	103	adantr	$⊢ (φ \land \|W\| = E) \to U (E) = I$
105	89 102 104	3eqtr3d	$⊢ (φ \land \|W\| = E) \to K = I$
106	5	eldifbd	$⊢ φ \to \neg I \in ran W$
107	106	adantr	$⊢ (φ \land \|W\| = E) \to \neg I \in ran W$
108	105 107	eqneltrd	$⊢ (φ \land \|W\| = E) \to \neg K \in ran W$
109	11 108	pm2.21dd	$⊢ (φ \land \|W\| = E) \to M (U) (U (\|U\| - 1)) = M (W) (U (\|U\| - 1))$
110		splcl	$⊢ (W \in Word D \land ⟨“ I ”⟩ \in Word D) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
111	26 15 110	syl2anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
112	8 111	eqeltrid	$⊢ φ \to U \in Word D$
113		nn0p1gt0	$⊢ \|W\| \in ℕ_{0} \to 0 < \|W\| + 1$
114	60 113	syl	$⊢ φ \to 0 < \|W\| + 1$
115	114 82	breqtrrd	$⊢ φ \to 0 < \|U\|$
116		eqidd	$⊢ φ \to \|U\| - 1 = \|U\| - 1$
117	1 3 112 91 115 116	cycpmfv2	$⊢ φ \to M (U) (U (\|U\| - 1)) = U (0)$
118	117	adantr	$⊢ (φ \land \|W\| \neq E) \to M (U) (U (\|U\| - 1)) = U (0)$
119		f1f	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W ⟶ D$
120	43 119	syl	$⊢ φ \to W : dom W ⟶ D$
121	120	frnd	$⊢ φ \to ran W \subseteq D$
122	3 121	ssexd	$⊢ φ \to ran W \in V$
123	6	ne0d	$⊢ φ \to ran W \neq \emptyset$
124		hashgt0	$⊢ (ran W \in V \land ran W \neq \emptyset) \to 0 < \|ran W\|$
125	122 123 124	syl2anc	$⊢ φ \to 0 < \|ran W\|$
126	4	dmexd	$⊢ φ \to dom W \in V$
127		hashf1rn	$⊢ (dom W \in V \land W : dom W \underset{1-1}{⟶} D) \to \|W\| = \|ran W\|$
128	126 43 127	syl2anc	$⊢ φ \to \|W\| = \|ran W\|$
129	125 128	breqtrrd	$⊢ φ \to 0 < \|W\|$
130		eqidd	$⊢ φ \to \|W\| - 1 = \|W\| - 1$
131	1 3 26 43 129 130	cycpmfv2	$⊢ φ \to M (W) (W (\|W\| - 1)) = W (0)$
132	131	adantr	$⊢ (φ \land \|W\| \neq E) \to M (W) (W (\|W\| - 1)) = W (0)$
133	8	a1i	$⊢ (φ \land \|W\| \neq E) \to U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
134	1 2 3 4 5 6 7 8	cycpmco2lem3	$⊢ φ \to \|U\| - 1 = \|W\|$
135	73 75	addcomd	$⊢ φ \to E + 1 = 1 + E$
136	135	oveq2d	$⊢ φ \to (\|W\| - 1 - E) + E + 1 = (\|W\| - 1 - E) + 1 + E$
137	72 75	subcld	$⊢ φ \to \|W\| - 1 \in ℂ$
138	137 73 75	nppcan3d	$⊢ φ \to (\|W\| - 1 - E) + 1 + E = \|W\| - 1 + 1$
139	72 75	npcand	$⊢ φ \to \|W\| - 1 + 1 = \|W\|$
140	136 138 139	3eqtrd	$⊢ φ \to (\|W\| - 1 - E) + E + 1 = \|W\|$
141	134 140	eqtr4d	$⊢ φ \to \|U\| - 1 = (\|W\| - 1 - E) + E + 1$
142	141	adantr	$⊢ (φ \land \|W\| \neq E) \to \|U\| - 1 = (\|W\| - 1 - E) + E + 1$
143	133 142	fveq12d	$⊢ (φ \land \|W\| \neq E) \to U (\|U\| - 1) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((\|W\| - 1 - E) + E + 1)$
144	26	adantr	$⊢ (φ \land \|W\| \neq E) \to W \in Word D$
145		nn0fz0	$⊢ E \in ℕ_{0} \leftrightarrow E \in (0 \dots E)$
146	68 145	sylib	$⊢ φ \to E \in (0 \dots E)$
147	146	adantr	$⊢ (φ \land \|W\| \neq E) \to E \in (0 \dots E)$
148	54	adantr	$⊢ (φ \land \|W\| \neq E) \to E \in (0 \dots \|W\|)$
149	15	adantr	$⊢ (φ \land \|W\| \neq E) \to ⟨“ I ”⟩ \in Word D$
150	72	adantr	$⊢ (φ \land \|W\| \neq E) \to \|W\| \in ℂ$
151		1cnd	$⊢ (φ \land \|W\| \neq E) \to 1 \in ℂ$
152	73	adantr	$⊢ (φ \land \|W\| \neq E) \to E \in ℂ$
153	150 151 152	sub32d	$⊢ (φ \land \|W\| \neq E) \to \|W\| - 1 - E = \|W\| - E - 1$
154		fznn0sub	$⊢ E \in (0 \dots \|W\|) \to \|W\| - E \in ℕ_{0}$
155	54 154	syl	$⊢ φ \to \|W\| - E \in ℕ_{0}$
156	155	adantr	$⊢ (φ \land \|W\| \neq E) \to \|W\| - E \in ℕ_{0}$
157		simpr	$⊢ (φ \land \|W\| \neq E) \to \|W\| \neq E$
158	150 152 156 157	subne0nn	$⊢ (φ \land \|W\| \neq E) \to \|W\| - E \in ℕ$
159		fzo0end	$⊢ \|W\| - E \in ℕ \to \|W\| - E - 1 \in (0 ..^\|W\| - E)$
160	158 159	syl	$⊢ (φ \land \|W\| \neq E) \to \|W\| - E - 1 \in (0 ..^\|W\| - E)$
161	153 160	eqeltrd	$⊢ (φ \land \|W\| \neq E) \to \|W\| - 1 - E \in (0 ..^\|W\| - E)$
162		s1len	$⊢ \|⟨“ I ”⟩\| = 1$
163	162	eqcomi	$⊢ 1 = \|⟨“ I ”⟩\|$
164	163	oveq2i	$⊢ E + 1 = E + \|⟨“ I ”⟩\|$
165	164	a1i	$⊢ (φ \land \|W\| \neq E) \to E + 1 = E + \|⟨“ I ”⟩\|$
166	144 147 148 149 161 165	splfv3	$⊢ (φ \land \|W\| \neq E) \to (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((\|W\| - 1 - E) + E + 1) = W ((\|W\| - 1) - E + E)$
167	137 73	npcand	$⊢ φ \to (\|W\| - 1) - E + E = \|W\| - 1$
168	167	fveq2d	$⊢ φ \to W ((\|W\| - 1) - E + E) = W (\|W\| - 1)$
169	168	adantr	$⊢ (φ \land \|W\| \neq E) \to W ((\|W\| - 1) - E + E) = W (\|W\| - 1)$
170	143 166 169	3eqtrd	$⊢ (φ \land \|W\| \neq E) \to U (\|U\| - 1) = W (\|W\| - 1)$
171	170	fveq2d	$⊢ (φ \land \|W\| \neq E) \to M (W) (U (\|U\| - 1)) = M (W) (W (\|W\| - 1))$
172	18	fveq1d	$⊢ φ \to U (0) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0)$
173		nn0p1nn	$⊢ E \in ℕ_{0} \to E + 1 \in ℕ$
174	68 173	syl	$⊢ φ \to E + 1 \in ℕ$
175		lbfzo0	$⊢ 0 \in (0 ..^E + 1) \leftrightarrow E + 1 \in ℕ$
176	174 175	sylibr	$⊢ φ \to 0 \in (0 ..^E + 1)$
177	58	oveq2d	$⊢ φ \to (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|) = (0 ..^E + 1)$
178	176 177	eleqtrrd	$⊢ φ \to 0 \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)$
179		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)$
180	30 32 178 179	syl3anc	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = ((W prefix E) ++ ⟨“ I ”⟩) (0)$
181		elfzonn0	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) \in ℕ_{0}$
182	51 181	syl	$⊢ φ \to W^{-1} (J) \in ℕ_{0}$
183		nn0p1nn	$⊢ W^{-1} (J) \in ℕ_{0} \to W^{-1} (J) + 1 \in ℕ$
184	182 183	syl	$⊢ φ \to W^{-1} (J) + 1 \in ℕ$
185	7 184	eqeltrid	$⊢ φ \to E \in ℕ$
186		lbfzo0	$⊢ 0 \in (0 ..^E) \leftrightarrow E \in ℕ$
187	185 186	sylibr	$⊢ φ \to 0 \in (0 ..^E)$
188	56	oveq2d	$⊢ φ \to (0 ..^\|W prefix E\|) = (0 ..^E)$
189	187 188	eleqtrrd	$⊢ φ \to 0 \in (0 ..^\|W prefix E\|)$
190		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)$
191	28 15 189 190	syl3anc	$⊢ φ \to ((W prefix E) ++ ⟨“ I ”⟩) (0) = (W prefix E) (0)$
192		nn0p1gt0	$⊢ W^{-1} (J) \in ℕ_{0} \to 0 < W^{-1} (J) + 1$
193	182 192	syl	$⊢ φ \to 0 < W^{-1} (J) + 1$
194	193 7	breqtrrdi	$⊢ φ \to 0 < E$
195	194	gt0ne0d	$⊢ φ \to E \neq 0$
196		fzne1	$⊢ (E \in (0 \dots \|W\|) \land E \neq 0) \to E \in (0 + 1 \dots \|W\|)$
197	54 195 196	syl2anc	$⊢ φ \to E \in (0 + 1 \dots \|W\|)$
198		0p1e1	$⊢ 0 + 1 = 1$
199	198	oveq1i	$⊢ (0 + 1 \dots \|W\|) = (1 \dots \|W\|)$
200	197 199	eleqtrdi	$⊢ φ \to E \in (1 \dots \|W\|)$
201		pfxfv0	$⊢ (W \in Word D \land E \in (1 \dots \|W\|)) \to (W prefix E) (0) = W (0)$
202	26 200 201	syl2anc	$⊢ φ \to (W prefix E) (0) = W (0)$
203	180 191 202	3eqtrd	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (0) = W (0)$
204	172 203	eqtrd	$⊢ φ \to U (0) = W (0)$
205	204	adantr	$⊢ (φ \land \|W\| \neq E) \to U (0) = W (0)$
206	132 171 205	3eqtr4rd	$⊢ (φ \land \|W\| \neq E) \to U (0) = M (W) (U (\|U\| - 1))$
207	118 206	eqtrd	$⊢ (φ \land \|W\| \neq E) \to M (U) (U (\|U\| - 1)) = M (W) (U (\|U\| - 1))$
208	109 207	pm2.61dane	$⊢ φ \to M (U) (U (\|U\| - 1)) = M (W) (U (\|U\| - 1))$
209	101	fveq2d	$⊢ φ \to M (U) (U (\|U\| - 1)) = M (U) (K)$
210	101	fveq2d	$⊢ φ \to M (W) (U (\|U\| - 1)) = M (W) (K)$
211	208 209 210	3eqtr3d	$⊢ φ \to M (U) (K) = M (W) (K)$

Metamath Proof Explorer

Theorem cycpmco2lem5

Proof