Metamath Proof Explorer

Theorem wlkiswwlks2

Description: A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Assertion wlkiswwlks2 ⊢G∈USHGraph→P∈WWalks⁡G→∃ffWalks⁡GP

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 wwlkbp ⊢P∈WWalks⁡G→G∈V∧P∈WordVtx⁡G
3 eqid ⊢Edg⁡G=Edg⁡G
4 1 3 iswwlks ⊢P∈WWalks⁡G↔P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G
5 ovex ⊢0..^P−1∈V
6 mptexg ⊢0..^P−1∈V→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈V
7 5 6 mp1i ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈V
8 simprr ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→G∈USHGraph
9 simplr ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→P∈WordVtx⁡G
10 hashge1 ⊢P∈WordVtx⁡G∧P≠∅→1≤P
11 10 ancoms ⊢P≠∅∧P∈WordVtx⁡G→1≤P
12 11 adantr ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→1≤P
13 8 9 12 3jca ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→G∈USHGraph∧P∈WordVtx⁡G∧1≤P
14 13 adantr ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→G∈USHGraph∧P∈WordVtx⁡G∧1≤P
15 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
16 15 a1i ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→Edg⁡G=ran⁡iEdg⁡G
17 16 eleq2d ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→P⁡iP⁡i+1∈Edg⁡G↔P⁡iP⁡i+1∈ran⁡iEdg⁡G
18 17 ralbidv ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G↔∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡iEdg⁡G
19 18 biimpd ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡iEdg⁡G
20 eqid ⊢x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1
21 eqid ⊢iEdg⁡G=iEdg⁡G
22 20 21 wlkiswwlks2lem6 ⊢G∈USHGraph∧P∈WordVtx⁡G∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡iEdg⁡G→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G∧P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G∧∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
23 14 19 22 sylsyld ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G∧P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G∧∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
24 eleq1 ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→f∈Worddom⁡iEdg⁡G↔x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G
25 fveq2 ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1
26 25 oveq2d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→0…f=0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1
27 26 feq2d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→P:0…f⟶Vtx⁡G↔P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G
28 25 oveq2d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→0..^f=0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1
29 fveq1 ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→f⁡i=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i
30 29 fveqeq2d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→iEdg⁡G⁡f⁡i=P⁡iP⁡i+1↔iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
31 28 30 raleqbidv ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1↔∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
32 24 27 31 3anbi123d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1↔x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G∧P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G∧∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
33 32 imbi2d ⊢f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G∧P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G∧∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
34 33 adantl ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1∈Worddom⁡iEdg⁡G∧P:0…x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⟶Vtx⁡G∧∀i∈0..^x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1iEdg⁡G⁡x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1⁡i=P⁡iP⁡i+1
35 23 34 mpbird ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph∧f=x∈0..^P−1⟼iEdg⁡G-1⁡P⁡xP⁡x+1→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
36 7 35 spcimedv ⊢P≠∅∧P∈WordVtx⁡G∧G∈V∧P∈WordVtx⁡G∧G∈USHGraph→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
37 36 ex ⊢P≠∅∧P∈WordVtx⁡G→G∈V∧P∈WordVtx⁡G∧G∈USHGraph→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
38 37 com23 ⊢P≠∅∧P∈WordVtx⁡G→∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈V∧P∈WordVtx⁡G∧G∈USHGraph→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
39 38 3impia ⊢P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈V∧P∈WordVtx⁡G∧G∈USHGraph→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
40 39 expd ⊢P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈V∧P∈WordVtx⁡G→G∈USHGraph→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
41 40 impcom ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈USHGraph→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
42 41 imp ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G∧G∈USHGraph→∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
43 uspgrupgr ⊢G∈USHGraph→G∈UPGraph
44 1 21 upgriswlk ⊢G∈UPGraph→fWalks⁡GP↔f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
45 43 44 syl ⊢G∈USHGraph→fWalks⁡GP↔f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
46 45 adantl ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G∧G∈USHGraph→fWalks⁡GP↔f∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
47 46 exbidv ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G∧G∈USHGraph→∃ffWalks⁡GP↔∃ff∈Worddom⁡iEdg⁡G∧P:0…f⟶Vtx⁡G∧∀i∈0..^fiEdg⁡G⁡f⁡i=P⁡iP⁡i+1
48 42 47 mpbird ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G∧G∈USHGraph→∃ffWalks⁡GP
49 48 ex ⊢G∈V∧P∈WordVtx⁡G∧P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈USHGraph→∃ffWalks⁡GP
50 49 ex ⊢G∈V∧P∈WordVtx⁡G→P≠∅∧P∈WordVtx⁡G∧∀i∈0..^P−1P⁡iP⁡i+1∈Edg⁡G→G∈USHGraph→∃ffWalks⁡GP
51 4 50 biimtrid ⊢G∈V∧P∈WordVtx⁡G→P∈WWalks⁡G→G∈USHGraph→∃ffWalks⁡GP
52 2 51 mpcom ⊢P∈WWalks⁡G→G∈USHGraph→∃ffWalks⁡GP
53 52 com12 ⊢G∈USHGraph→P∈WWalks⁡G→∃ffWalks⁡GP