Metamath Proof Explorer

Theorem clwlkclwwlkfo

Description: F is a function from the nonempty closed walks onto the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 2-May-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c ⊢C=w∈ClWalks⁡G|1≤1st⁡w
clwlkclwwlkf.f ⊢F=c∈C⟼2nd⁡cprefix2nd⁡c−1
Assertion clwlkclwwlkfo ⊢G∈USHGraph→F:C⟶ontoClWWalks⁡G

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢C=w∈ClWalks⁡G|1≤1st⁡w
2 clwlkclwwlkf.f ⊢F=c∈C⟼2nd⁡cprefix2nd⁡c−1
3 1 2 clwlkclwwlkf ⊢G∈USHGraph→F:C⟶ClWWalks⁡G
4 clwwlkgt0 ⊢w∈ClWWalks⁡G→0<w
5 eqid ⊢Vtx⁡G=Vtx⁡G
6 5 clwwlkbp ⊢w∈ClWWalks⁡G→G∈V∧w∈WordVtx⁡G∧w≠∅
7 lencl ⊢w∈WordVtx⁡G→w∈ℕ0
8 7 nn0zd ⊢w∈WordVtx⁡G→w∈ℤ
9 zgt0ge1 ⊢w∈ℤ→0<w↔1≤w
10 8 9 syl ⊢w∈WordVtx⁡G→0<w↔1≤w
11 10 biimpd ⊢w∈WordVtx⁡G→0<w→1≤w
12 11 anc2li ⊢w∈WordVtx⁡G→0<w→w∈WordVtx⁡G∧1≤w
13 12 3ad2ant2 ⊢G∈V∧w∈WordVtx⁡G∧w≠∅→0<w→w∈WordVtx⁡G∧1≤w
14 6 13 syl ⊢w∈ClWWalks⁡G→0<w→w∈WordVtx⁡G∧1≤w
15 4 14 mpd ⊢w∈ClWWalks⁡G→w∈WordVtx⁡G∧1≤w
16 15 adantl ⊢G∈USHGraph∧w∈ClWWalks⁡G→w∈WordVtx⁡G∧1≤w
17 eqid ⊢iEdg⁡G=iEdg⁡G
18 5 17 clwlkclwwlk2 ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→∃ffClWalks⁡Gw++⟨“w⁡0”⟩↔w∈ClWWalks⁡G
19 df-br ⊢fClWalks⁡Gw++⟨“w⁡0”⟩↔fw++⟨“w⁡0”⟩∈ClWalks⁡G
20 simpr2 ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w→w∈WordVtx⁡G
21 simpr3 ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w→1≤w
22 simpl ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G
23 1 clwlkclwwlkfolem ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→fw++⟨“w⁡0”⟩∈C
24 20 21 22 23 syl3anc ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈C
25 23 3expa ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→fw++⟨“w⁡0”⟩∈C
26 ovex ⊢w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1∈V
27 fveq2 ⊢c=fw++⟨“w⁡0”⟩→2nd⁡c=2nd⁡fw++⟨“w⁡0”⟩
28 2fveq3 ⊢c=fw++⟨“w⁡0”⟩→2nd⁡c=2nd⁡fw++⟨“w⁡0”⟩
29 28 oveq1d ⊢c=fw++⟨“w⁡0”⟩→2nd⁡c−1=2nd⁡fw++⟨“w⁡0”⟩−1
30 27 29 oveq12d ⊢c=fw++⟨“w⁡0”⟩→2nd⁡cprefix2nd⁡c−1=2nd⁡fw++⟨“w⁡0”⟩prefix2nd⁡fw++⟨“w⁡0”⟩−1
31 vex ⊢f∈V
32 ovex ⊢w++⟨“w⁡0”⟩∈V
33 31 32 op2nd ⊢2nd⁡fw++⟨“w⁡0”⟩=w++⟨“w⁡0”⟩
34 33 fveq2i ⊢2nd⁡fw++⟨“w⁡0”⟩=w++⟨“w⁡0”⟩
35 34 oveq1i ⊢2nd⁡fw++⟨“w⁡0”⟩−1=w++⟨“w⁡0”⟩−1
36 33 35 oveq12i ⊢2nd⁡fw++⟨“w⁡0”⟩prefix2nd⁡fw++⟨“w⁡0”⟩−1=w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1
37 30 36 eqtrdi ⊢c=fw++⟨“w⁡0”⟩→2nd⁡cprefix2nd⁡c−1=w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1
38 37 2 fvmptg ⊢fw++⟨“w⁡0”⟩∈C∧w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1∈V→F⁡fw++⟨“w⁡0”⟩=w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1
39 25 26 38 sylancl ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→F⁡fw++⟨“w⁡0”⟩=w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1
40 wrdlenccats1lenm1 ⊢w∈WordVtx⁡G→w++⟨“w⁡0”⟩−1=w
41 40 ad2antrr ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w++⟨“w⁡0”⟩−1=w
42 41 oveq2d ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w++⟨“w⁡0”⟩prefixw++⟨“w⁡0”⟩−1=w++⟨“w⁡0”⟩prefixw
43 simpll ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w∈WordVtx⁡G
44 simpl ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w∈WordVtx⁡G∧1≤w
45 wrdsymb1 ⊢w∈WordVtx⁡G∧1≤w→w⁡0∈Vtx⁡G
46 44 45 syl ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w⁡0∈Vtx⁡G
47 46 s1cld ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→⟨“w⁡0”⟩∈WordVtx⁡G
48 eqidd ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=w
49 pfxccatid ⊢w∈WordVtx⁡G∧⟨“w⁡0”⟩∈WordVtx⁡G∧w=w→w++⟨“w⁡0”⟩prefixw=w
50 43 47 48 49 syl3anc ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w++⟨“w⁡0”⟩prefixw=w
51 39 42 50 3eqtrrd ⊢w∈WordVtx⁡G∧1≤w∧fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
52 51 ex ⊢w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
53 52 3adant1 ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
54 53 ad2antlr ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w∧c=fw++⟨“w⁡0”⟩→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
55 fveq2 ⊢c=fw++⟨“w⁡0”⟩→F⁡c=F⁡fw++⟨“w⁡0”⟩
56 55 eqeq2d ⊢c=fw++⟨“w⁡0”⟩→w=F⁡c↔w=F⁡fw++⟨“w⁡0”⟩
57 56 imbi2d ⊢c=fw++⟨“w⁡0”⟩→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡c↔fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
58 57 adantl ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w∧c=fw++⟨“w⁡0”⟩→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡c↔fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡fw++⟨“w⁡0”⟩
59 54 58 mpbird ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w∧c=fw++⟨“w⁡0”⟩→fw++⟨“w⁡0”⟩∈ClWalks⁡G→w=F⁡c
60 24 59 rspcimedv ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G∧G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G→∃c∈Cw=F⁡c
61 60 ex ⊢fw++⟨“w⁡0”⟩∈ClWalks⁡G→G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G→∃c∈Cw=F⁡c
62 61 pm2.43b ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fw++⟨“w⁡0”⟩∈ClWalks⁡G→∃c∈Cw=F⁡c
63 19 62 biimtrid ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→fClWalks⁡Gw++⟨“w⁡0”⟩→∃c∈Cw=F⁡c
64 63 exlimdv ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→∃ffClWalks⁡Gw++⟨“w⁡0”⟩→∃c∈Cw=F⁡c
65 18 64 sylbird ⊢G∈USHGraph∧w∈WordVtx⁡G∧1≤w→w∈ClWWalks⁡G→∃c∈Cw=F⁡c
66 65 3expib ⊢G∈USHGraph→w∈WordVtx⁡G∧1≤w→w∈ClWWalks⁡G→∃c∈Cw=F⁡c
67 66 com23 ⊢G∈USHGraph→w∈ClWWalks⁡G→w∈WordVtx⁡G∧1≤w→∃c∈Cw=F⁡c
68 67 imp ⊢G∈USHGraph∧w∈ClWWalks⁡G→w∈WordVtx⁡G∧1≤w→∃c∈Cw=F⁡c
69 16 68 mpd ⊢G∈USHGraph∧w∈ClWWalks⁡G→∃c∈Cw=F⁡c
70 69 ralrimiva ⊢G∈USHGraph→∀w∈ClWWalks⁡G∃c∈Cw=F⁡c
71 dffo3 ⊢F:C⟶ontoClWWalks⁡G↔F:C⟶ClWWalks⁡G∧∀w∈ClWWalks⁡G∃c∈Cw=F⁡c
72 3 70 71 sylanbrc ⊢G∈USHGraph→F:C⟶ontoClWWalks⁡G