cycpmco2lem6

	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$
	cycpmco2lem6.2	$⊢ φ \to K \neq I$
	cycpmco2lem6.1	$⊢ φ \to U^{-1} (K) \in (E ..^\|U\| - 1)$
Assertion	cycpmco2lem6	$⊢ φ \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		cycpmco2lem6.2	$⊢ φ \to K \neq I$
11		cycpmco2lem6.1	$⊢ φ \to U^{-1} (K) \in (E ..^\|U\| - 1)$
12		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14	1 2 13	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
15	3 14	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
16	15	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
17	4 16	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
18	12 17	sselid	$⊢ φ \to W \in Word D$
19	5	eldifad	$⊢ φ \to I \in D$
20	19	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
21		splcl	$⊢ (W \in Word D \land ⟨“ I ”⟩ \in Word D) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
22	18 20 21	syl2anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
23	8 22	eqeltrid	$⊢ φ \to U \in Word D$
24	1 2 3 4 5 6 7 8	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$
25		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
26		id	$⊢ w = W \to w = W$
27		dmeq	$⊢ w = W \to dom w = dom W$
28		eqidd	$⊢ w = W \to D = D$
29	26 27 28	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
30	29	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)$
31	17 30	sylib	$⊢ φ \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
32	31	simprd	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
33		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
34		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
35	32 33 34	3syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
36	35 6	ffvelcdmd	$⊢ φ \to W^{-1} (J) \in dom W$
37		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
38	18 37	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
39	36 38	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
40		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
41	39 40	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
42	7 41	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
43	25 42	sselid	$⊢ φ \to E \in ℕ_{0}$
44		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
45	43 44	eleqtrdi	$⊢ φ \to E \in ℤ_{\geq 0}$
46		fzoss1	$⊢ E \in ℤ_{\geq 0} \to (E ..^\|U\| - 1) \subseteq (0 ..^\|U\| - 1)$
47	45 46	syl	$⊢ φ \to (E ..^\|U\| - 1) \subseteq (0 ..^\|U\| - 1)$
48	47 11	sseldd	$⊢ φ \to U^{-1} (K) \in (0 ..^\|U\| - 1)$
49	1 3 23 24 48	cycpmfv1	$⊢ φ \to M (U) (U (U^{-1} (K))) = U (U^{-1} (K) + 1)$
50		f1f1orn	$⊢ U : dom U \underset{1-1}{⟶} D \to U : dom U \underset{1-1 onto}{⟶} ran U$
51	24 50	syl	$⊢ φ \to U : dom U \underset{1-1 onto}{⟶} ran U$
52		ssun1	$⊢ ran W \subseteq ran W \cup \{I\}$
53	1 2 3 4 5 6 7 8	cycpmco2rn	$⊢ φ \to ran U = ran W \cup \{I\}$
54	52 53	sseqtrrid	$⊢ φ \to ran W \subseteq ran U$
55	54	sselda	$⊢ (φ \land K \in ran W) \to K \in ran U$
56		f1ocnvfv2	$⊢ (U : dom U \underset{1-1 onto}{⟶} ran U \land K \in ran U) \to U (U^{-1} (K)) = K$
57	51 55 56	syl2an2r	$⊢ (φ \land K \in ran W) \to U (U^{-1} (K)) = K$
58	9 57	mpdan	$⊢ φ \to U (U^{-1} (K)) = K$
59	58	fveq2d	$⊢ φ \to M (U) (U (U^{-1} (K))) = M (U) (K)$
60	8	a1i	$⊢ φ \to U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
61		fzossz	$⊢ (E ..^\|U\| - 1) \subseteq ℤ$
62	61 11	sselid	$⊢ φ \to U^{-1} (K) \in ℤ$
63	62	zcnd	$⊢ φ \to U^{-1} (K) \in ℂ$
64	43	nn0cnd	$⊢ φ \to E \in ℂ$
65		1cnd	$⊢ φ \to 1 \in ℂ$
66	63 64 65	nppcan3d	$⊢ φ \to (U^{-1} (K) - E) + 1 + E = U^{-1} (K) + 1$
67	66	eqcomd	$⊢ φ \to U^{-1} (K) + 1 = (U^{-1} (K) - E) + 1 + E$
68	60 67	fveq12d	$⊢ φ \to U (U^{-1} (K) + 1) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - E) + 1 + E)$
69	49 59 68	3eqtr3d	$⊢ φ \to M (U) (K) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - E) + 1 + E)$
70	63 64	npcand	$⊢ φ \to U^{-1} (K) - E + E = U^{-1} (K)$
71	70	fveq2d	$⊢ φ \to W (U^{-1} (K) - E + E) = W (U^{-1} (K))$
72		nn0fz0	$⊢ E \in ℕ_{0} \leftrightarrow E \in (0 \dots E)$
73	43 72	sylib	$⊢ φ \to E \in (0 \dots E)$
74		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
75	18 74	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
76	75	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
77		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
78	7 77	eqeltrid	$⊢ φ \to E \in V$
79		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\|⟩)$
80	4 78 78 20 79	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
81	8 80	eqtrid	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
82	81	fveq2d	$⊢ φ \to \|U\| = \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\|$
83		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
84	18 83	syl	$⊢ φ \to W prefix E \in Word D$
85		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
86	84 20 85	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
87		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
88	18 87	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
89		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\|⟩\|$
90	86 88 89	syl2anc	$⊢ φ \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
91		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
92	18 83 91	3syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
93		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
94	18 42 93	syl2anc	$⊢ φ \to \|W prefix E\| = E$
95	94	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
96	92 95	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
97		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
98	75 97	sylib	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
99		swrdlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
100	18 42 98 99	syl3anc	$⊢ φ \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
101	96 100	oveq12d	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = E + 1 + (\|W\| - E)$
102	82 90 101	3eqtrd	$⊢ φ \to \|U\| = E + 1 + (\|W\| - E)$
103	43	nn0zd	$⊢ φ \to E \in ℤ$
104	103	peano2zd	$⊢ φ \to E + 1 \in ℤ$
105	104	zcnd	$⊢ φ \to E + 1 \in ℂ$
106	105 76 64	addsubassd	$⊢ φ \to (E + 1) + \|W\| - E = E + 1 + (\|W\| - E)$
107	64 65 76	addassd	$⊢ φ \to E + 1 + \|W\| = E + 1 + \|W\|$
108	107	oveq1d	$⊢ φ \to (E + 1) + \|W\| - E = E + (1 + \|W\|) - E$
109	102 106 108	3eqtr2d	$⊢ φ \to \|U\| = E + (1 + \|W\|) - E$
110	65 76	addcld	$⊢ φ \to 1 + \|W\| \in ℂ$
111	64 110	pncan2d	$⊢ φ \to E + (1 + \|W\|) - E = 1 + \|W\|$
112	65 76	addcomd	$⊢ φ \to 1 + \|W\| = \|W\| + 1$
113	109 111 112	3eqtrd	$⊢ φ \to \|U\| = \|W\| + 1$
114	76 65 113	mvrraddd	$⊢ φ \to \|U\| - 1 = \|W\|$
115	114	oveq2d	$⊢ φ \to (E ..^\|U\| - 1) = (E ..^\|W\|)$
116	11 115	eleqtrd	$⊢ φ \to U^{-1} (K) \in (E ..^\|W\|)$
117		fzosubel	$⊢ (U^{-1} (K) \in (E ..^\|W\|) \land E \in ℤ) \to U^{-1} (K) - E \in (E - E ..^\|W\| - E)$
118	116 103 117	syl2anc	$⊢ φ \to U^{-1} (K) - E \in (E - E ..^\|W\| - E)$
119	64	subidd	$⊢ φ \to E - E = 0$
120	119	oveq1d	$⊢ φ \to (E - E ..^\|W\| - E) = (0 ..^\|W\| - E)$
121	118 120	eleqtrd	$⊢ φ \to U^{-1} (K) - E \in (0 ..^\|W\| - E)$
122	65 64	addcomd	$⊢ φ \to 1 + E = E + 1$
123		s1len	$⊢ \|⟨“ I ”⟩\| = 1$
124	123	oveq2i	$⊢ E + \|⟨“ I ”⟩\| = E + 1$
125	122 124	eqtr4di	$⊢ φ \to 1 + E = E + \|⟨“ I ”⟩\|$
126	18 73 42 20 121 125	splfv3	$⊢ φ \to (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - E) + 1 + E) = W (U^{-1} (K) - E + E)$
127	114	oveq1d	$⊢ φ \to \|U\| - 1 - 1 = \|W\| - 1$
128	127	oveq2d	$⊢ φ \to (E ..^\|U\| - 1 - 1) = (E ..^\|W\| - 1)$
129		fzoss1	$⊢ E \in ℤ_{\geq 0} \to (E ..^\|W\| - 1) \subseteq (0 ..^\|W\| - 1)$
130	45 129	syl	$⊢ φ \to (E ..^\|W\| - 1) \subseteq (0 ..^\|W\| - 1)$
131	128 130	eqsstrd	$⊢ φ \to (E ..^\|U\| - 1 - 1) \subseteq (0 ..^\|W\| - 1)$
132		f1ocnvdm	$⊢ (U : dom U \underset{1-1 onto}{⟶} ran U \land K \in ran U) \to U^{-1} (K) \in dom U$
133	51 55 132	syl2an2r	$⊢ (φ \land K \in ran W) \to U^{-1} (K) \in dom U$
134	9 133	mpdan	$⊢ φ \to U^{-1} (K) \in dom U$
135	75	nn0zd	$⊢ φ \to \|W\| \in ℤ$
136	135	peano2zd	$⊢ φ \to \|W\| + 1 \in ℤ$
137		elfzonn0	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) \in ℕ_{0}$
138		nn0p1nn	$⊢ W^{-1} (J) \in ℕ_{0} \to W^{-1} (J) + 1 \in ℕ$
139	39 137 138	3syl	$⊢ φ \to W^{-1} (J) + 1 \in ℕ$
140	7 139	eqeltrid	$⊢ φ \to E \in ℕ$
141	140	nnred	$⊢ φ \to E \in ℝ$
142	135	zred	$⊢ φ \to \|W\| \in ℝ$
143		1red	$⊢ φ \to 1 \in ℝ$
144		elfzle2	$⊢ E \in (0 \dots \|W\|) \to E \leq \|W\|$
145	42 144	syl	$⊢ φ \to E \leq \|W\|$
146	141 142 143 145	leadd1dd	$⊢ φ \to E + 1 \leq \|W\| + 1$
147		eluz2	$⊢ \|W\| + 1 \in ℤ_{\geq (E + 1)} \leftrightarrow (E + 1 \in ℤ \land \|W\| + 1 \in ℤ \land E + 1 \leq \|W\| + 1)$
148	104 136 146 147	syl3anbrc	$⊢ φ \to \|W\| + 1 \in ℤ_{\geq (E + 1)}$
149		fzoss2	$⊢ \|W\| + 1 \in ℤ_{\geq (E + 1)} \to (0 ..^E + 1) \subseteq (0 ..^\|W\| + 1)$
150	148 149	syl	$⊢ φ \to (0 ..^E + 1) \subseteq (0 ..^\|W\| + 1)$
151		fzonn0p1	$⊢ E \in ℕ_{0} \to E \in (0 ..^E + 1)$
152	43 151	syl	$⊢ φ \to E \in (0 ..^E + 1)$
153	150 152	sseldd	$⊢ φ \to E \in (0 ..^\|W\| + 1)$
154	113	oveq2d	$⊢ φ \to (0 ..^\|U\|) = (0 ..^\|W\| + 1)$
155	153 154	eleqtrrd	$⊢ φ \to E \in (0 ..^\|U\|)$
156		wrddm	$⊢ U \in Word D \to dom U = (0 ..^\|U\|)$
157	23 156	syl	$⊢ φ \to dom U = (0 ..^\|U\|)$
158	155 157	eleqtrrd	$⊢ φ \to E \in dom U$
159	1 2 3 4 5 6 7 8	cycpmco2lem2	$⊢ φ \to U (E) = I$
160	10 58 159	3netr4d	$⊢ φ \to U (U^{-1} (K)) \neq U (E)$
161		f1fveq	$⊢ (U : dom U \underset{1-1}{⟶} D \land (U^{-1} (K) \in dom U \land E \in dom U)) \to (U (U^{-1} (K)) = U (E) \leftrightarrow U^{-1} (K) = E)$
162	161	necon3bid	$⊢ (U : dom U \underset{1-1}{⟶} D \land (U^{-1} (K) \in dom U \land E \in dom U)) \to (U (U^{-1} (K)) \neq U (E) \leftrightarrow U^{-1} (K) \neq E)$
163	162	biimp3a	$⊢ (U : dom U \underset{1-1}{⟶} D \land (U^{-1} (K) \in dom U \land E \in dom U) \land U (U^{-1} (K)) \neq U (E)) \to U^{-1} (K) \neq E$
164	24 134 158 160 163	syl121anc	$⊢ φ \to U^{-1} (K) \neq E$
165		fzom1ne1	$⊢ (U^{-1} (K) \in (E ..^\|U\| - 1) \land U^{-1} (K) \neq E) \to U^{-1} (K) - 1 \in (E ..^\|U\| - 1 - 1)$
166	11 164 165	syl2anc	$⊢ φ \to U^{-1} (K) - 1 \in (E ..^\|U\| - 1 - 1)$
167	131 166	sseldd	$⊢ φ \to U^{-1} (K) - 1 \in (0 ..^\|W\| - 1)$
168	1 3 18 32 167	cycpmfv1	$⊢ φ \to M (W) (W (U^{-1} (K) - 1)) = W (U^{-1} (K) - 1 + 1)$
169	63 65 64	subsub4d	$⊢ φ \to U^{-1} (K) - 1 - E = U^{-1} (K) - (1 + E)$
170	169	oveq1d	$⊢ φ \to (U^{-1} (K) - 1 - E) + 1 + E = (U^{-1} (K) - (1 + E)) + 1 + E$
171	65 64	addcld	$⊢ φ \to 1 + E \in ℂ$
172	63 171	npcand	$⊢ φ \to (U^{-1} (K) - (1 + E)) + 1 + E = U^{-1} (K)$
173	170 172	eqtr2d	$⊢ φ \to U^{-1} (K) = (U^{-1} (K) - 1 - E) + 1 + E$
174	60 173	fveq12d	$⊢ φ \to U (U^{-1} (K)) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - 1 - E) + 1 + E)$
175	64 76	pncan3d	$⊢ φ \to E + \|W\| - E = \|W\|$
176	114 135	eqeltrd	$⊢ φ \to \|U\| - 1 \in ℤ$
177		1zzd	$⊢ φ \to 1 \in ℤ$
178	176 177	zsubcld	$⊢ φ \to \|U\| - 1 - 1 \in ℤ$
179	178	zred	$⊢ φ \to \|U\| - 1 - 1 \in ℝ$
180	114 142	eqeltrd	$⊢ φ \to \|U\| - 1 \in ℝ$
181	180	ltm1d	$⊢ φ \to \|U\| - 1 - 1 < \|U\| - 1$
182	181 114	breqtrd	$⊢ φ \to \|U\| - 1 - 1 < \|W\|$
183	179 142 182	ltled	$⊢ φ \to \|U\| - 1 - 1 \leq \|W\|$
184		eluz1	$⊢ \|U\| - 1 - 1 \in ℤ \to (\|W\| \in ℤ_{\geq (\|U\| - 1 - 1)} \leftrightarrow (\|W\| \in ℤ \land \|U\| - 1 - 1 \leq \|W\|))$
185	184	biimpar	$⊢ (\|U\| - 1 - 1 \in ℤ \land (\|W\| \in ℤ \land \|U\| - 1 - 1 \leq \|W\|)) \to \|W\| \in ℤ_{\geq (\|U\| - 1 - 1)}$
186	178 135 183 185	syl12anc	$⊢ φ \to \|W\| \in ℤ_{\geq (\|U\| - 1 - 1)}$
187	175 186	eqeltrd	$⊢ φ \to E + \|W\| - E \in ℤ_{\geq (\|U\| - 1 - 1)}$
188		fzoss2	$⊢ E + \|W\| - E \in ℤ_{\geq (\|U\| - 1 - 1)} \to (E ..^\|U\| - 1 - 1) \subseteq (E ..^E + \|W\| - E)$
189	187 188	syl	$⊢ φ \to (E ..^\|U\| - 1 - 1) \subseteq (E ..^E + \|W\| - E)$
190	189 166	sseldd	$⊢ φ \to U^{-1} (K) - 1 \in (E ..^E + \|W\| - E)$
191	135 103	zsubcld	$⊢ φ \to \|W\| - E \in ℤ$
192		fzosubel3	$⊢ (U^{-1} (K) - 1 \in (E ..^E + \|W\| - E) \land \|W\| - E \in ℤ) \to U^{-1} (K) - 1 - E \in (0 ..^\|W\| - E)$
193	190 191 192	syl2anc	$⊢ φ \to U^{-1} (K) - 1 - E \in (0 ..^\|W\| - E)$
194	18 73 42 20 193 125	splfv3	$⊢ φ \to (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - 1 - E) + 1 + E) = W ((U^{-1} (K) - 1) - E + E)$
195	63 65	subcld	$⊢ φ \to U^{-1} (K) - 1 \in ℂ$
196	195 64	npcand	$⊢ φ \to (U^{-1} (K) - 1) - E + E = U^{-1} (K) - 1$
197	196	fveq2d	$⊢ φ \to W ((U^{-1} (K) - 1) - E + E) = W (U^{-1} (K) - 1)$
198	174 194 197	3eqtrd	$⊢ φ \to U (U^{-1} (K)) = W (U^{-1} (K) - 1)$
199	198 58	eqtr3d	$⊢ φ \to W (U^{-1} (K) - 1) = K$
200	199	fveq2d	$⊢ φ \to M (W) (W (U^{-1} (K) - 1)) = M (W) (K)$
201	63 65	npcand	$⊢ φ \to U^{-1} (K) - 1 + 1 = U^{-1} (K)$
202	201	fveq2d	$⊢ φ \to W (U^{-1} (K) - 1 + 1) = W (U^{-1} (K))$
203	168 200 202	3eqtr3d	$⊢ φ \to M (W) (K) = W (U^{-1} (K))$
204	71 126 203	3eqtr4rd	$⊢ φ \to M (W) (K) = (W splice ⟨E, E, ⟨“ I ”⟩⟩) ((U^{-1} (K) - E) + 1 + E)$
205	69 204	eqtr4d	$⊢ φ \to M (U) (K) = M (W) (K)$

Metamath Proof Explorer

Theorem cycpmco2lem6

Proof