Metamath Proof Explorer

Theorem cycpmco2lem4

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ⊢ M = toCyc ⁡ D
cycpmco2.s ⊢ S = SymGrp ⁡ D
cycpmco2.d ⊢ φ → D ∈ V
cycpmco2.w ⊢ φ → W ∈ dom ⁡ M
cycpmco2.i ⊢ φ → I ∈ D ∖ ran ⁡ W
cycpmco2.j ⊢ φ → J ∈ ran ⁡ W
cycpmco2.e ⊢ E = W -1 ⁡ J + 1
cycpmco2.1 ⊢ U = W splice E E ⟨“ I ”⟩
Assertion cycpmco2lem4 ⊢ φ → M ⁡ W ⁡ M ⁡ ⟨“ IJ ”⟩ ⁡ I = M ⁡ U ⁡ I

Proof

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