Metamath Proof Explorer


Theorem uspgr2wlkeq

Description: Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018) (Revised by AV, 14-Apr-2021)

Ref Expression
Assertion uspgr2wlkeq G USHGraph A Walks G B Walks G N = 1 st A A = B N = 1 st B y 0 N 2 nd A y = 2 nd B y

Proof

Step Hyp Ref Expression
1 3anan32 N = 1 st B y 0 ..^ N 1 st A y = 1 st B y y 0 N 2 nd A y = 2 nd B y N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 1 st A y = 1 st B y
2 1 a1i G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y = 1 st B y y 0 N 2 nd A y = 2 nd B y N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 1 st A y = 1 st B y
3 wlkeq A Walks G B Walks G N = 1 st A A = B N = 1 st B y 0 ..^ N 1 st A y = 1 st B y y 0 N 2 nd A y = 2 nd B y
4 3 3expa A Walks G B Walks G N = 1 st A A = B N = 1 st B y 0 ..^ N 1 st A y = 1 st B y y 0 N 2 nd A y = 2 nd B y
5 4 3adant1 G USHGraph A Walks G B Walks G N = 1 st A A = B N = 1 st B y 0 ..^ N 1 st A y = 1 st B y y 0 N 2 nd A y = 2 nd B y
6 fzofzp1 x 0 ..^ N x + 1 0 N
7 6 adantl G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B x 0 ..^ N x + 1 0 N
8 fveq2 y = x + 1 2 nd A y = 2 nd A x + 1
9 fveq2 y = x + 1 2 nd B y = 2 nd B x + 1
10 8 9 eqeq12d y = x + 1 2 nd A y = 2 nd B y 2 nd A x + 1 = 2 nd B x + 1
11 10 adantl G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B x 0 ..^ N y = x + 1 2 nd A y = 2 nd B y 2 nd A x + 1 = 2 nd B x + 1
12 7 11 rspcdv G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B x 0 ..^ N y 0 N 2 nd A y = 2 nd B y 2 nd A x + 1 = 2 nd B x + 1
13 12 impancom G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y x 0 ..^ N 2 nd A x + 1 = 2 nd B x + 1
14 13 ralrimiv G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y x 0 ..^ N 2 nd A x + 1 = 2 nd B x + 1
15 fvoveq1 y = x 2 nd A y + 1 = 2 nd A x + 1
16 fvoveq1 y = x 2 nd B y + 1 = 2 nd B x + 1
17 15 16 eqeq12d y = x 2 nd A y + 1 = 2 nd B y + 1 2 nd A x + 1 = 2 nd B x + 1
18 17 cbvralvw y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1 x 0 ..^ N 2 nd A x + 1 = 2 nd B x + 1
19 14 18 sylibr G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1
20 fzossfz 0 ..^ N 0 N
21 ssralv 0 ..^ N 0 N y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y = 2 nd B y
22 20 21 mp1i G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y = 2 nd B y
23 r19.26 y 0 ..^ N 2 nd A y = 2 nd B y 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1
24 preq12 2 nd A y = 2 nd B y 2 nd A y + 1 = 2 nd B y + 1 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
25 24 a1i G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B 2 nd A y = 2 nd B y 2 nd A y + 1 = 2 nd B y + 1 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
26 25 ralimdv G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y = 2 nd B y 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
27 23 26 syl5bir G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
28 27 expd G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
29 22 28 syld G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
30 29 imp G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y + 1 = 2 nd B y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
31 19 30 mpd G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
32 31 ex G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1
33 uspgrupgr G USHGraph G UPGraph
34 eqid Vtx G = Vtx G
35 eqid iEdg G = iEdg G
36 eqid 1 st A = 1 st A
37 eqid 2 nd A = 2 nd A
38 34 35 36 37 upgrwlkcompim G UPGraph A Walks G 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
39 38 ex G UPGraph A Walks G 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
40 33 39 syl G USHGraph A Walks G 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
41 eqid 1 st B = 1 st B
42 eqid 2 nd B = 2 nd B
43 34 35 41 42 upgrwlkcompim G UPGraph B Walks G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1
44 43 ex G UPGraph B Walks G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1
45 33 44 syl G USHGraph B Walks G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1
46 oveq2 1 st B = N 0 ..^ 1 st B = 0 ..^ N
47 46 eqcoms N = 1 st B 0 ..^ 1 st B = 0 ..^ N
48 47 raleqdv N = 1 st B y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1
49 oveq2 1 st A = N 0 ..^ 1 st A = 0 ..^ N
50 49 eqcoms N = 1 st A 0 ..^ 1 st A = 0 ..^ N
51 50 raleqdv N = 1 st A y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
52 48 51 bi2anan9r N = 1 st A N = 1 st B y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
53 r19.26 y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st A y = 2 nd A y 2 nd A y + 1
54 eqeq2 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 iEdg G 1 st A y = 2 nd B y 2 nd B y + 1
55 eqeq2 2 nd B y 2 nd B y + 1 = iEdg G 1 st A y iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
56 55 eqcoms iEdg G 1 st A y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
57 56 biimpd iEdg G 1 st A y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
58 54 57 syl6bi 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
59 58 com13 iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
60 59 imp iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 iEdg G 1 st B y = iEdg G 1 st A y
61 60 ral2imi y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
62 53 61 sylbir y 0 ..^ N iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
63 52 62 syl6bi N = 1 st A N = 1 st B y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
64 63 com12 y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
65 64 ex y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
66 65 3ad2ant3 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
67 66 com12 y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
68 67 3ad2ant3 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
69 68 imp 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
70 69 expd 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
71 70 a1i G USHGraph 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G y 0 ..^ 1 st A iEdg G 1 st A y = 2 nd A y 2 nd A y + 1 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G y 0 ..^ 1 st B iEdg G 1 st B y = 2 nd B y 2 nd B y + 1 N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
72 40 45 71 syl2and G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
73 72 3imp1 G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 2 nd A y 2 nd A y + 1 = 2 nd B y 2 nd B y + 1 y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y
74 eqcom iEdg G 1 st B y = iEdg G 1 st A y iEdg G 1 st A y = iEdg G 1 st B y
75 35 uspgrf1oedg G USHGraph iEdg G : dom iEdg G 1-1 onto Edg G
76 f1of1 iEdg G : dom iEdg G 1-1 onto Edg G iEdg G : dom iEdg G 1-1 Edg G
77 75 76 syl G USHGraph iEdg G : dom iEdg G 1-1 Edg G
78 eqidd G USHGraph iEdg G = iEdg G
79 eqidd G USHGraph dom iEdg G = dom iEdg G
80 edgval Edg G = ran iEdg G
81 80 eqcomi ran iEdg G = Edg G
82 81 a1i G USHGraph ran iEdg G = Edg G
83 78 79 82 f1eq123d G USHGraph iEdg G : dom iEdg G 1-1 ran iEdg G iEdg G : dom iEdg G 1-1 Edg G
84 77 83 mpbird G USHGraph iEdg G : dom iEdg G 1-1 ran iEdg G
85 84 3ad2ant1 G USHGraph A Walks G B Walks G N = 1 st A iEdg G : dom iEdg G 1-1 ran iEdg G
86 85 adantr G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B iEdg G : dom iEdg G 1-1 ran iEdg G
87 34 35 36 37 wlkelwrd A Walks G 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G
88 34 35 41 42 wlkelwrd B Walks G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G
89 oveq2 N = 1 st A 0 ..^ N = 0 ..^ 1 st A
90 89 eleq2d N = 1 st A y 0 ..^ N y 0 ..^ 1 st A
91 wrdsymbcl 1 st A Word dom iEdg G y 0 ..^ 1 st A 1 st A y dom iEdg G
92 91 expcom y 0 ..^ 1 st A 1 st A Word dom iEdg G 1 st A y dom iEdg G
93 90 92 syl6bi N = 1 st A y 0 ..^ N 1 st A Word dom iEdg G 1 st A y dom iEdg G
94 93 adantr N = 1 st A N = 1 st B y 0 ..^ N 1 st A Word dom iEdg G 1 st A y dom iEdg G
95 94 imp N = 1 st A N = 1 st B y 0 ..^ N 1 st A Word dom iEdg G 1 st A y dom iEdg G
96 95 com12 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G
97 96 adantl 1 st B Word dom iEdg G 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G
98 oveq2 N = 1 st B 0 ..^ N = 0 ..^ 1 st B
99 98 eleq2d N = 1 st B y 0 ..^ N y 0 ..^ 1 st B
100 wrdsymbcl 1 st B Word dom iEdg G y 0 ..^ 1 st B 1 st B y dom iEdg G
101 100 expcom y 0 ..^ 1 st B 1 st B Word dom iEdg G 1 st B y dom iEdg G
102 99 101 syl6bi N = 1 st B y 0 ..^ N 1 st B Word dom iEdg G 1 st B y dom iEdg G
103 102 adantl N = 1 st A N = 1 st B y 0 ..^ N 1 st B Word dom iEdg G 1 st B y dom iEdg G
104 103 imp N = 1 st A N = 1 st B y 0 ..^ N 1 st B Word dom iEdg G 1 st B y dom iEdg G
105 104 com12 1 st B Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st B y dom iEdg G
106 105 adantr 1 st B Word dom iEdg G 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st B y dom iEdg G
107 97 106 jcad 1 st B Word dom iEdg G 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
108 107 ex 1 st B Word dom iEdg G 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
109 108 adantr 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G 1 st A Word dom iEdg G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
110 109 com12 1 st A Word dom iEdg G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
111 110 adantr 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
112 111 imp 1 st A Word dom iEdg G 2 nd A : 0 1 st A Vtx G 1 st B Word dom iEdg G 2 nd B : 0 1 st B Vtx G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
113 87 88 112 syl2an A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
114 113 expd A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
115 114 expd A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
116 115 imp A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
117 116 3adant1 G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
118 117 imp G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
119 118 imp G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N 1 st A y dom iEdg G 1 st B y dom iEdg G
120 f1veqaeq iEdg G : dom iEdg G 1-1 ran iEdg G 1 st A y dom iEdg G 1 st B y dom iEdg G iEdg G 1 st A y = iEdg G 1 st B y 1 st A y = 1 st B y
121 86 119 120 syl2an2r G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N iEdg G 1 st A y = iEdg G 1 st B y 1 st A y = 1 st B y
122 74 121 syl5bi G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y 1 st A y = 1 st B y
123 122 ralimdva G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 ..^ N iEdg G 1 st B y = iEdg G 1 st A y y 0 ..^ N 1 st A y = 1 st B y
124 32 73 123 3syld G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 1 st A y = 1 st B y
125 124 expimpd G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 1 st A y = 1 st B y
126 125 pm4.71d G USHGraph A Walks G B Walks G N = 1 st A N = 1 st B y 0 N 2 nd A y = 2 nd B y N = 1 st B y 0 N 2 nd A y = 2 nd B y y 0 ..^ N 1 st A y = 1 st B y
127 2 5 126 3bitr4d G USHGraph A Walks G B Walks G N = 1 st A A = B N = 1 st B y 0 N 2 nd A y = 2 nd B y