cycpmco2

Description: The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-Jan-2024)

	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	cycpmco2	$⊢ φ \to M (W) \circ M (⟨“ I J ”⟩) = M (U)$

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		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10	1 2 9	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
11	3 10	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
12	11	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
13	4 12	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
14	11 13	ffvelrnd	$⊢ φ \to M (W) \in {Base}_{S}$
15	2 9	symgbasf	$⊢ M (W) \in {Base}_{S} \to M (W) : D ⟶ D$
16	14 15	syl	$⊢ φ \to M (W) : D ⟶ D$
17	16	ffnd	$⊢ φ \to M (W) Fn D$
18	5	eldifad	$⊢ φ \to I \in D$
19		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
20	19 13	sselid	$⊢ φ \to W \in Word D$
21		id	$⊢ w = W \to w = W$
22		dmeq	$⊢ w = W \to dom w = dom W$
23		eqidd	$⊢ w = W \to D = D$
24	21 22 23	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
25	24	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)$
26	25	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$
27	20 13 26	syl2anc	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
28		f1f	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W ⟶ D$
29	27 28	syl	$⊢ φ \to W : dom W ⟶ D$
30	29	frnd	$⊢ φ \to ran W \subseteq D$
31	30 6	sseldd	$⊢ φ \to J \in D$
32	5	eldifbd	$⊢ φ \to \neg I \in ran W$
33		nelne2	$⊢ (J \in ran W \land \neg I \in ran W) \to J \neq I$
34	6 32 33	syl2anc	$⊢ φ \to J \neq I$
35	34	necomd	$⊢ φ \to I \neq J$
36	1 3 18 31 35 2	cycpm2cl	$⊢ φ \to M (⟨“ I J ”⟩) \in {Base}_{S}$
37	2 9	symgbasf	$⊢ M (⟨“ I J ”⟩) \in {Base}_{S} \to M (⟨“ I J ”⟩) : D ⟶ D$
38	36 37	syl	$⊢ φ \to M (⟨“ I J ”⟩) : D ⟶ D$
39	38	ffnd	$⊢ φ \to M (⟨“ I J ”⟩) Fn D$
40	38	frnd	$⊢ φ \to ran M (⟨“ I J ”⟩) \subseteq D$
41		fnco	$⊢ (M (W) Fn D \land M (⟨“ I J ”⟩) Fn D \land ran M (⟨“ I J ”⟩) \subseteq D) \to (M (W) \circ M (⟨“ I J ”⟩)) Fn D$
42	17 39 40 41	syl3anc	$⊢ φ \to (M (W) \circ M (⟨“ I J ”⟩)) Fn D$
43	18	s1cld	$⊢ φ \to ⟨“ I ”⟩ \in Word D$
44		splcl	$⊢ (W \in Word D \land ⟨“ I ”⟩ \in Word D) \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
45	20 43 44	syl2anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ \in Word D$
46	8 45	eqeltrid	$⊢ φ \to U \in Word D$
47	1 2 3 4 5 6 7 8	cycpmco2f1	$⊢ φ \to U : dom U \underset{1-1}{⟶} D$
48	1 3 46 47 2	cycpmcl	$⊢ φ \to M (U) \in {Base}_{S}$
49	2 9	symgbasf	$⊢ M (U) \in {Base}_{S} \to M (U) : D ⟶ D$
50	48 49	syl	$⊢ φ \to M (U) : D ⟶ D$
51	50	ffnd	$⊢ φ \to M (U) Fn D$
52		fvco3	$⊢ (M (⟨“ I J ”⟩) : D ⟶ D \land i \in D) \to (M (W) \circ M (⟨“ I J ”⟩)) (i) = M (W) (M (⟨“ I J ”⟩) (i))$
53	38 52	sylan	$⊢ (φ \land i \in D) \to (M (W) \circ M (⟨“ I J ”⟩)) (i) = M (W) (M (⟨“ I J ”⟩) (i))$
54	1 3 18 31 35 2	cyc2fv2	$⊢ φ \to M (⟨“ I J ”⟩) (J) = I$
55	54	fveq2d	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (J)) = M (W) (I)$
56	1 2 3 4 5 6 7 8	cycpmco2lem2	$⊢ φ \to U (E) = I$
57		f1cnv	$⊢ W : dom W \underset{1-1}{⟶} D \to W^{-1} : ran W \underset{1-1 onto}{⟶} dom W$
58		f1of	$⊢ W^{-1} : ran W \underset{1-1 onto}{⟶} dom W \to W^{-1} : ran W ⟶ dom W$
59	27 57 58	3syl	$⊢ φ \to W^{-1} : ran W ⟶ dom W$
60	59 6	ffvelrnd	$⊢ φ \to W^{-1} (J) \in dom W$
61		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
62	20 61	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
63	60 62	eleqtrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W\|)$
64		lencl	$⊢ W \in Word D \to \|W\| \in ℕ_{0}$
65	20 64	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
66	65	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
67		1cnd	$⊢ φ \to 1 \in ℂ$
68		ovexd	$⊢ φ \to W^{-1} (J) + 1 \in V$
69	7 68	eqeltrid	$⊢ φ \to E \in V$
70		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\|⟩)$
71	4 69 69 43 70	syl13anc	$⊢ φ \to W splice ⟨E, E, ⟨“ I ”⟩⟩ = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
72	8 71	syl5eq	$⊢ φ \to U = ((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)$
73	72	fveq2d	$⊢ φ \to \|U\| = \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\|$
74		pfxcl	$⊢ W \in Word D \to W prefix E \in Word D$
75	20 74	syl	$⊢ φ \to W prefix E \in Word D$
76		ccatcl	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D) \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
77	75 43 76	syl2anc	$⊢ φ \to (W prefix E) ++ ⟨“ I ”⟩ \in Word D$
78		swrdcl	$⊢ W \in Word D \to W substr ⟨E, \|W\|⟩ \in Word D$
79	20 78	syl	$⊢ φ \to W substr ⟨E, \|W\|⟩ \in Word D$
80		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\|⟩\|$
81	77 79 80	syl2anc	$⊢ φ \to \|((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)\| = \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\|$
82		ccatws1len	$⊢ W prefix E \in Word D \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
83	20 74 82	3syl	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = \|W prefix E\| + 1$
84		fzofzp1	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
85	63 84	syl	$⊢ φ \to W^{-1} (J) + 1 \in (0 \dots \|W\|)$
86	7 85	eqeltrid	$⊢ φ \to E \in (0 \dots \|W\|)$
87		pfxlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|)) \to \|W prefix E\| = E$
88	20 86 87	syl2anc	$⊢ φ \to \|W prefix E\| = E$
89	88	oveq1d	$⊢ φ \to \|W prefix E\| + 1 = E + 1$
90	83 89	eqtrd	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| = E + 1$
91		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
92	65 91	sylib	$⊢ φ \to \|W\| \in (0 \dots \|W\|)$
93		swrdlen	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
94	20 86 92 93	syl3anc	$⊢ φ \to \|W substr ⟨E, \|W\|⟩\| = \|W\| - E$
95	90 94	oveq12d	$⊢ φ \to \|(W prefix E) ++ ⟨“ I ”⟩\| + \|W substr ⟨E, \|W\|⟩\| = E + 1 + (\|W\| - E)$
96	73 81 95	3eqtrd	$⊢ φ \to \|U\| = E + 1 + (\|W\| - E)$
97		fz0ssnn0	$⊢ (0 \dots \|W\|) \subseteq ℕ_{0}$
98	97 86	sselid	$⊢ φ \to E \in ℕ_{0}$
99	98	nn0zd	$⊢ φ \to E \in ℤ$
100	99	peano2zd	$⊢ φ \to E + 1 \in ℤ$
101	100	zcnd	$⊢ φ \to E + 1 \in ℂ$
102	98	nn0cnd	$⊢ φ \to E \in ℂ$
103	101 66 102	addsubassd	$⊢ φ \to (E + 1) + \|W\| - E = E + 1 + (\|W\| - E)$
104	102 67 66	addassd	$⊢ φ \to E + 1 + \|W\| = E + 1 + \|W\|$
105	104	oveq1d	$⊢ φ \to (E + 1) + \|W\| - E = E + (1 + \|W\|) - E$
106	96 103 105	3eqtr2d	$⊢ φ \to \|U\| = E + (1 + \|W\|) - E$
107	67 66	addcld	$⊢ φ \to 1 + \|W\| \in ℂ$
108	102 107	pncan2d	$⊢ φ \to E + (1 + \|W\|) - E = 1 + \|W\|$
109	67 66	addcomd	$⊢ φ \to 1 + \|W\| = \|W\| + 1$
110	106 108 109	3eqtrd	$⊢ φ \to \|U\| = \|W\| + 1$
111	66 67 110	mvrraddd	$⊢ φ \to \|U\| - 1 = \|W\|$
112	111	oveq2d	$⊢ φ \to (0 ..^\|U\| - 1) = (0 ..^\|W\|)$
113	63 112	eleqtrrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|U\| - 1)$
114	1 3 46 47 113	cycpmfv1	$⊢ φ \to M (U) (U (W^{-1} (J))) = U (W^{-1} (J) + 1)$
115	7	fveq2i	$⊢ U (E) = U (W^{-1} (J) + 1)$
116	114 115	eqtr4di	$⊢ φ \to M (U) (U (W^{-1} (J))) = U (E)$
117	1 3 20 27 18 32	cycpmfv3	$⊢ φ \to M (W) (I) = I$
118	56 116 117	3eqtr4d	$⊢ φ \to M (U) (U (W^{-1} (J))) = M (W) (I)$
119	72	fveq1d	$⊢ φ \to U (W^{-1} (J)) = (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (W^{-1} (J))$
120		fzossfzop1	$⊢ E \in ℕ_{0} \to (0 ..^E) \subseteq (0 ..^E + 1)$
121	98 120	syl	$⊢ φ \to (0 ..^E) \subseteq (0 ..^E + 1)$
122		elfzonn0	$⊢ W^{-1} (J) \in (0 ..^\|W\|) \to W^{-1} (J) \in ℕ_{0}$
123		fzonn0p1	$⊢ W^{-1} (J) \in ℕ_{0} \to W^{-1} (J) \in (0 ..^W^{-1} (J) + 1)$
124	63 122 123	3syl	$⊢ φ \to W^{-1} (J) \in (0 ..^W^{-1} (J) + 1)$
125	7	oveq2i	$⊢ (0 ..^E) = (0 ..^W^{-1} (J) + 1)$
126	124 125	eleqtrrdi	$⊢ φ \to W^{-1} (J) \in (0 ..^E)$
127	121 126	sseldd	$⊢ φ \to W^{-1} (J) \in (0 ..^E + 1)$
128	90	oveq2d	$⊢ φ \to (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|) = (0 ..^E + 1)$
129	127 128	eleqtrrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)$
130		ccatval1	$⊢ ((W prefix E) ++ ⟨“ I ”⟩ \in Word D \land W substr ⟨E, \|W\|⟩ \in Word D \land W^{-1} (J) \in (0 ..^\|(W prefix E) ++ ⟨“ I ”⟩\|)) \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (W^{-1} (J)) = ((W prefix E) ++ ⟨“ I ”⟩) (W^{-1} (J))$
131	77 79 129 130	syl3anc	$⊢ φ \to (((W prefix E) ++ ⟨“ I ”⟩) ++ (W substr ⟨E, \|W\|⟩)) (W^{-1} (J)) = ((W prefix E) ++ ⟨“ I ”⟩) (W^{-1} (J))$
132	88	oveq2d	$⊢ φ \to (0 ..^\|W prefix E\|) = (0 ..^E)$
133	126 132	eleqtrrd	$⊢ φ \to W^{-1} (J) \in (0 ..^\|W prefix E\|)$
134		ccatval1	$⊢ (W prefix E \in Word D \land ⟨“ I ”⟩ \in Word D \land W^{-1} (J) \in (0 ..^\|W prefix E\|)) \to ((W prefix E) ++ ⟨“ I ”⟩) (W^{-1} (J)) = (W prefix E) (W^{-1} (J))$
135	75 43 133 134	syl3anc	$⊢ φ \to ((W prefix E) ++ ⟨“ I ”⟩) (W^{-1} (J)) = (W prefix E) (W^{-1} (J))$
136	119 131 135	3eqtrd	$⊢ φ \to U (W^{-1} (J)) = (W prefix E) (W^{-1} (J))$
137		pfxfv	$⊢ (W \in Word D \land E \in (0 \dots \|W\|) \land W^{-1} (J) \in (0 ..^E)) \to (W prefix E) (W^{-1} (J)) = W (W^{-1} (J))$
138	20 86 126 137	syl3anc	$⊢ φ \to (W prefix E) (W^{-1} (J)) = W (W^{-1} (J))$
139		f1f1orn	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W \underset{1-1 onto}{⟶} ran W$
140	27 139	syl	$⊢ φ \to W : dom W \underset{1-1 onto}{⟶} ran W$
141		f1ocnvfv2	$⊢ (W : dom W \underset{1-1 onto}{⟶} ran W \land J \in ran W) \to W (W^{-1} (J)) = J$
142	140 6 141	syl2anc	$⊢ φ \to W (W^{-1} (J)) = J$
143	136 138 142	3eqtrd	$⊢ φ \to U (W^{-1} (J)) = J$
144	143	fveq2d	$⊢ φ \to M (U) (U (W^{-1} (J))) = M (U) (J)$
145	55 118 144	3eqtr2d	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (J)) = M (U) (J)$
146	145	ad2antrr	$⊢ ((φ \land i \in ran W) \land i = J) \to M (W) (M (⟨“ I J ”⟩) (J)) = M (U) (J)$
147		simpr	$⊢ ((φ \land i \in ran W) \land i = J) \to i = J$
148	147	fveq2d	$⊢ ((φ \land i \in ran W) \land i = J) \to M (⟨“ I J ”⟩) (i) = M (⟨“ I J ”⟩) (J)$
149	148	fveq2d	$⊢ ((φ \land i \in ran W) \land i = J) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (W) (M (⟨“ I J ”⟩) (J))$
150	147	fveq2d	$⊢ ((φ \land i \in ran W) \land i = J) \to M (U) (i) = M (U) (J)$
151	146 149 150	3eqtr4d	$⊢ ((φ \land i \in ran W) \land i = J) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
152	3	ad2antrr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to D \in V$
153	18 31	s2cld	$⊢ φ \to ⟨“ I J ”⟩ \in Word D$
154	153	ad2antrr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to ⟨“ I J ”⟩ \in Word D$
155	18 31 35	s2f1	$⊢ φ \to ⟨“ I J ”⟩ : dom ⟨“ I J ”⟩ \underset{1-1}{⟶} D$
156	155	ad2antrr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to ⟨“ I J ”⟩ : dom ⟨“ I J ”⟩ \underset{1-1}{⟶} D$
157	30	sselda	$⊢ (φ \land i \in ran W) \to i \in D$
158	157	adantr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to i \in D$
159		simpr	$⊢ (φ \land i \in ran W) \to i \in ran W$
160	32	adantr	$⊢ (φ \land i \in ran W) \to \neg I \in ran W$
161		nelne2	$⊢ (i \in ran W \land \neg I \in ran W) \to i \neq I$
162	159 160 161	syl2anc	$⊢ (φ \land i \in ran W) \to i \neq I$
163	162	adantr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to i \neq I$
164		simpr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to i \neq J$
165	163 164	nelprd	$⊢ ((φ \land i \in ran W) \land i \neq J) \to \neg i \in \{I, J\}$
166	18 31	s2rn	$⊢ φ \to ran ⟨“ I J ”⟩ = \{I, J\}$
167	166	eleq2d	$⊢ φ \to (i \in ran ⟨“ I J ”⟩ \leftrightarrow i \in \{I, J\})$
168	167	notbid	$⊢ φ \to (\neg i \in ran ⟨“ I J ”⟩ \leftrightarrow \neg i \in \{I, J\})$
169	168	ad2antrr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to (\neg i \in ran ⟨“ I J ”⟩ \leftrightarrow \neg i \in \{I, J\})$
170	165 169	mpbird	$⊢ ((φ \land i \in ran W) \land i \neq J) \to \neg i \in ran ⟨“ I J ”⟩$
171	1 152 154 156 158 170	cycpmfv3	$⊢ ((φ \land i \in ran W) \land i \neq J) \to M (⟨“ I J ”⟩) (i) = i$
172	171	fveq2d	$⊢ ((φ \land i \in ran W) \land i \neq J) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (W) (i)$
173	3	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to D \in V$
174	4	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to W \in dom M$
175	5	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to I \in (D ∖ ran W)$
176	6	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to J \in ran W$
177		simpllr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to i \in ran W$
178		simplr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to i \neq J$
179		simpr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to U^{-1} (i) \in (0 ..^E)$
180	1 2 173 174 175 176 7 8 177 178 179	cycpmco2lem7	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (0 ..^E)) \to M (U) (i) = M (W) (i)$
181	3	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to D \in V$
182	4	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to W \in dom M$
183	5	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to I \in (D ∖ ran W)$
184	6	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to J \in ran W$
185		simpllr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to i \in ran W$
186	162	ad2antrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to i \neq I$
187		simpr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to U^{-1} (i) \in (E ..^\|U\| - 1)$
188	1 2 181 182 183 184 7 8 185 186 187	cycpmco2lem6	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) \in (E ..^\|U\| - 1)) \to M (U) (i) = M (W) (i)$
189	3	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to D \in V$
190	4	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to W \in dom M$
191	5	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to I \in (D ∖ ran W)$
192	6	ad3antrrr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to J \in ran W$
193		simpllr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to i \in ran W$
194		simpr	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to U^{-1} (i) = \|U\| - 1$
195	1 2 189 190 191 192 7 8 193 194	cycpmco2lem5	$⊢ (((φ \land i \in ran W) \land i \neq J) \land U^{-1} (i) = \|U\| - 1) \to M (U) (i) = M (W) (i)$
196		f1f1orn	$⊢ U : dom U \underset{1-1}{⟶} D \to U : dom U \underset{1-1 onto}{⟶} ran U$
197	47 196	syl	$⊢ φ \to U : dom U \underset{1-1 onto}{⟶} ran U$
198		ssun1	$⊢ ran W \subseteq ran W \cup \{I\}$
199	1 2 3 4 5 6 7 8	cycpmco2rn	$⊢ φ \to ran U = ran W \cup \{I\}$
200	198 199	sseqtrrid	$⊢ φ \to ran W \subseteq ran U$
201	200	sselda	$⊢ (φ \land i \in ran W) \to i \in ran U$
202		f1ocnvdm	$⊢ (U : dom U \underset{1-1 onto}{⟶} ran U \land i \in ran U) \to U^{-1} (i) \in dom U$
203	197 201 202	syl2an2r	$⊢ (φ \land i \in ran W) \to U^{-1} (i) \in dom U$
204		wrddm	$⊢ U \in Word D \to dom U = (0 ..^\|U\|)$
205	46 204	syl	$⊢ φ \to dom U = (0 ..^\|U\|)$
206	205	adantr	$⊢ (φ \land i \in ran W) \to dom U = (0 ..^\|U\|)$
207	203 206	eleqtrd	$⊢ (φ \land i \in ran W) \to U^{-1} (i) \in (0 ..^\|U\|)$
208	65	nn0zd	$⊢ φ \to \|W\| \in ℤ$
209	208	peano2zd	$⊢ φ \to \|W\| + 1 \in ℤ$
210	110 209	eqeltrd	$⊢ φ \to \|U\| \in ℤ$
211		fzoval	$⊢ \|U\| \in ℤ \to (0 ..^\|U\|) = (0 \dots \|U\| - 1)$
212	210 211	syl	$⊢ φ \to (0 ..^\|U\|) = (0 \dots \|U\| - 1)$
213	212	adantr	$⊢ (φ \land i \in ran W) \to (0 ..^\|U\|) = (0 \dots \|U\| - 1)$
214	207 213	eleqtrd	$⊢ (φ \land i \in ran W) \to U^{-1} (i) \in (0 \dots \|U\| - 1)$
215		elfzr	$⊢ U^{-1} (i) \in (0 \dots \|U\| - 1) \to (U^{-1} (i) \in (0 ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1)$
216	214 215	syl	$⊢ (φ \land i \in ran W) \to (U^{-1} (i) \in (0 ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1)$
217		simpr	$⊢ ((φ \land i \in ran W) \land U^{-1} (i) \in (0 ..^\|U\| - 1)) \to U^{-1} (i) \in (0 ..^\|U\| - 1)$
218	99	ad2antrr	$⊢ ((φ \land i \in ran W) \land U^{-1} (i) \in (0 ..^\|U\| - 1)) \to E \in ℤ$
219		fzospliti	$⊢ (U^{-1} (i) \in (0 ..^\|U\| - 1) \land E \in ℤ) \to (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1))$
220	217 218 219	syl2anc	$⊢ ((φ \land i \in ran W) \land U^{-1} (i) \in (0 ..^\|U\| - 1)) \to (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1))$
221	220	ex	$⊢ (φ \land i \in ran W) \to (U^{-1} (i) \in (0 ..^\|U\| - 1) \to (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1)))$
222	221	orim1d	$⊢ (φ \land i \in ran W) \to ((U^{-1} (i) \in (0 ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1) \to ((U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1)) \lor U^{-1} (i) = \|U\| - 1))$
223	216 222	mpd	$⊢ (φ \land i \in ran W) \to ((U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1)) \lor U^{-1} (i) = \|U\| - 1)$
224		df-3or	$⊢ (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1) \leftrightarrow ((U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1)) \lor U^{-1} (i) = \|U\| - 1)$
225	223 224	sylibr	$⊢ (φ \land i \in ran W) \to (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1)$
226	225	adantr	$⊢ ((φ \land i \in ran W) \land i \neq J) \to (U^{-1} (i) \in (0 ..^E) \lor U^{-1} (i) \in (E ..^\|U\| - 1) \lor U^{-1} (i) = \|U\| - 1)$
227	180 188 195 226	mpjao3dan	$⊢ ((φ \land i \in ran W) \land i \neq J) \to M (U) (i) = M (W) (i)$
228	172 227	eqtr4d	$⊢ ((φ \land i \in ran W) \land i \neq J) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
229	151 228	pm2.61dane	$⊢ (φ \land i \in ran W) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
230	229	adantlr	$⊢ ((φ \land i \in D) \land i \in ran W) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
231	1 2 3 4 5 6 7 8	cycpmco2lem4	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (U) (I)$
232	231	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to M (W) (M (⟨“ I J ”⟩) (I)) = M (U) (I)$
233		simpr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to i = I$
234	233	fveq2d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to M (⟨“ I J ”⟩) (i) = M (⟨“ I J ”⟩) (I)$
235	234	fveq2d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (W) (M (⟨“ I J ”⟩) (I))$
236	233	fveq2d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to M (U) (i) = M (U) (I)$
237	232 235 236	3eqtr4d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i = I) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
238	3	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to D \in V$
239	20	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to W \in Word D$
240	27	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to W : dom W \underset{1-1}{⟶} D$
241		simplr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to i \in (D ∖ ran W)$
242	241	eldifad	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to i \in D$
243	241	eldifbd	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to \neg i \in ran W$
244	1 238 239 240 242 243	cycpmfv3	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to M (W) (i) = i$
245	153	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to ⟨“ I J ”⟩ \in Word D$
246	155	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to ⟨“ I J ”⟩ : dom ⟨“ I J ”⟩ \underset{1-1}{⟶} D$
247		simpr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to i \neq I$
248		eldifn	$⊢ i \in (D ∖ ran W) \to \neg i \in ran W$
249		nelne2	$⊢ (J \in ran W \land \neg i \in ran W) \to J \neq i$
250	6 248 249	syl2an	$⊢ (φ \land i \in (D ∖ ran W)) \to J \neq i$
251	250	necomd	$⊢ (φ \land i \in (D ∖ ran W)) \to i \neq J$
252	251	adantr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to i \neq J$
253	247 252	nelprd	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to \neg i \in \{I, J\}$
254	168	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to (\neg i \in ran ⟨“ I J ”⟩ \leftrightarrow \neg i \in \{I, J\})$
255	253 254	mpbird	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to \neg i \in ran ⟨“ I J ”⟩$
256	1 238 245 246 242 255	cycpmfv3	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to M (⟨“ I J ”⟩) (i) = i$
257	256	fveq2d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (W) (i)$
258	46	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to U \in Word D$
259	47	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to U : dom U \underset{1-1}{⟶} D$
260	199	ad2antrr	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to ran U = ran W \cup \{I\}$
261		nelsn	$⊢ i \neq I \to \neg i \in \{I\}$
262	261	adantl	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to \neg i \in \{I\}$
263		nelun	$⊢ ran U = ran W \cup \{I\} \to (\neg i \in ran U \leftrightarrow (\neg i \in ran W \land \neg i \in \{I\}))$
264	263	biimpar	$⊢ (ran U = ran W \cup \{I\} \land (\neg i \in ran W \land \neg i \in \{I\})) \to \neg i \in ran U$
265	260 243 262 264	syl12anc	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to \neg i \in ran U$
266	1 238 258 259 242 265	cycpmfv3	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to M (U) (i) = i$
267	244 257 266	3eqtr4d	$⊢ ((φ \land i \in (D ∖ ran W)) \land i \neq I) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
268	237 267	pm2.61dane	$⊢ (φ \land i \in (D ∖ ran W)) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
269	268	adantlr	$⊢ ((φ \land i \in D) \land i \in (D ∖ ran W)) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
270		undif	$⊢ ran W \subseteq D \leftrightarrow ran W \cup (D ∖ ran W) = D$
271	30 270	sylib	$⊢ φ \to ran W \cup (D ∖ ran W) = D$
272	271	eleq2d	$⊢ φ \to (i \in (ran W \cup (D ∖ ran W)) \leftrightarrow i \in D)$
273		elun	$⊢ i \in (ran W \cup (D ∖ ran W)) \leftrightarrow (i \in ran W \lor i \in (D ∖ ran W))$
274	272 273	bitr3di	$⊢ φ \to (i \in D \leftrightarrow (i \in ran W \lor i \in (D ∖ ran W)))$
275	274	biimpa	$⊢ (φ \land i \in D) \to (i \in ran W \lor i \in (D ∖ ran W))$
276	230 269 275	mpjaodan	$⊢ (φ \land i \in D) \to M (W) (M (⟨“ I J ”⟩) (i)) = M (U) (i)$
277	53 276	eqtrd	$⊢ (φ \land i \in D) \to (M (W) \circ M (⟨“ I J ”⟩)) (i) = M (U) (i)$
278	42 51 277	eqfnfvd	$⊢ φ \to M (W) \circ M (⟨“ I J ”⟩) = M (U)$

Metamath Proof Explorer

Theorem cycpmco2

Proof