Metamath Proof Explorer


Theorem clwlkclwwlkf

Description: F is a function from the nonempty closed walks into the closed walks as word in a simple pseudograph. (Contributed by AV, 23-May-2022) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c C=wClWalksG|11stw
clwlkclwwlkf.f F=cC2ndcprefix2ndc1
Assertion clwlkclwwlkf GUSHGraphF:CClWWalksG

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c C=wClWalksG|11stw
2 clwlkclwwlkf.f F=cC2ndcprefix2ndc1
3 eqid 1stc=1stc
4 eqid 2ndc=2ndc
5 1 3 4 clwlkclwwlkflem cC1stcWalksG2ndc2ndc0=2ndc1stc1stc
6 isclwlk 1stcClWalksG2ndc1stcWalksG2ndc2ndc0=2ndc1stc
7 fvex 1stcV
8 breq1 f=1stcfClWalksG2ndc1stcClWalksG2ndc
9 7 8 spcev 1stcClWalksG2ndcffClWalksG2ndc
10 6 9 sylbir 1stcWalksG2ndc2ndc0=2ndc1stcffClWalksG2ndc
11 10 3adant3 1stcWalksG2ndc2ndc0=2ndc1stc1stcffClWalksG2ndc
12 11 adantl GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stcffClWalksG2ndc
13 simpl GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stcGUSHGraph
14 eqid VtxG=VtxG
15 14 wlkpwrd 1stcWalksG2ndc2ndcWordVtxG
16 15 3ad2ant1 1stcWalksG2ndc2ndc0=2ndc1stc1stc2ndcWordVtxG
17 16 adantl GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stc2ndcWordVtxG
18 elnnnn0c 1stc1stc011stc
19 nn0re 1stc01stc
20 1e2m1 1=21
21 20 breq1i 11stc211stc
22 21 biimpi 11stc211stc
23 2re 2
24 1re 1
25 lesubadd 211stc211stc21stc+1
26 23 24 25 mp3an12 1stc211stc21stc+1
27 22 26 syl5ib 1stc11stc21stc+1
28 19 27 syl 1stc011stc21stc+1
29 28 adantl 1stcWalksG2ndc1stc011stc21stc+1
30 wlklenvp1 1stcWalksG2ndc2ndc=1stc+1
31 30 adantr 1stcWalksG2ndc1stc02ndc=1stc+1
32 31 breq2d 1stcWalksG2ndc1stc022ndc21stc+1
33 29 32 sylibrd 1stcWalksG2ndc1stc011stc22ndc
34 33 expimpd 1stcWalksG2ndc1stc011stc22ndc
35 18 34 syl5bi 1stcWalksG2ndc1stc22ndc
36 35 a1d 1stcWalksG2ndc2ndc0=2ndc1stc1stc22ndc
37 36 3imp 1stcWalksG2ndc2ndc0=2ndc1stc1stc22ndc
38 37 adantl GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stc22ndc
39 eqid iEdgG=iEdgG
40 14 39 clwlkclwwlk GUSHGraph2ndcWordVtxG22ndcffClWalksG2ndclastS2ndc=2ndc02ndcprefix2ndc1ClWWalksG
41 13 17 38 40 syl3anc GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stcffClWalksG2ndclastS2ndc=2ndc02ndcprefix2ndc1ClWWalksG
42 12 41 mpbid GUSHGraph1stcWalksG2ndc2ndc0=2ndc1stc1stclastS2ndc=2ndc02ndcprefix2ndc1ClWWalksG
43 5 42 sylan2 GUSHGraphcClastS2ndc=2ndc02ndcprefix2ndc1ClWWalksG
44 43 simprd GUSHGraphcC2ndcprefix2ndc1ClWWalksG
45 44 2 fmptd GUSHGraphF:CClWWalksG