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 Word V 2 P f f ClWalks G P lastS P = P 0 P prefix P 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 onto Edg G
4 f1of1 E : dom E 1-1 onto Edg G E : dom E 1-1 Edg G
5 3 4 syl G USHGraph E : dom E 1-1 Edg G
6 clwlkclwwlklem3 E : dom E 1-1 Edg G P Word V 2 P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E
7 5 6 syl3an1 G USHGraph P Word V 2 P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E
8 lencl P Word V P 0
9 ige2m1fz P 0 2 P P 1 0 P
10 8 9 sylan P Word V 2 P P 1 0 P
11 pfxlen P Word V P 1 0 P P prefix P 1 = P 1
12 10 11 syldan P Word V 2 P P prefix P 1 = P 1
13 8 nn0cnd P Word V P
14 1cnd P Word V 1
15 13 14 subcld P Word V P 1
16 15 subid1d P Word V P - 1 - 0 = P 1
17 16 eqcomd P Word V P 1 = P - 1 - 0
18 17 adantr P Word V 2 P P 1 = P - 1 - 0
19 12 18 eqtrd P Word V 2 P P prefix P 1 = P - 1 - 0
20 19 oveq1d P Word V 2 P P prefix P 1 1 = P 1 - 0 - 1
21 20 oveq2d P Word V 2 P 0 ..^ P prefix P 1 1 = 0 ..^ P 1 - 0 - 1
22 12 oveq1d P Word V 2 P P prefix P 1 1 = P - 1 - 1
23 22 oveq2d P Word V 2 P 0 ..^ P prefix P 1 1 = 0 ..^ P - 1 - 1
24 23 eleq2d P Word V 2 P i 0 ..^ P prefix P 1 1 i 0 ..^ P - 1 - 1
25 simpll P Word V 2 P i 0 ..^ P - 1 - 1 P Word V
26 wrdlenge2n0 P Word V 2 P P
27 26 adantr P Word V 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 Word V P 1
32 31 adantr P Word V 2 P P 1
33 elfzom1elfzo P 1 i 0 ..^ P - 1 - 1 i 0 ..^ P 1
34 32 33 sylan P Word V 2 P i 0 ..^ P - 1 - 1 i 0 ..^ P 1
35 pfxtrcfv P Word V P i 0 ..^ P 1 P prefix P 1 i = P i
36 25 27 34 35 syl3anc P Word V 2 P i 0 ..^ P - 1 - 1 P prefix P 1 i = P i
37 8 adantr P Word V 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 Word V 2 P i 0 ..^ P - 1 - 1 i + 1 0 ..^ P 1
41 pfxtrcfv P Word V P i + 1 0 ..^ P 1 P prefix P 1 i + 1 = P i + 1
42 25 27 40 41 syl3anc P Word V 2 P i 0 ..^ P - 1 - 1 P prefix P 1 i + 1 = P i + 1
43 36 42 preq12d P Word V 2 P i 0 ..^ P - 1 - 1 P prefix P 1 i P prefix P 1 i + 1 = P i P i + 1
44 43 eleq1d P Word V 2 P i 0 ..^ P - 1 - 1 P prefix P 1 i P prefix P 1 i + 1 ran E P i P i + 1 ran E
45 44 ex P Word V 2 P i 0 ..^ P - 1 - 1 P prefix P 1 i P prefix P 1 i + 1 ran E P i P i + 1 ran E
46 24 45 sylbid P Word V 2 P i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E P i P i + 1 ran E
47 46 imp P Word V 2 P i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E P i P i + 1 ran E
48 21 47 raleqbidva P Word V 2 P i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E
49 pfxtrcfvl P Word V 2 P lastS P prefix P 1 = P P 2
50 pfxtrcfv0 P Word V 2 P P prefix P 1 0 = P 0
51 49 50 preq12d P Word V 2 P lastS P prefix P 1 P prefix P 1 0 = P P 2 P 0
52 51 eleq1d P Word V 2 P lastS P prefix P 1 P prefix P 1 0 ran E P P 2 P 0 ran E
53 48 52 anbi12d P Word V 2 P i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E
54 53 bicomd P Word V 2 P i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
55 54 3adant1 G USHGraph P Word V 2 P i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
56 pfxcl P Word V P prefix P 1 Word V
57 56 3ad2ant2 G USHGraph P Word V 2 P P prefix P 1 Word V
58 57 3biant1d G USHGraph P Word V 2 P i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
59 55 58 bitrd G USHGraph P Word V 2 P i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
60 59 anbi2d G USHGraph P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E lastS P = P 0 P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
61 7 60 bitrd G USHGraph P Word V 2 P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f lastS P = P 0 P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
62 uspgrupgr G USHGraph G UPGraph
63 1 2 isclwlkupgr G UPGraph f ClWalks G P f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
64 3an4anass f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
65 63 64 bitr4di G UPGraph f ClWalks G P f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
66 62 65 syl G USHGraph f ClWalks G P f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
67 66 adantr G USHGraph P Word V f ClWalks G P f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
68 67 exbidv G USHGraph P Word V f f ClWalks G P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
69 68 3adant3 G USHGraph P Word V 2 P f f ClWalks G P f f Word dom E P : 0 f V i 0 ..^ f E f i = P i P i + 1 P 0 = P f
70 eqid Edg G = Edg G
71 1 70 isclwwlk P prefix P 1 ClWWalks G P prefix P 1 Word V P prefix P 1 i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G lastS P prefix P 1 P prefix P 1 0 Edg G
72 simpl P Word V 2 P P Word V
73 nn0ge2m1nn P 0 2 P P 1
74 8 73 sylan P Word V 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 Word V 2 P P 1 P
79 78 imp P Word V 2 P P 1 P
80 72 74 79 3jca P Word V 2 P P Word V P 1 P 1 P
81 80 3adant1 G USHGraph P Word V 2 P P Word V P 1 P 1 P
82 pfxn0 P Word V P 1 P 1 P P prefix P 1
83 81 82 syl G USHGraph P Word V 2 P P prefix P 1
84 83 biantrud G USHGraph P Word V 2 P P prefix P 1 Word V P prefix P 1 Word V P prefix P 1
85 84 bicomd G USHGraph P Word V 2 P P prefix P 1 Word V P prefix P 1 P prefix P 1 Word V
86 85 3anbi1d G USHGraph P Word V 2 P P prefix P 1 Word V P prefix P 1 i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G lastS P prefix P 1 P prefix P 1 0 Edg G P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G lastS P prefix P 1 P prefix P 1 0 Edg G
87 71 86 syl5bb G USHGraph P Word V 2 P P prefix P 1 ClWWalks G P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G lastS P prefix P 1 P prefix P 1 0 Edg G
88 biid P prefix P 1 Word V P prefix P 1 Word V
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 P prefix P 1 i P prefix P 1 i + 1 Edg G P prefix P 1 i P prefix P 1 i + 1 ran E
94 93 ralbii i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E
95 92 eleq2i lastS P prefix P 1 P prefix P 1 0 Edg G lastS P prefix P 1 P prefix P 1 0 ran E
96 88 94 95 3anbi123i P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 Edg G lastS P prefix P 1 P prefix P 1 0 Edg G P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
97 87 96 bitrdi G USHGraph P Word V 2 P P prefix P 1 ClWWalks G P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
98 97 anbi2d G USHGraph P Word V 2 P lastS P = P 0 P prefix P 1 ClWWalks G lastS P = P 0 P prefix P 1 Word V i 0 ..^ P prefix P 1 1 P prefix P 1 i P prefix P 1 i + 1 ran E lastS P prefix P 1 P prefix P 1 0 ran E
99 61 69 98 3bitr4d G USHGraph P Word V 2 P f f ClWalks G P lastS P = P 0 P prefix P 1 ClWWalks G