Metamath Proof Explorer

Theorem wlkeq

Description: Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018) (Revised by AV, 16-May-2019) (Revised by AV, 14-Apr-2021)

Ref Expression
Assertion wlkeq ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → A = B ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 eqid ⊢ 1 st ⁡ A = 1 st ⁡ A
4 eqid ⊢ 2 nd ⁡ A = 2 nd ⁡ A
5 1 2 3 4 wlkelwrd ⊢ A ∈ Walks ⁡ G → 1 st ⁡ A ∈ Word dom ⁡ iEdg ⁡ G ∧ 2 nd ⁡ A : 0 … 1 st ⁡ A ⟶ Vtx ⁡ G
6 eqid ⊢ 1 st ⁡ B = 1 st ⁡ B
7 eqid ⊢ 2 nd ⁡ B = 2 nd ⁡ B
8 1 2 6 7 wlkelwrd ⊢ B ∈ Walks ⁡ G → 1 st ⁡ B ∈ Word dom ⁡ iEdg ⁡ G ∧ 2 nd ⁡ B : 0 … 1 st ⁡ B ⟶ Vtx ⁡ G
9 5 8 anim12i ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 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
10 wlkop ⊢ A ∈ Walks ⁡ G → A = 1 st ⁡ A 2 nd ⁡ A
11 eleq1 ⊢ A = 1 st ⁡ A 2 nd ⁡ A → A ∈ Walks ⁡ G ↔ 1 st ⁡ A 2 nd ⁡ A ∈ Walks ⁡ G
12 df-br ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ↔ 1 st ⁡ A 2 nd ⁡ A ∈ Walks ⁡ G
13 wlklenvm1 ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → 1 st ⁡ A = 2 nd ⁡ A − 1
14 12 13 sylbir ⊢ 1 st ⁡ A 2 nd ⁡ A ∈ Walks ⁡ G → 1 st ⁡ A = 2 nd ⁡ A − 1
15 11 14 biimtrdi ⊢ A = 1 st ⁡ A 2 nd ⁡ A → A ∈ Walks ⁡ G → 1 st ⁡ A = 2 nd ⁡ A − 1
16 10 15 mpcom ⊢ A ∈ Walks ⁡ G → 1 st ⁡ A = 2 nd ⁡ A − 1
17 wlkop ⊢ B ∈ Walks ⁡ G → B = 1 st ⁡ B 2 nd ⁡ B
18 eleq1 ⊢ B = 1 st ⁡ B 2 nd ⁡ B → B ∈ Walks ⁡ G ↔ 1 st ⁡ B 2 nd ⁡ B ∈ Walks ⁡ G
19 df-br ⊢ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B ↔ 1 st ⁡ B 2 nd ⁡ B ∈ Walks ⁡ G
20 wlklenvm1 ⊢ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B → 1 st ⁡ B = 2 nd ⁡ B − 1
21 19 20 sylbir ⊢ 1 st ⁡ B 2 nd ⁡ B ∈ Walks ⁡ G → 1 st ⁡ B = 2 nd ⁡ B − 1
22 18 21 biimtrdi ⊢ B = 1 st ⁡ B 2 nd ⁡ B → B ∈ Walks ⁡ G → 1 st ⁡ B = 2 nd ⁡ B − 1
23 17 22 mpcom ⊢ B ∈ Walks ⁡ G → 1 st ⁡ B = 2 nd ⁡ B − 1
24 16 23 anim12i ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 1 st ⁡ A = 2 nd ⁡ A − 1 ∧ 1 st ⁡ B = 2 nd ⁡ B − 1
25 eqwrd ⊢ 1 st ⁡ A ∈ Word dom ⁡ iEdg ⁡ G ∧ 1 st ⁡ B ∈ Word dom ⁡ iEdg ⁡ G → 1 st ⁡ A = 1 st ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x
26 25 ad2ant2r ⊢ 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 → 1 st ⁡ A = 1 st ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x
27 26 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 ∧ 1 st ⁡ A = 2 nd ⁡ A − 1 ∧ 1 st ⁡ B = 2 nd ⁡ B − 1 → 1 st ⁡ A = 1 st ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x
28 lencl ⊢ 1 st ⁡ A ∈ Word dom ⁡ iEdg ⁡ G → 1 st ⁡ A ∈ ℕ 0
29 28 adantr ⊢ 1 st ⁡ A ∈ Word dom ⁡ iEdg ⁡ G ∧ 2 nd ⁡ A : 0 … 1 st ⁡ A ⟶ Vtx ⁡ G → 1 st ⁡ A ∈ ℕ 0
30 simpr ⊢ 1 st ⁡ A ∈ Word dom ⁡ iEdg ⁡ G ∧ 2 nd ⁡ A : 0 … 1 st ⁡ A ⟶ Vtx ⁡ G → 2 nd ⁡ A : 0 … 1 st ⁡ A ⟶ Vtx ⁡ G
31 simpr ⊢ 1 st ⁡ B ∈ Word dom ⁡ iEdg ⁡ G ∧ 2 nd ⁡ B : 0 … 1 st ⁡ B ⟶ Vtx ⁡ G → 2 nd ⁡ B : 0 … 1 st ⁡ B ⟶ Vtx ⁡ G
32 2ffzeq ⊢ 1 st ⁡ A ∈ ℕ 0 ∧ 2 nd ⁡ A : 0 … 1 st ⁡ A ⟶ Vtx ⁡ G ∧ 2 nd ⁡ B : 0 … 1 st ⁡ B ⟶ Vtx ⁡ G → 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
33 29 30 31 32 syl2an3an ⊢ 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 → 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
34 33 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 ∧ 1 st ⁡ A = 2 nd ⁡ A − 1 ∧ 1 st ⁡ B = 2 nd ⁡ B − 1 → 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
35 27 34 anbi12d ⊢ 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 ∧ 1 st ⁡ A = 2 nd ⁡ A − 1 ∧ 1 st ⁡ B = 2 nd ⁡ B − 1 → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
36 9 24 35 syl2anc ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
37 36 3adant3 ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
38 eqeq1 ⊢ N = 1 st ⁡ A → N = 1 st ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B
39 oveq2 ⊢ N = 1 st ⁡ A → 0 ..^ N = 0 ..^ 1 st ⁡ A
40 39 raleqdv ⊢ N = 1 st ⁡ A → ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ↔ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x
41 38 40 anbi12d ⊢ N = 1 st ⁡ A → N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x
42 oveq2 ⊢ N = 1 st ⁡ A → 0 … N = 0 … 1 st ⁡ A
43 42 raleqdv ⊢ N = 1 st ⁡ A → ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
44 38 43 anbi12d ⊢ N = 1 st ⁡ A → N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
45 41 44 anbi12d ⊢ N = 1 st ⁡ A → N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
46 45 bibi2d ⊢ N = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
47 46 3ad2ant3 ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ 1 st ⁡ A 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ 1 st ⁡ A = 1 st ⁡ B ∧ ∀ x ∈ 0 … 1 st ⁡ A 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
48 37 47 mpbird ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
49 1st2ndb ⊢ A ∈ V × V ↔ A = 1 st ⁡ A 2 nd ⁡ A
50 10 49 sylibr ⊢ A ∈ Walks ⁡ G → A ∈ V × V
51 1st2ndb ⊢ B ∈ V × V ↔ B = 1 st ⁡ B 2 nd ⁡ B
52 17 51 sylibr ⊢ B ∈ Walks ⁡ G → B ∈ V × V
53 xpopth ⊢ A ∈ V × V ∧ B ∈ V × V → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ A = B
54 50 52 53 syl2an ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ A = B
55 54 3adant3 ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ A = B
56 3anass ⊢ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
57 anandi ⊢ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
58 56 57 bitr2i ⊢ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
59 58 a1i ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ N = 1 st ⁡ B ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x
60 48 55 59 3bitr3d ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → A = B ↔ N = 1 st ⁡ B ∧ ∀ x ∈ 0 ..^ N 1 st ⁡ A ⁡ x = 1 st ⁡ B ⁡ x ∧ ∀ x ∈ 0 … N 2 nd ⁡ A ⁡ x = 2 nd ⁡ B ⁡ x