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 syl5eq φ 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 ffvelrnd φ 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