Metamath Proof Explorer


Theorem upgrwlkupwlk

Description: In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 2-Jan-2021)

Ref Expression
Assertion upgrwlkupwlk G UPGraph F Walks G P F UPWalks G P

Proof

Step Hyp Ref Expression
1 wlkv F Walks G P G V F V P V
2 eqid Vtx G = Vtx G
3 eqid iEdg G = iEdg G
4 2 3 iswlk G V F V P V F Walks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
5 simpr1 G V F V P V G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k F Word dom iEdg G
6 simpr2 G V F V P V G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k P : 0 F Vtx G
7 df-ifp if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k P k = P k + 1 iEdg G F k = P k ¬ P k = P k + 1 P k P k + 1 iEdg G F k
8 dfsn2 P k = P k P k
9 preq2 P k = P k + 1 P k P k = P k P k + 1
10 8 9 syl5eq P k = P k + 1 P k = P k P k + 1
11 10 eqeq2d P k = P k + 1 iEdg G F k = P k iEdg G F k = P k P k + 1
12 11 biimpa P k = P k + 1 iEdg G F k = P k iEdg G F k = P k P k + 1
13 12 a1d P k = P k + 1 iEdg G F k = P k F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k = P k P k + 1
14 simpr G V F V P V G UPGraph G UPGraph
15 simpl F Word dom iEdg G P : 0 F Vtx G F Word dom iEdg G
16 eqid Edg G = Edg G
17 3 16 upgredginwlk G UPGraph F Word dom iEdg G k 0 ..^ F iEdg G F k Edg G
18 14 15 17 syl2anr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G
19 18 imp F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G
20 simprr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph G UPGraph
21 20 adantr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F G UPGraph
22 21 adantr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G G UPGraph
23 22 adantr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k G UPGraph
24 simplr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k iEdg G F k Edg G
25 simprr F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k P k P k + 1 iEdg G F k
26 df-ne P k P k + 1 ¬ P k = P k + 1
27 fvexd P k P k + 1 P k V
28 fvexd P k P k + 1 P k + 1 V
29 id P k P k + 1 P k P k + 1
30 27 28 29 3jca P k P k + 1 P k V P k + 1 V P k P k + 1
31 26 30 sylbir ¬ P k = P k + 1 P k V P k + 1 V P k P k + 1
32 31 adantr ¬ P k = P k + 1 P k P k + 1 iEdg G F k P k V P k + 1 V P k P k + 1
33 32 adantl F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k P k V P k + 1 V P k P k + 1
34 2 16 upgredgpr G UPGraph iEdg G F k Edg G P k P k + 1 iEdg G F k P k V P k + 1 V P k P k + 1 P k P k + 1 = iEdg G F k
35 23 24 25 33 34 syl31anc F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k P k P k + 1 = iEdg G F k
36 35 eqcomd F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k iEdg G F k = P k P k + 1
37 36 exp31 F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k Edg G ¬ P k = P k + 1 P k P k + 1 iEdg G F k iEdg G F k = P k P k + 1
38 19 37 mpd F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F ¬ P k = P k + 1 P k P k + 1 iEdg G F k iEdg G F k = P k P k + 1
39 38 com12 ¬ P k = P k + 1 P k P k + 1 iEdg G F k F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k = P k P k + 1
40 13 39 jaoi P k = P k + 1 iEdg G F k = P k ¬ P k = P k + 1 P k P k + 1 iEdg G F k F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F iEdg G F k = P k P k + 1
41 40 com12 F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F P k = P k + 1 iEdg G F k = P k ¬ P k = P k + 1 P k P k + 1 iEdg G F k iEdg G F k = P k P k + 1
42 7 41 syl5bi F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k iEdg G F k = P k P k + 1
43 42 ralimdva F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k k 0 ..^ F iEdg G F k = P k P k + 1
44 43 ex F Word dom iEdg G P : 0 F Vtx G G V F V P V G UPGraph k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k k 0 ..^ F iEdg G F k = P k P k + 1
45 44 com23 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k G V F V P V G UPGraph k 0 ..^ F iEdg G F k = P k P k + 1
46 45 3impia F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k G V F V P V G UPGraph k 0 ..^ F iEdg G F k = P k P k + 1
47 46 impcom G V F V P V G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k k 0 ..^ F iEdg G F k = P k P k + 1
48 5 6 47 3jca G V F V P V G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
49 48 exp31 G V F V P V G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
50 49 com23 G V F V P V F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
51 4 50 sylbid G V F V P V F Walks G P G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
52 51 impd G V F V P V F Walks G P G UPGraph F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
53 52 impcom F Walks G P G UPGraph G V F V P V F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
54 2 3 isupwlk G V F V P V F UPWalks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
55 54 adantl F Walks G P G UPGraph G V F V P V F UPWalks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
56 53 55 mpbird F Walks G P G UPGraph G V F V P V F UPWalks G P
57 56 exp31 F Walks G P G UPGraph G V F V P V F UPWalks G P
58 1 57 mpid F Walks G P G UPGraph F UPWalks G P
59 58 impcom G UPGraph F Walks G P F UPWalks G P