Metamath Proof Explorer

Theorem clwlkclwwlk

Description: A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlk.v ⊢V=Vtx⁡G
clwlkclwwlk.e ⊢E=iEdg⁡G
Assertion clwlkclwwlk ⊢G∈USHGraph∧P∈WordV∧2≤P→∃ffClWalks⁡GP↔lastS⁡P=P⁡0∧PprefixP−1∈ClWWalks⁡G

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v ⊢V=Vtx⁡G
2 clwlkclwwlk.e ⊢E=iEdg⁡G
3 2 uspgrf1oedg ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoEdg⁡G
4 f1of1 ⊢E:dom⁡E⟶1-1 ontoEdg⁡G→E:dom⁡E⟶1-1Edg⁡G
5 3 4 syl ⊢G∈USHGraph→E:dom⁡E⟶1-1Edg⁡G
6 clwlkclwwlklem3 ⊢E:dom⁡E⟶1-1Edg⁡G∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
7 5 6 syl3an1 ⊢G∈USHGraph∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
8 lencl ⊢P∈WordV→P∈ℕ0
9 ige2m1fz ⊢P∈ℕ0∧2≤P→P−1∈0…P
10 8 9 sylan ⊢P∈WordV∧2≤P→P−1∈0…P
11 pfxlen ⊢P∈WordV∧P−1∈0…P→PprefixP−1=P−1
12 10 11 syldan ⊢P∈WordV∧2≤P→PprefixP−1=P−1
13 8 nn0cnd ⊢P∈WordV→P∈ℂ
14 1cnd ⊢P∈WordV→1∈ℂ
15 13 14 subcld ⊢P∈WordV→P−1∈ℂ
16 15 subid1d ⊢P∈WordV→P-1-0=P−1
17 16 eqcomd ⊢P∈WordV→P−1=P-1-0
18 17 adantr ⊢P∈WordV∧2≤P→P−1=P-1-0
19 12 18 eqtrd ⊢P∈WordV∧2≤P→PprefixP−1=P-1-0
20 19 oveq1d ⊢P∈WordV∧2≤P→PprefixP−1−1=P−1-0-1
21 20 oveq2d ⊢P∈WordV∧2≤P→0..^PprefixP−1−1=0..^P−1-0-1
22 12 oveq1d ⊢P∈WordV∧2≤P→PprefixP−1−1=P-1-1
23 22 oveq2d ⊢P∈WordV∧2≤P→0..^PprefixP−1−1=0..^P-1-1
24 23 eleq2d ⊢P∈WordV∧2≤P→i∈0..^PprefixP−1−1↔i∈0..^P-1-1
25 simpll ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→P∈WordV
26 wrdlenge2n0 ⊢P∈WordV∧2≤P→P≠∅
27 26 adantr ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→P≠∅
28 nn0z ⊢P∈ℕ0→P∈ℤ
29 peano2zm ⊢P∈ℤ→P−1∈ℤ
30 28 29 syl ⊢P∈ℕ0→P−1∈ℤ
31 8 30 syl ⊢P∈WordV→P−1∈ℤ
32 31 adantr ⊢P∈WordV∧2≤P→P−1∈ℤ
33 elfzom1elfzo ⊢P−1∈ℤ∧i∈0..^P-1-1→i∈0..^P−1
34 32 33 sylan ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→i∈0..^P−1
35 pfxtrcfv ⊢P∈WordV∧P≠∅∧i∈0..^P−1→PprefixP−1⁡i=P⁡i
36 25 27 34 35 syl3anc ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→PprefixP−1⁡i=P⁡i
37 8 adantr ⊢P∈WordV∧2≤P→P∈ℕ0
38 elfzom1elp1fzo ⊢P−1∈ℤ∧i∈0..^P-1-1→i+1∈0..^P−1
39 30 38 sylan ⊢P∈ℕ0∧i∈0..^P-1-1→i+1∈0..^P−1
40 37 39 sylan ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→i+1∈0..^P−1
41 pfxtrcfv ⊢P∈WordV∧P≠∅∧i+1∈0..^P−1→PprefixP−1⁡i+1=P⁡i+1
42 25 27 40 41 syl3anc ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→PprefixP−1⁡i+1=P⁡i+1
43 36 42 preq12d ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→PprefixP−1⁡iPprefixP−1⁡i+1=P⁡iP⁡i+1
44 43 eleq1d ⊢P∈WordV∧2≤P∧i∈0..^P-1-1→PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E↔P⁡iP⁡i+1∈ran⁡E
45 44 ex ⊢P∈WordV∧2≤P→i∈0..^P-1-1→PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E↔P⁡iP⁡i+1∈ran⁡E
46 24 45 sylbid ⊢P∈WordV∧2≤P→i∈0..^PprefixP−1−1→PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E↔P⁡iP⁡i+1∈ran⁡E
47 46 imp ⊢P∈WordV∧2≤P∧i∈0..^PprefixP−1−1→PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E↔P⁡iP⁡i+1∈ran⁡E
48 21 47 raleqbidva ⊢P∈WordV∧2≤P→∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E↔∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E
49 pfxtrcfvl ⊢P∈WordV∧2≤P→lastS⁡PprefixP−1=P⁡P−2
50 pfxtrcfv0 ⊢P∈WordV∧2≤P→PprefixP−1⁡0=P⁡0
51 49 50 preq12d ⊢P∈WordV∧2≤P→lastS⁡PprefixP−1PprefixP−1⁡0=P⁡P−2P⁡0
52 51 eleq1d ⊢P∈WordV∧2≤P→lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E↔P⁡P−2P⁡0∈ran⁡E
53 48 52 anbi12d ⊢P∈WordV∧2≤P→∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E↔∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E
54 53 bicomd ⊢P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
55 54 3adant1 ⊢G∈USHGraph∧P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
56 pfxcl ⊢P∈WordV→PprefixP−1∈WordV
57 56 3ad2ant2 ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈WordV
58 57 3biant1d ⊢G∈USHGraph∧P∈WordV∧2≤P→∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
59 55 58 bitrd ⊢G∈USHGraph∧P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
60 59 anbi2d ⊢G∈USHGraph∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E↔lastS⁡P=P⁡0∧PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
61 7 60 bitrd ⊢G∈USHGraph∧P∈WordV∧2≤P→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
62 uspgrupgr ⊢G∈USHGraph→G∈UPGraph
63 1 2 isclwlkupgr ⊢G∈UPGraph→fClWalks⁡GP↔f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
64 3an4anass ⊢f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
65 63 64 bitr4di ⊢G∈UPGraph→fClWalks⁡GP↔f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
66 62 65 syl ⊢G∈USHGraph→fClWalks⁡GP↔f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
67 66 adantr ⊢G∈USHGraph∧P∈WordV→fClWalks⁡GP↔f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
68 67 exbidv ⊢G∈USHGraph∧P∈WordV→∃ffClWalks⁡GP↔∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
69 68 3adant3 ⊢G∈USHGraph∧P∈WordV∧2≤P→∃ffClWalks⁡GP↔∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
70 eqid ⊢Edg⁡G=Edg⁡G
71 1 70 isclwwlk ⊢PprefixP−1∈ClWWalks⁡G↔PprefixP−1∈WordV∧PprefixP−1≠∅∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G∧lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G
72 simpl ⊢P∈WordV∧2≤P→P∈WordV
73 nn0ge2m1nn ⊢P∈ℕ0∧2≤P→P−1∈ℕ
74 8 73 sylan ⊢P∈WordV∧2≤P→P−1∈ℕ
75 nn0re ⊢P∈ℕ0→P∈ℝ
76 75 lem1d ⊢P∈ℕ0→P−1≤P
77 76 a1d ⊢P∈ℕ0→2≤P→P−1≤P
78 8 77 syl ⊢P∈WordV→2≤P→P−1≤P
79 78 imp ⊢P∈WordV∧2≤P→P−1≤P
80 72 74 79 3jca ⊢P∈WordV∧2≤P→P∈WordV∧P−1∈ℕ∧P−1≤P
81 80 3adant1 ⊢G∈USHGraph∧P∈WordV∧2≤P→P∈WordV∧P−1∈ℕ∧P−1≤P
82 pfxn0 ⊢P∈WordV∧P−1∈ℕ∧P−1≤P→PprefixP−1≠∅
83 81 82 syl ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1≠∅
84 83 biantrud ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈WordV↔PprefixP−1∈WordV∧PprefixP−1≠∅
85 84 bicomd ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈WordV∧PprefixP−1≠∅↔PprefixP−1∈WordV
86 85 3anbi1d ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈WordV∧PprefixP−1≠∅∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G∧lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G∧lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G
87 71 86 bitrid ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈ClWWalks⁡G↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G∧lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G
88 biid ⊢PprefixP−1∈WordV↔PprefixP−1∈WordV
89 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
90 2 eqcomi ⊢iEdg⁡G=E
91 90 rneqi ⊢ran⁡iEdg⁡G=ran⁡E
92 89 91 eqtri ⊢Edg⁡G=ran⁡E
93 92 eleq2i ⊢PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G↔PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E
94 93 ralbii ⊢∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G↔∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E
95 92 eleq2i ⊢lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G↔lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
96 88 94 95 3anbi123i ⊢PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈Edg⁡G∧lastS⁡PprefixP−1PprefixP−1⁡0∈Edg⁡G↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
97 87 96 bitrdi ⊢G∈USHGraph∧P∈WordV∧2≤P→PprefixP−1∈ClWWalks⁡G↔PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
98 97 anbi2d ⊢G∈USHGraph∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧PprefixP−1∈ClWWalks⁡G↔lastS⁡P=P⁡0∧PprefixP−1∈WordV∧∀i∈0..^PprefixP−1−1PprefixP−1⁡iPprefixP−1⁡i+1∈ran⁡E∧lastS⁡PprefixP−1PprefixP−1⁡0∈ran⁡E
99 61 69 98 3bitr4d ⊢G∈USHGraph∧P∈WordV∧2≤P→∃ffClWalks⁡GP↔lastS⁡P=P⁡0∧PprefixP−1∈ClWWalks⁡G