Metamath Proof Explorer

Theorem cycpmco2lem3

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 cycpmco2lem3 ⊢ φ → U − 1 = W

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