Metamath Proof Explorer


Theorem upgr2wlk

Description: Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018) (Revised by AV, 3-Jan-2021) (Revised by AV, 28-Oct-2021)

Ref Expression
Hypotheses upgr2wlk.v V = Vtx G
upgr2wlk.i I = iEdg G
Assertion upgr2wlk G UPGraph F Walks G P F = 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2

Proof

Step Hyp Ref Expression
1 upgr2wlk.v V = Vtx G
2 upgr2wlk.i I = iEdg G
3 1 2 upgriswlk G UPGraph F Walks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
4 3 anbi1d G UPGraph F Walks G P F = 2 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F = 2
5 iswrdb F Word dom I F : 0 ..^ F dom I
6 oveq2 F = 2 0 ..^ F = 0 ..^ 2
7 6 feq2d F = 2 F : 0 ..^ F dom I F : 0 ..^ 2 dom I
8 5 7 syl5bb F = 2 F Word dom I F : 0 ..^ 2 dom I
9 oveq2 F = 2 0 F = 0 2
10 9 feq2d F = 2 P : 0 F V P : 0 2 V
11 fzo0to2pr 0 ..^ 2 = 0 1
12 6 11 eqtrdi F = 2 0 ..^ F = 0 1
13 12 raleqdv F = 2 k 0 ..^ F I F k = P k P k + 1 k 0 1 I F k = P k P k + 1
14 2wlklem k 0 1 I F k = P k P k + 1 I F 0 = P 0 P 1 I F 1 = P 1 P 2
15 13 14 bitrdi F = 2 k 0 ..^ F I F k = P k P k + 1 I F 0 = P 0 P 1 I F 1 = P 1 P 2
16 8 10 15 3anbi123d F = 2 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
17 16 adantl G UPGraph F = 2 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
18 3anass F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
19 17 18 bitrdi G UPGraph F = 2 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
20 19 ex G UPGraph F = 2 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
21 20 pm5.32rd G UPGraph F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F = 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F = 2
22 3anass F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
23 an32 F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F = 2
24 22 23 bitri F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F = 2
25 21 24 bitr4di G UPGraph F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F = 2 F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
26 2nn0 2 0
27 fnfzo0hash 2 0 F : 0 ..^ 2 dom I F = 2
28 26 27 mpan F : 0 ..^ 2 dom I F = 2
29 28 pm4.71i F : 0 ..^ 2 dom I F : 0 ..^ 2 dom I F = 2
30 29 bicomi F : 0 ..^ 2 dom I F = 2 F : 0 ..^ 2 dom I
31 30 a1i G UPGraph F : 0 ..^ 2 dom I F = 2 F : 0 ..^ 2 dom I
32 31 3anbi1d G UPGraph F : 0 ..^ 2 dom I F = 2 P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2
33 4 25 32 3bitrd G UPGraph F Walks G P F = 2 F : 0 ..^ 2 dom I P : 0 2 V I F 0 = P 0 P 1 I F 1 = P 1 P 2