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 
|- ( 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 cycpmco2lem2 
|- ( ph -> ( U ` E ) = I )

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 ovexd 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
10 7 9 eqeltrid 
 |-  ( ph -> E e. _V )
11 5 eldifad 
 |-  ( ph -> I e. D )
12 11 s1cld 
 |-  ( ph -> <" I "> e. Word D )
13 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 ) >. ) ) )
14 4 10 10 12 13 syl13anc 
 |-  ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
15 8 14 syl5eq 
 |-  ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
16 15 fveq1d 
 |-  ( ph -> ( U ` E ) = ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` E ) )
17 ssrab2 
 |-  { w e. Word D | w : dom w -1-1-> D } C_ Word D
18 eqid 
 |-  ( Base ` S ) = ( Base ` S )
19 1 2 18 tocycf 
 |-  ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
20 3 19 syl 
 |-  ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
21 20 fdmd 
 |-  ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
22 4 21 eleqtrd 
 |-  ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
23 17 22 sseldi 
 |-  ( ph -> W e. Word D )
24 pfxcl 
 |-  ( W e. Word D -> ( W prefix E ) e. Word D )
25 23 24 syl 
 |-  ( ph -> ( W prefix E ) e. Word D )
26 ccatcl 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
27 25 12 26 syl2anc 
 |-  ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
28 swrdcl 
 |-  ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
29 23 28 syl 
 |-  ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
30 fz0ssnn0 
 |-  ( 0 ... ( # ` W ) ) C_ NN0
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 e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
36 22 35 sylib 
 |-  ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
37 36 simprd 
 |-  ( ph -> W : dom W -1-1-> D )
38 f1cnv 
 |-  ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
39 f1of 
 |-  ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
40 37 38 39 3syl 
 |-  ( ph -> `' W : ran W --> dom W )
41 40 6 ffvelrnd 
 |-  ( ph -> ( `' W ` J ) e. dom W )
42 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
43 23 42 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
44 41 43 eleqtrd 
 |-  ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
45 fzofzp1 
 |-  ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
46 44 45 syl 
 |-  ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
47 7 46 eqeltrid 
 |-  ( ph -> E e. ( 0 ... ( # ` W ) ) )
48 30 47 sseldi 
 |-  ( ph -> E e. NN0 )
49 fzonn0p1 
 |-  ( E e. NN0 -> E e. ( 0 ..^ ( E + 1 ) ) )
50 48 49 syl 
 |-  ( ph -> E e. ( 0 ..^ ( E + 1 ) ) )
51 ccatws1len 
 |-  ( ( W prefix E ) e. Word D -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
52 23 24 51 3syl 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( ( # ` ( W prefix E ) ) + 1 ) )
53 pfxlen 
 |-  ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix E ) ) = E )
54 23 47 53 syl2anc 
 |-  ( ph -> ( # ` ( W prefix E ) ) = E )
55 54 oveq1d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + 1 ) = ( E + 1 ) )
56 52 55 eqtrd 
 |-  ( ph -> ( # ` ( ( W prefix E ) ++ <" I "> ) ) = ( E + 1 ) )
57 56 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) = ( 0 ..^ ( E + 1 ) ) )
58 50 57 eleqtrrd 
 |-  ( ph -> E e. ( 0 ..^ ( # ` ( ( W prefix E ) ++ <" I "> ) ) ) )
59 ccatval1 
 |-  ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D /\ E 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 
 |-  ( ph -> ( ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ` E ) = ( ( ( W prefix E ) ++ <" I "> ) ` E ) )
61 48 nn0zd 
 |-  ( ph -> E e. ZZ )
62 elfzomin 
 |-  ( E e. ZZ -> E e. ( E ..^ ( E + 1 ) ) )
63 61 62 syl 
 |-  ( ph -> E e. ( E ..^ ( E + 1 ) ) )
64 s1len 
 |-  ( # ` <" I "> ) = 1
65 64 a1i 
 |-  ( ph -> ( # ` <" I "> ) = 1 )
66 54 65 oveq12d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) + ( # ` <" I "> ) ) = ( E + 1 ) )
67 54 66 oveq12d 
 |-  ( ph -> ( ( # ` ( W prefix E ) ) ..^ ( ( # ` ( W prefix E ) ) + ( # ` <" I "> ) ) ) = ( E ..^ ( E + 1 ) ) )
68 63 67 eleqtrrd 
 |-  ( ph -> E e. ( ( # ` ( W prefix E ) ) ..^ ( ( # ` ( W prefix E ) ) + ( # ` <" I "> ) ) ) )
69 ccatval2 
 |-  ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D /\ E e. ( ( # ` ( W prefix E ) ) ..^ ( ( # ` ( W prefix E ) ) + ( # ` <" I "> ) ) ) ) -> ( ( ( W prefix E ) ++ <" I "> ) ` E ) = ( <" I "> ` ( E - ( # ` ( W prefix E ) ) ) ) )
70 25 12 68 69 syl3anc 
 |-  ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ` E ) = ( <" I "> ` ( E - ( # ` ( W prefix E ) ) ) ) )
71 16 60 70 3eqtrd 
 |-  ( ph -> ( U ` E ) = ( <" I "> ` ( E - ( # ` ( W prefix E ) ) ) ) )
72 54 oveq2d 
 |-  ( ph -> ( E - ( # ` ( W prefix E ) ) ) = ( E - E ) )
73 48 nn0cnd 
 |-  ( ph -> E e. CC )
74 73 subidd 
 |-  ( ph -> ( E - E ) = 0 )
75 72 74 eqtrd 
 |-  ( ph -> ( E - ( # ` ( W prefix E ) ) ) = 0 )
76 75 fveq2d 
 |-  ( ph -> ( <" I "> ` ( E - ( # ` ( W prefix E ) ) ) ) = ( <" I "> ` 0 ) )
77 s1fv 
 |-  ( I e. ( D \ ran W ) -> ( <" I "> ` 0 ) = I )
78 5 77 syl 
 |-  ( ph -> ( <" I "> ` 0 ) = I )
79 71 76 78 3eqtrd 
 |-  ( ph -> ( U ` E ) = I )