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 GUSHGraphAWalksGBWalksGN=1stAA=BN=1stBy0N2ndAy=2ndBy

Proof

Step Hyp Ref Expression
1 3anan32 N=1stBy0..^N1stAy=1stByy0N2ndAy=2ndByN=1stBy0N2ndAy=2ndByy0..^N1stAy=1stBy
2 1 a1i GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N1stAy=1stByy0N2ndAy=2ndByN=1stBy0N2ndAy=2ndByy0..^N1stAy=1stBy
3 wlkeq AWalksGBWalksGN=1stAA=BN=1stBy0..^N1stAy=1stByy0N2ndAy=2ndBy
4 3 3expa AWalksGBWalksGN=1stAA=BN=1stBy0..^N1stAy=1stByy0N2ndAy=2ndBy
5 4 3adant1 GUSHGraphAWalksGBWalksGN=1stAA=BN=1stBy0..^N1stAy=1stByy0N2ndAy=2ndBy
6 fzofzp1 x0..^Nx+10N
7 6 adantl GUSHGraphAWalksGBWalksGN=1stAN=1stBx0..^Nx+10N
8 fveq2 y=x+12ndAy=2ndAx+1
9 fveq2 y=x+12ndBy=2ndBx+1
10 8 9 eqeq12d y=x+12ndAy=2ndBy2ndAx+1=2ndBx+1
11 10 adantl GUSHGraphAWalksGBWalksGN=1stAN=1stBx0..^Ny=x+12ndAy=2ndBy2ndAx+1=2ndBx+1
12 7 11 rspcdv GUSHGraphAWalksGBWalksGN=1stAN=1stBx0..^Ny0N2ndAy=2ndBy2ndAx+1=2ndBx+1
13 12 impancom GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByx0..^N2ndAx+1=2ndBx+1
14 13 ralrimiv GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByx0..^N2ndAx+1=2ndBx+1
15 fvoveq1 y=x2ndAy+1=2ndAx+1
16 fvoveq1 y=x2ndBy+1=2ndBx+1
17 15 16 eqeq12d y=x2ndAy+1=2ndBy+12ndAx+1=2ndBx+1
18 17 cbvralvw y0..^N2ndAy+1=2ndBy+1x0..^N2ndAx+1=2ndBx+1
19 14 18 sylibr GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1
20 fzossfz 0..^N0N
21 ssralv 0..^N0Ny0N2ndAy=2ndByy0..^N2ndAy=2ndBy
22 20 21 mp1i GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy=2ndBy
23 r19.26 y0..^N2ndAy=2ndBy2ndAy+1=2ndBy+1y0..^N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1
24 preq12 2ndAy=2ndBy2ndAy+1=2ndBy+12ndAy2ndAy+1=2ndBy2ndBy+1
25 24 a1i GUSHGraphAWalksGBWalksGN=1stAN=1stB2ndAy=2ndBy2ndAy+1=2ndBy+12ndAy2ndAy+1=2ndBy2ndBy+1
26 25 ralimdv GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N2ndAy=2ndBy2ndAy+1=2ndBy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
27 23 26 syl5bir GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
28 27 expd GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
29 22 28 syld GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
30 29 imp GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy+1=2ndBy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
31 19 30 mpd GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
32 31 ex GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1
33 uspgrupgr GUSHGraphGUPGraph
34 eqid VtxG=VtxG
35 eqid iEdgG=iEdgG
36 eqid 1stA=1stA
37 eqid 2ndA=2ndA
38 34 35 36 37 upgrwlkcompim GUPGraphAWalksG1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+1
39 38 ex GUPGraphAWalksG1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+1
40 33 39 syl GUSHGraphAWalksG1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+1
41 eqid 1stB=1stB
42 eqid 2ndB=2ndB
43 34 35 41 42 upgrwlkcompim GUPGraphBWalksG1stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1
44 43 ex GUPGraphBWalksG1stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1
45 33 44 syl GUSHGraphBWalksG1stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1
46 oveq2 1stB=N0..^1stB=0..^N
47 46 eqcoms N=1stB0..^1stB=0..^N
48 47 raleqdv N=1stBy0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^NiEdgG1stBy=2ndBy2ndBy+1
49 oveq2 1stA=N0..^1stA=0..^N
50 49 eqcoms N=1stA0..^1stA=0..^N
51 50 raleqdv N=1stAy0..^1stAiEdgG1stAy=2ndAy2ndAy+1y0..^NiEdgG1stAy=2ndAy2ndAy+1
52 48 51 bi2anan9r N=1stAN=1stBy0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^1stAiEdgG1stAy=2ndAy2ndAy+1y0..^NiEdgG1stBy=2ndBy2ndBy+1y0..^NiEdgG1stAy=2ndAy2ndAy+1
53 r19.26 y0..^NiEdgG1stBy=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+1y0..^NiEdgG1stBy=2ndBy2ndBy+1y0..^NiEdgG1stAy=2ndAy2ndAy+1
54 eqeq2 2ndAy2ndAy+1=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+1iEdgG1stAy=2ndBy2ndBy+1
55 eqeq2 2ndBy2ndBy+1=iEdgG1stAyiEdgG1stBy=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
56 55 eqcoms iEdgG1stAy=2ndBy2ndBy+1iEdgG1stBy=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
57 56 biimpd iEdgG1stAy=2ndBy2ndBy+1iEdgG1stBy=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
58 54 57 syl6bi 2ndAy2ndAy+1=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+1iEdgG1stBy=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
59 58 com13 iEdgG1stBy=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+12ndAy2ndAy+1=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
60 59 imp iEdgG1stBy=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+12ndAy2ndAy+1=2ndBy2ndBy+1iEdgG1stBy=iEdgG1stAy
61 60 ral2imi y0..^NiEdgG1stBy=2ndBy2ndBy+1iEdgG1stAy=2ndAy2ndAy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
62 53 61 sylbir y0..^NiEdgG1stBy=2ndBy2ndBy+1y0..^NiEdgG1stAy=2ndAy2ndAy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
63 52 62 syl6bi N=1stAN=1stBy0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^1stAiEdgG1stAy=2ndAy2ndAy+1y0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
64 63 com12 y0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^1stAiEdgG1stAy=2ndAy2ndAy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
65 64 ex y0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^1stAiEdgG1stAy=2ndAy2ndAy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
66 65 3ad2ant3 1stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1y0..^1stAiEdgG1stAy=2ndAy2ndAy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
67 66 com12 y0..^1stAiEdgG1stAy=2ndAy2ndAy+11stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
68 67 3ad2ant3 1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+11stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
69 68 imp 1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+11stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
70 69 expd 1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+11stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
71 70 a1i GUSHGraph1stAWorddomiEdgG2ndA:01stAVtxGy0..^1stAiEdgG1stAy=2ndAy2ndAy+11stBWorddomiEdgG2ndB:01stBVtxGy0..^1stBiEdgG1stBy=2ndBy2ndBy+1N=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
72 40 45 71 syl2and GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
73 72 3imp1 GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N2ndAy2ndAy+1=2ndBy2ndBy+1y0..^NiEdgG1stBy=iEdgG1stAy
74 eqcom iEdgG1stBy=iEdgG1stAyiEdgG1stAy=iEdgG1stBy
75 35 uspgrf1oedg GUSHGraphiEdgG:domiEdgG1-1 ontoEdgG
76 f1of1 iEdgG:domiEdgG1-1 ontoEdgGiEdgG:domiEdgG1-1EdgG
77 75 76 syl GUSHGraphiEdgG:domiEdgG1-1EdgG
78 eqidd GUSHGraphiEdgG=iEdgG
79 eqidd GUSHGraphdomiEdgG=domiEdgG
80 edgval EdgG=raniEdgG
81 80 eqcomi raniEdgG=EdgG
82 81 a1i GUSHGraphraniEdgG=EdgG
83 78 79 82 f1eq123d GUSHGraphiEdgG:domiEdgG1-1raniEdgGiEdgG:domiEdgG1-1EdgG
84 77 83 mpbird GUSHGraphiEdgG:domiEdgG1-1raniEdgG
85 84 3ad2ant1 GUSHGraphAWalksGBWalksGN=1stAiEdgG:domiEdgG1-1raniEdgG
86 85 adantr GUSHGraphAWalksGBWalksGN=1stAN=1stBiEdgG:domiEdgG1-1raniEdgG
87 34 35 36 37 wlkelwrd AWalksG1stAWorddomiEdgG2ndA:01stAVtxG
88 34 35 41 42 wlkelwrd BWalksG1stBWorddomiEdgG2ndB:01stBVtxG
89 oveq2 N=1stA0..^N=0..^1stA
90 89 eleq2d N=1stAy0..^Ny0..^1stA
91 wrdsymbcl 1stAWorddomiEdgGy0..^1stA1stAydomiEdgG
92 91 expcom y0..^1stA1stAWorddomiEdgG1stAydomiEdgG
93 90 92 syl6bi N=1stAy0..^N1stAWorddomiEdgG1stAydomiEdgG
94 93 adantr N=1stAN=1stBy0..^N1stAWorddomiEdgG1stAydomiEdgG
95 94 imp N=1stAN=1stBy0..^N1stAWorddomiEdgG1stAydomiEdgG
96 95 com12 1stAWorddomiEdgGN=1stAN=1stBy0..^N1stAydomiEdgG
97 96 adantl 1stBWorddomiEdgG1stAWorddomiEdgGN=1stAN=1stBy0..^N1stAydomiEdgG
98 oveq2 N=1stB0..^N=0..^1stB
99 98 eleq2d N=1stBy0..^Ny0..^1stB
100 wrdsymbcl 1stBWorddomiEdgGy0..^1stB1stBydomiEdgG
101 100 expcom y0..^1stB1stBWorddomiEdgG1stBydomiEdgG
102 99 101 syl6bi N=1stBy0..^N1stBWorddomiEdgG1stBydomiEdgG
103 102 adantl N=1stAN=1stBy0..^N1stBWorddomiEdgG1stBydomiEdgG
104 103 imp N=1stAN=1stBy0..^N1stBWorddomiEdgG1stBydomiEdgG
105 104 com12 1stBWorddomiEdgGN=1stAN=1stBy0..^N1stBydomiEdgG
106 105 adantr 1stBWorddomiEdgG1stAWorddomiEdgGN=1stAN=1stBy0..^N1stBydomiEdgG
107 97 106 jcad 1stBWorddomiEdgG1stAWorddomiEdgGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
108 107 ex 1stBWorddomiEdgG1stAWorddomiEdgGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
109 108 adantr 1stBWorddomiEdgG2ndB:01stBVtxG1stAWorddomiEdgGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
110 109 com12 1stAWorddomiEdgG1stBWorddomiEdgG2ndB:01stBVtxGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
111 110 adantr 1stAWorddomiEdgG2ndA:01stAVtxG1stBWorddomiEdgG2ndB:01stBVtxGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
112 111 imp 1stAWorddomiEdgG2ndA:01stAVtxG1stBWorddomiEdgG2ndB:01stBVtxGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
113 87 88 112 syl2an AWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
114 113 expd AWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
115 114 expd AWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
116 115 imp AWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
117 116 3adant1 GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
118 117 imp GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
119 118 imp GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^N1stAydomiEdgG1stBydomiEdgG
120 f1veqaeq iEdgG:domiEdgG1-1raniEdgG1stAydomiEdgG1stBydomiEdgGiEdgG1stAy=iEdgG1stBy1stAy=1stBy
121 86 119 120 syl2an2r GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^NiEdgG1stAy=iEdgG1stBy1stAy=1stBy
122 74 121 syl5bi GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^NiEdgG1stBy=iEdgG1stAy1stAy=1stBy
123 122 ralimdva GUSHGraphAWalksGBWalksGN=1stAN=1stBy0..^NiEdgG1stBy=iEdgG1stAyy0..^N1stAy=1stBy
124 32 73 123 3syld GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N1stAy=1stBy
125 124 expimpd GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByy0..^N1stAy=1stBy
126 125 pm4.71d GUSHGraphAWalksGBWalksGN=1stAN=1stBy0N2ndAy=2ndByN=1stBy0N2ndAy=2ndByy0..^N1stAy=1stBy
127 2 5 126 3bitr4d GUSHGraphAWalksGBWalksGN=1stAA=BN=1stBy0N2ndAy=2ndBy