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 
|- ( ph -> D e. V )
cycpmco2.w 
|- ( ph -> W e. dom M )
cycpmco2.i 
|- ( ph -> I e. ( D \ ran W ) )
cycpmco2.j 
|- ( ph -> J e. ran W )
cycpmco2.e 
|- E = ( ( `' W ` J ) + 1 )
cycpmco2.1 
|- U = ( W splice <. E , E , <" I "> >. )
Assertion cycpmco2lem3 
|- ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )

Proof

Step Hyp Ref Expression
1 cycpmco2.c 
 |-  M = ( toCyc ` D )
2 cycpmco2.s 
 |-  S = ( SymGrp ` D )
3 cycpmco2.d 
 |-  ( ph -> D e. V )
4 cycpmco2.w 
 |-  ( ph -> W e. dom M )
5 cycpmco2.i 
 |-  ( ph -> I e. ( D \ ran W ) )
6 cycpmco2.j 
 |-  ( ph -> J e. ran W )
7 cycpmco2.e 
 |-  E = ( ( `' W ` J ) + 1 )
8 cycpmco2.1 
 |-  U = ( W splice <. E , E , <" I "> >. )
9 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 1 2 10 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
12 3 11 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
13 12 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
14 4 13 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
15 9 14 sselid 
 |-  ( ph -> W e. Word D )
16 lencl 
 |-  ( W e. Word D -> ( # ` W ) e. NN0 )
17 15 16 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
18 17 nn0cnd 
 |-  ( ph -> ( # ` W ) e. CC )
19 1cnd 
 |-  ( ph -> 1 e. CC )
20 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
21 7 20 eqeltrid 
 |-  ( ph -> E e. _V )
22 5 eldifad 
 |-  ( ph -> I e. D )
23 22 s1cld 
 |-  ( ph -> <" I "> e. Word D )
24 splval 
 |-  ( ( W e. dom M /\ ( E e. _V /\ E e. _V /\ <" I "> e. Word D ) ) -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
25 4 21 21 23 24 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
26 8 25 eqtrid 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
27 26 fveq2d 
 |-  ( ph -> ( # ` U ) = ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) )
28 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
29 15 28 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
30 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
31 29 23 30 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
32 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
33 15 32 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
34 ccatlen 
 |-  ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D ) -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
35 31 33 34 syl2anc 
 |-  ( ph -> ( # ` ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) )
36 ccatws1len 
 |-  ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
37 29 36 syl 
 |-  ( ph -> ( # ` ( ( 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 e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
43 14 42 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
44 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
45 43 44 simpl2im 
 |-  ( ph -> `' W : ran W -1-1-onto-> dom W )
46 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
47 45 46 syl 
 |-  ( ph -> `' W : ran W --> dom W )
48 47 6 ffvelcdmd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
49 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
50 15 49 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
51 48 50 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
52 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
53 51 52 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
54 7 53 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
55 pfxlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
56 15 54 55 syl2anc 
 |-  ( ph -> ( # ` ( W prefix E ) ) = E )
57 56 oveq1d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
58 37 57 eqtrd 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
59 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
60 17 59 sylib 
 |-  ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
61 swrdlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
62 15 54 60 61 syl3anc 
 |-  ( ph -> ( # ` ( W substr <. E , ( # ` W ) >. ) ) = ( ( # ` W ) - E ) )
63 58 62 oveq12d 
 |-  ( ph -> ( ( # ` ( ( W prefix E ) ++ <" I "> ) ) + ( # ` ( W substr <. E , ( # ` W ) >. ) ) ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
64 27 35 63 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
65 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
66 65 54 sselid 
 |-  ( ph -> E e. NN0 )
67 66 nn0zd 
 |-  ( ph -> E e. ZZ )
68 67 peano2zd 
 |-  ( ph -> ( E + 1 ) e. ZZ )
69 68 zcnd 
 |-  ( ph -> ( E + 1 ) e. CC )
70 66 nn0cnd 
 |-  ( ph -> E e. CC )
71 69 18 70 addsubassd 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + 1 ) + ( ( # ` W ) - E ) ) )
72 70 19 18 addassd 
 |-  ( ph -> ( ( E + 1 ) + ( # ` W ) ) = ( E + ( 1 + ( # ` W ) ) ) )
73 72 oveq1d 
 |-  ( ph -> ( ( ( E + 1 ) + ( # ` W ) ) - E ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
74 64 71 73 3eqtr2d 
 |-  ( ph -> ( # ` U ) = ( ( E + ( 1 + ( # ` W ) ) ) - E ) )
75 19 18 addcld 
 |-  ( ph -> ( 1 + ( # ` W ) ) e. CC )
76 70 75 pncan2d 
 |-  ( ph -> ( ( E + ( 1 + ( # ` W ) ) ) - E ) = ( 1 + ( # ` W ) ) )
77 19 18 addcomd 
 |-  ( ph -> ( 1 + ( # ` W ) ) = ( ( # ` W ) + 1 ) )
78 74 76 77 3eqtrd 
 |-  ( ph -> ( # ` U ) = ( ( # ` W ) + 1 ) )
79 18 19 78 mvrraddd 
 |-  ( ph -> ( ( # ` U ) - 1 ) = ( # ` W ) )