Metamath Proof Explorer

Theorem cycpmco2lem2

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 cycpmco2lem2 ⊢ φ → U ⁡ E = 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 ovexd ⊢ φ → W -1 ⁡ J + 1 ∈ V
10 7 9 eqeltrid ⊢ φ → E ∈ V
11 5 eldifad ⊢ φ → I ∈ D
12 11 s1cld ⊢ φ → ⟨“ I ”⟩ ∈ Word D
13 splval ⊢ W ∈ dom ⁡ M ∧ E ∈ V ∧ E ∈ V ∧ ⟨“ I ”⟩ ∈ Word D → W splice E E ⟨“ I ”⟩ = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
14 4 10 10 12 13 syl13anc ⊢ φ → W splice E E ⟨“ I ”⟩ = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
15 8 14 syl5eq ⊢ φ → U = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W
16 15 fveq1d ⊢ φ → U ⁡ E = W prefix E ++ ⟨“ I ”⟩ ++ W substr E W ⁡ E
17 ssrab2 ⊢ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⊆ Word D
18 eqid ⊢ Base S = Base S
19 1 2 18 tocycf ⊢ D ∈ V → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
20 3 19 syl ⊢ φ → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
21 20 fdmd ⊢ φ → dom ⁡ M = w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
22 4 21 eleqtrd ⊢ φ → W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
23 17 22 sselid ⊢ φ → W ∈ Word D
24 pfxcl ⊢ W ∈ Word D → W prefix E ∈ Word D
25 23 24 syl ⊢ φ → W prefix E ∈ Word D
26 ccatcl ⊢ W prefix E ∈ Word D ∧ ⟨“ I ”⟩ ∈ Word D → W prefix E ++ ⟨“ I ”⟩ ∈ Word D
27 25 12 26 syl2anc ⊢ φ → W prefix E ++ ⟨“ I ”⟩ ∈ Word D
28 swrdcl ⊢ W ∈ Word D → W substr E W ∈ Word D
29 23 28 syl ⊢ φ → W substr E W ∈ Word D
30 fz0ssnn0 ⊢ 0 … W ⊆ ℕ 0
31 id ⊢ w = W → w = W
32 dmeq ⊢ w = W → dom ⁡ w = dom ⁡ W
33 eqidd ⊢ w = W → D = D
34 31 32 33 f1eq123d ⊢ w = W → w : dom ⁡ w ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
35 34 elrab ⊢ W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ↔ W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
36 22 35 sylib ⊢ φ → W ∈ Word D ∧ W : dom ⁡ W ⟶ 1-1 D
37 36 simprd ⊢ φ → W : dom ⁡ W ⟶ 1-1 D
38 f1cnv ⊢ W : dom ⁡ W ⟶ 1-1 D → W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W
39 f1of ⊢ W -1 : ran ⁡ W ⟶ 1-1 onto dom ⁡ W → W -1 : ran ⁡ W ⟶ dom ⁡ W
40 37 38 39 3syl ⊢ φ → W -1 : ran ⁡ W ⟶ dom ⁡ W
41 40 6 ffvelrnd ⊢ φ → W -1 ⁡ J ∈ dom ⁡ W
42 wrddm ⊢ W ∈ Word D → dom ⁡ W = 0 ..^ W
43 23 42 syl ⊢ φ → dom ⁡ W = 0 ..^ W
44 41 43 eleqtrd ⊢ φ → W -1 ⁡ J ∈ 0 ..^ W
45 fzofzp1 ⊢ W -1 ⁡ J ∈ 0 ..^ W → W -1 ⁡ J + 1 ∈ 0 … W
46 44 45 syl ⊢ φ → W -1 ⁡ J + 1 ∈ 0 … W
47 7 46 eqeltrid ⊢ φ → E ∈ 0 … W
48 30 47 sselid ⊢ φ → E ∈ ℕ 0
49 fzonn0p1 ⊢ E ∈ ℕ 0 → E ∈ 0 ..^ E + 1
50 48 49 syl ⊢ φ → E ∈ 0 ..^ E + 1
51 ccatws1len ⊢ W prefix E ∈ Word D → W prefix E ++ ⟨“ I ”⟩ = W prefix E + 1
52 23 24 51 3syl ⊢ φ → W prefix E ++ ⟨“ I ”⟩ = W prefix E + 1
53 pfxlen ⊢ W ∈ Word D ∧ E ∈ 0 … W → W prefix E = E
54 23 47 53 syl2anc ⊢ φ → W prefix E = E
55 54 oveq1d ⊢ φ → W prefix E + 1 = E + 1
56 52 55 eqtrd ⊢ φ → W prefix E ++ ⟨“ I ”⟩ = E + 1
57 56 oveq2d ⊢ φ → 0 ..^ W prefix E ++ ⟨“ I ”⟩ = 0 ..^ E + 1
58 50 57 eleqtrrd ⊢ φ → E ∈ 0 ..^ W prefix E ++ ⟨“ I ”⟩
59 ccatval1 ⊢ W prefix E ++ ⟨“ I ”⟩ ∈ Word D ∧ W substr E W ∈ Word D ∧ E ∈ 0 ..^ W prefix E ++ ⟨“ I ”⟩ → W prefix E ++ ⟨“ I ”⟩ ++ W substr E W ⁡ E = W prefix E ++ ⟨“ I ”⟩ ⁡ E
60 27 29 58 59 syl3anc ⊢ φ → W prefix E ++ ⟨“ I ”⟩ ++ W substr E W ⁡ E = W prefix E ++ ⟨“ I ”⟩ ⁡ E
61 48 nn0zd ⊢ φ → E ∈ ℤ
62 elfzomin ⊢ E ∈ ℤ → E ∈ E ..^ E + 1
63 61 62 syl ⊢ φ → E ∈ E ..^ E + 1
64 s1len ⊢ ⟨“ I ”⟩ = 1
65 64 a1i ⊢ φ → ⟨“ I ”⟩ = 1
66 54 65 oveq12d ⊢ φ → W prefix E + ⟨“ I ”⟩ = E + 1
67 54 66 oveq12d ⊢ φ → W prefix E ..^ W prefix E + ⟨“ I ”⟩ = E ..^ E + 1
68 63 67 eleqtrrd ⊢ φ → E ∈ W prefix E ..^ W prefix E + ⟨“ I ”⟩
69 ccatval2 ⊢ W prefix E ∈ Word D ∧ ⟨“ I ”⟩ ∈ Word D ∧ E ∈ W prefix E ..^ W prefix E + ⟨“ I ”⟩ → W prefix E ++ ⟨“ I ”⟩ ⁡ E = ⟨“ I ”⟩ ⁡ E − W prefix E
70 25 12 68 69 syl3anc ⊢ φ → W prefix E ++ ⟨“ I ”⟩ ⁡ E = ⟨“ I ”⟩ ⁡ E − W prefix E
71 16 60 70 3eqtrd ⊢ φ → U ⁡ E = ⟨“ I ”⟩ ⁡ E − W prefix E
72 54 oveq2d ⊢ φ → E − W prefix E = E − E
73 48 nn0cnd ⊢ φ → E ∈ ℂ
74 73 subidd ⊢ φ → E − E = 0
75 72 74 eqtrd ⊢ φ → E − W prefix E = 0
76 75 fveq2d ⊢ φ → ⟨“ I ”⟩ ⁡ E − W prefix E = ⟨“ I ”⟩ ⁡ 0
77 s1fv ⊢ I ∈ D ∖ ran ⁡ W → ⟨“ I ”⟩ ⁡ 0 = I
78 5 77 syl ⊢ φ → ⟨“ I ”⟩ ⁡ 0 = I
79 71 76 78 3eqtrd ⊢ φ → U ⁡ E = I