Metamath Proof Explorer

Theorem cycpmco2lem7

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 ”⟩
cycpmco2lem7.1 ⊢ φ → K ∈ ran ⁡ W
cycpmco2lem7.2 ⊢ φ → K ≠ J
cycpmco2lem7.3 ⊢ φ → U -1 ⁡ K ∈ 0 ..^ E
Assertion cycpmco2lem7 ⊢ φ → 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 ⊢ φ → 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 cycpmco2lem7.1 ⊢ φ → K ∈ ran ⁡ W
10 cycpmco2lem7.2 ⊢ φ → K ≠ J
11 cycpmco2lem7.3 ⊢ φ → U -1 ⁡ K ∈ 0 ..^ E
12 ssrab2 ⊢ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⊆ Word D
13 eqid ⊢ Base S = Base S
14 1 2 13 tocycf ⊢ D ∈ V → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
15 3 14 syl ⊢ φ → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
16 15 fdmd ⊢ φ → dom ⁡ M = w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
17 4 16 eleqtrd ⊢ φ → W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
18 12 17 sseldi ⊢ φ → W ∈ Word D
19 5 eldifad ⊢ φ → I ∈ D
20 19 s1cld ⊢ φ → ⟨“ I ”⟩ ∈ Word D
21 splcl ⊢ W ∈ Word D ∧ ⟨“ I ”⟩ ∈ Word D → W splice E E ⟨“ I ”⟩ ∈ Word D
22 18 20 21 syl2anc ⊢ φ → W splice E E ⟨“ I ”⟩ ∈ Word D
23 8 22 eqeltrid ⊢ φ → U ∈ Word D
24 1 2 3 4 5 6 7 8 cycpmco2f1 ⊢ φ → U : dom ⁡ U ⟶ 1-1 D
25 id ⊢ w = W → w = W
26 dmeq ⊢ w = W → dom ⁡ w = dom ⁡ W
27 eqidd ⊢ w = W → D = D
28 25 26 27 f1eq123d ⊢ w = W → w : dom ⁡ w ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
29 28 elrab ⊢ W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ↔ W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
30 17 29 sylib ⊢ φ → W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
31 30 simprd ⊢ φ → W : dom ⁡ W ⟶ 1-1 D
32 f1cnv ⊢ W : dom ⁡ W ⟶ 1-1 D → W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W
33 f1of ⊢ W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W → W -1 : ran ⁡ W ⟶ dom ⁡ W
34 31 32 33 3syl ⊢ φ → W -1 : ran ⁡ W ⟶ dom ⁡ W
35 34 6 ffvelrnd ⊢ φ → W -1 ⁡ J ∈ dom ⁡ W
36 wrddm ⊢ W ∈ Word D → dom ⁡ W = 0 ..^ W
37 18 36 syl ⊢ φ → dom ⁡ W = 0 ..^ W
38 35 37 eleqtrd ⊢ φ → W -1 ⁡ J ∈ 0 ..^ W
39 fzofzp1 ⊢ W -1 ⁡ J ∈ 0 ..^ W → W -1 ⁡ J + 1 ∈ 0 … W
40 38 39 syl ⊢ φ → W -1 ⁡ J + 1 ∈ 0 … W
41 7 40 eqeltrid ⊢ φ → E ∈ 0 … W
42 elfzuz3 ⊢ E ∈ 0 … W → W ∈ ℤ ≥ E
43 fzoss2 ⊢ W ∈ ℤ ≥ E → 0 ..^ E ⊆ 0 ..^ W
44 41 42 43 3syl ⊢ φ → 0 ..^ E ⊆ 0 ..^ W
45 1 2 3 4 5 6 7 8 cycpmco2lem3 ⊢ φ → U − 1 = W
46 45 oveq2d ⊢ φ → 0 ..^ U − 1 = 0 ..^ W
47 44 46 sseqtrrd ⊢ φ → 0 ..^ E ⊆ 0 ..^ U − 1
48 47 11 sseldd ⊢ φ → U -1 ⁡ K ∈ 0 ..^ U − 1
49 1 3 23 24 48 cycpmfv1 ⊢ φ → M ⁡ U ⁡ U ⁡ U -1 ⁡ K = U ⁡ U -1 ⁡ K + 1
50 f1f1orn ⊢ U : dom ⁡ U ⟶ 1-1 D → U : dom ⁡ U ⟶ 1-1 onto ran ⁡ U
51 24 50 syl ⊢ φ → U : dom ⁡ U ⟶ 1-1 onto ran ⁡ U
52 ssun1 ⊢ ran ⁡ W ⊆ ran ⁡ W ∪ I
53 1 2 3 4 5 6 7 8 cycpmco2rn ⊢ φ → ran ⁡ U = ran ⁡ W ∪ I
54 52 53 sseqtrrid ⊢ φ → ran ⁡ W ⊆ ran ⁡ U
55 54 sselda ⊢ φ ∧ K ∈ ran ⁡ W → K ∈ ran ⁡ U
56 f1ocnvfv2 ⊢ U : dom ⁡ U ⟶ 1-1 onto ran ⁡ U ∧ K ∈ ran ⁡ U → U ⁡ U -1 ⁡ K = K
57 51 55 56 syl2an2r ⊢ φ ∧ K ∈ ran ⁡ W → U ⁡ U -1 ⁡ K = K
58 57 fveq2d ⊢ φ ∧ K ∈ ran ⁡ W → M ⁡ U ⁡ U ⁡ U -1 ⁡ K = M ⁡ U ⁡ K
59 9 58 mpdan ⊢ φ → M ⁡ U ⁡ U ⁡ U -1 ⁡ K = M ⁡ U ⁡ K
60 f1f1orn ⊢ W : dom ⁡ W ⟶ 1-1 D → W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W
61 31 60 syl ⊢ φ → W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W
62 44 37 sseqtrrd ⊢ φ → 0 ..^ E ⊆ dom ⁡ W
63 62 11 sseldd ⊢ φ → U -1 ⁡ K ∈ dom ⁡ W
64 f1ocnvfv1 ⊢ W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W ∧ U -1 ⁡ K ∈ dom ⁡ W → W -1 ⁡ W ⁡ U -1 ⁡ K = U -1 ⁡ K
65 61 63 64 syl2anc ⊢ φ → W -1 ⁡ W ⁡ U -1 ⁡ K = U -1 ⁡ K
66 8 fveq1i ⊢ U ⁡ U -1 ⁡ K = W splice E E ⟨“ I ”⟩ ⁡ U -1 ⁡ K
67 fz0ssnn0 ⊢ 0 … W ⊆ ℕ 0
68 67 41 sseldi ⊢ φ → E ∈ ℕ 0
69 nn0fz0 ⊢ E ∈ ℕ 0 ↔ E ∈ 0 … E
70 68 69 sylib ⊢ φ → E ∈ 0 … E
71 18 70 41 20 11 splfv1 ⊢ φ → W splice E E ⟨“ I ”⟩ ⁡ U -1 ⁡ K = W ⁡ U -1 ⁡ K
72 66 71 syl5eq ⊢ φ → U ⁡ U -1 ⁡ K = W ⁡ U -1 ⁡ K
73 9 57 mpdan ⊢ φ → U ⁡ U -1 ⁡ K = K
74 72 73 eqtr3d ⊢ φ → W ⁡ U -1 ⁡ K = K
75 74 fveq2d ⊢ φ → W -1 ⁡ W ⁡ U -1 ⁡ K = W -1 ⁡ K
76 65 75 eqtr3d ⊢ φ → U -1 ⁡ K = W -1 ⁡ K
77 76 oveq1d ⊢ φ → U -1 ⁡ K + 1 = W -1 ⁡ K + 1
78 77 fveq2d ⊢ φ → U ⁡ U -1 ⁡ K + 1 = U ⁡ W -1 ⁡ K + 1
79 49 59 78 3eqtr3d ⊢ φ → M ⁡ U ⁡ K = U ⁡ W -1 ⁡ K + 1
80 8 a1i ⊢ φ → U = W splice E E ⟨“ I ”⟩
81 80 fveq1d ⊢ φ → U ⁡ W -1 ⁡ K + 1 = W splice E E ⟨“ I ”⟩ ⁡ W -1 ⁡ K + 1
82 68 nn0zd ⊢ φ → E ∈ ℤ
83 simpr ⊢ φ ∧ U -1 ⁡ K ∈ 0 ..^ E − 1 → U -1 ⁡ K ∈ 0 ..^ E − 1
84 7 a1i ⊢ φ → E = W -1 ⁡ J + 1
85 84 oveq1d ⊢ φ → E − 1 = W -1 ⁡ J + 1 - 1
86 elfzonn0 ⊢ W -1 ⁡ J ∈ 0 ..^ W → W -1 ⁡ J ∈ ℕ 0
87 38 86 syl ⊢ φ → W -1 ⁡ J ∈ ℕ 0
88 87 nn0cnd ⊢ φ → W -1 ⁡ J ∈ ℂ
89 1cnd ⊢ φ → 1 ∈ ℂ
90 88 89 pncand ⊢ φ → W -1 ⁡ J + 1 - 1 = W -1 ⁡ J
91 85 90 eqtr2d ⊢ φ → W -1 ⁡ J = E − 1
92 91 adantr ⊢ φ ∧ U -1 ⁡ K = E − 1 → W -1 ⁡ J = E − 1
93 simpr ⊢ φ ∧ U -1 ⁡ K = E − 1 → U -1 ⁡ K = E − 1
94 76 adantr ⊢ φ ∧ U -1 ⁡ K = E − 1 → U -1 ⁡ K = W -1 ⁡ K
95 92 93 94 3eqtr2rd ⊢ φ ∧ U -1 ⁡ K = E − 1 → W -1 ⁡ K = W -1 ⁡ J
96 95 fveq2d ⊢ φ ∧ U -1 ⁡ K = E − 1 → W ⁡ W -1 ⁡ K = W ⁡ W -1 ⁡ J
97 f1ocnvfv2 ⊢ W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W ∧ K ∈ ran ⁡ W → W ⁡ W -1 ⁡ K = K
98 61 9 97 syl2anc ⊢ φ → W ⁡ W -1 ⁡ K = K
99 98 adantr ⊢ φ ∧ U -1 ⁡ K = E − 1 → W ⁡ W -1 ⁡ K = K
100 f1ocnvfv2 ⊢ W : dom ⁡ W ⟶ 1-1 onto ran ⁡ W ∧ J ∈ ran ⁡ W → W ⁡ W -1 ⁡ J = J
101 61 6 100 syl2anc ⊢ φ → W ⁡ W -1 ⁡ J = J
102 101 adantr ⊢ φ ∧ U -1 ⁡ K = E − 1 → W ⁡ W -1 ⁡ J = J
103 96 99 102 3eqtr3d ⊢ φ ∧ U -1 ⁡ K = E − 1 → K = J
104 10 adantr ⊢ φ ∧ U -1 ⁡ K = E − 1 → K ≠ J
105 103 104 pm2.21ddne ⊢ φ ∧ U -1 ⁡ K = E − 1 → U -1 ⁡ K ∈ 0 ..^ E − 1
106 0zd ⊢ φ → 0 ∈ ℤ
107 nn0p1nn ⊢ W -1 ⁡ J ∈ ℕ 0 → W -1 ⁡ J + 1 ∈ ℕ
108 87 107 syl ⊢ φ → W -1 ⁡ J + 1 ∈ ℕ
109 7 108 eqeltrid ⊢ φ → E ∈ ℕ
110 0p1e1 ⊢ 0 + 1 = 1
111 110 fveq2i ⊢ ℤ ≥ 0 + 1 = ℤ ≥ 1
112 nnuz ⊢ ℕ = ℤ ≥ 1
113 111 112 eqtr4i ⊢ ℤ ≥ 0 + 1 = ℕ
114 109 113 eleqtrrdi ⊢ φ → E ∈ ℤ ≥ 0 + 1
115 fzosplitsnm1 ⊢ 0 ∈ ℤ ∧ E ∈ ℤ ≥ 0 + 1 → 0 ..^ E = 0 ..^ E − 1 ∪ E − 1
116 106 114 115 syl2anc ⊢ φ → 0 ..^ E = 0 ..^ E − 1 ∪ E − 1
117 11 116 eleqtrd ⊢ φ → U -1 ⁡ K ∈ 0 ..^ E − 1 ∪ E − 1
118 fvex ⊢ U -1 ⁡ K ∈ V
119 elunsn ⊢ U -1 ⁡ K ∈ V → U -1 ⁡ K ∈ 0 ..^ E − 1 ∪ E − 1 ↔ U -1 ⁡ K ∈ 0 ..^ E − 1 ∨ U -1 ⁡ K = E − 1
120 118 119 ax-mp ⊢ U -1 ⁡ K ∈ 0 ..^ E − 1 ∪ E − 1 ↔ U -1 ⁡ K ∈ 0 ..^ E − 1 ∨ U -1 ⁡ K = E − 1
121 117 120 sylib ⊢ φ → U -1 ⁡ K ∈ 0 ..^ E − 1 ∨ U -1 ⁡ K = E − 1
122 83 105 121 mpjaodan ⊢ φ → U -1 ⁡ K ∈ 0 ..^ E − 1
123 elfzom1elp1fzo ⊢ E ∈ ℤ ∧ U -1 ⁡ K ∈ 0 ..^ E − 1 → U -1 ⁡ K + 1 ∈ 0 ..^ E
124 82 122 123 syl2anc ⊢ φ → U -1 ⁡ K + 1 ∈ 0 ..^ E
125 77 124 eqeltrrd ⊢ φ → W -1 ⁡ K + 1 ∈ 0 ..^ E
126 18 70 41 20 125 splfv1 ⊢ φ → W splice E E ⟨“ I ”⟩ ⁡ W -1 ⁡ K + 1 = W ⁡ W -1 ⁡ K + 1
127 81 126 eqtrd ⊢ φ → U ⁡ W -1 ⁡ K + 1 = W ⁡ W -1 ⁡ K + 1
128 1zzd ⊢ φ → 1 ∈ ℤ
129 82 128 zsubcld ⊢ φ → E − 1 ∈ ℤ
130 lencl ⊢ W ∈ Word D → W ∈ ℕ 0
131 nn0fz0 ⊢ W ∈ ℕ 0 ↔ W ∈ 0 … W
132 131 biimpi ⊢ W ∈ ℕ 0 → W ∈ 0 … W
133 18 130 132 3syl ⊢ φ → W ∈ 0 … W
134 elfzelz ⊢ W ∈ 0 … W → W ∈ ℤ
135 133 134 syl ⊢ φ → W ∈ ℤ
136 135 128 zsubcld ⊢ φ → W − 1 ∈ ℤ
137 109 nnred ⊢ φ → E ∈ ℝ
138 135 zred ⊢ φ → W ∈ ℝ
139 1red ⊢ φ → 1 ∈ ℝ
140 elfzle2 ⊢ E ∈ 0 … W → E ≤ W
141 41 140 syl ⊢ φ → E ≤ W
142 137 138 139 141 lesub1dd ⊢ φ → E − 1 ≤ W − 1
143 eluz ⊢ E − 1 ∈ ℤ ∧ W − 1 ∈ ℤ → W − 1 ∈ ℤ ≥ E − 1 ↔ E − 1 ≤ W − 1
144 143 biimpar ⊢ E − 1 ∈ ℤ ∧ W − 1 ∈ ℤ ∧ E − 1 ≤ W − 1 → W − 1 ∈ ℤ ≥ E − 1
145 129 136 142 144 syl21anc ⊢ φ → W − 1 ∈ ℤ ≥ E − 1
146 fzoss2 ⊢ W − 1 ∈ ℤ ≥ E − 1 → 0 ..^ E − 1 ⊆ 0 ..^ W − 1
147 145 146 syl ⊢ φ → 0 ..^ E − 1 ⊆ 0 ..^ W − 1
148 147 122 sseldd ⊢ φ → U -1 ⁡ K ∈ 0 ..^ W − 1
149 76 148 eqeltrrd ⊢ φ → W -1 ⁡ K ∈ 0 ..^ W − 1
150 1 3 18 31 149 cycpmfv1 ⊢ φ → M ⁡ W ⁡ W ⁡ W -1 ⁡ K = W ⁡ W -1 ⁡ K + 1
151 98 fveq2d ⊢ φ → M ⁡ W ⁡ W ⁡ W -1 ⁡ K = M ⁡ W ⁡ K
152 127 150 151 3eqtr2rd ⊢ φ → M ⁡ W ⁡ K = U ⁡ W -1 ⁡ K + 1
153 79 152 eqtr4d ⊢ φ → M ⁡ U ⁡ K = M ⁡ W ⁡ K