Metamath Proof Explorer

Theorem uspgr2wlkeqi

Description: Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021)

Ref Expression
Assertion uspgr2wlkeqi ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 2 nd ⁡ A = 2 nd ⁡ B → A = B

Proof

Step Hyp Ref Expression
1 wlkcpr ⊢ A ∈ Walks ⁡ G ↔ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A
2 wlkcpr ⊢ B ∈ Walks ⁡ G ↔ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B
3 wlkcl ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → 1 st ⁡ A ∈ ℕ 0
4 fveq2 ⊢ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ A = 2 nd ⁡ B
5 4 oveq1d ⊢ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ A − 1 = 2 nd ⁡ B − 1
6 5 eqcomd ⊢ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ B − 1 = 2 nd ⁡ A − 1
7 6 adantl ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ∧ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ B − 1 = 2 nd ⁡ A − 1
8 wlklenvm1 ⊢ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B → 1 st ⁡ B = 2 nd ⁡ B − 1
9 wlklenvm1 ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → 1 st ⁡ A = 2 nd ⁡ A − 1
10 8 9 eqeqan12rd ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ∧ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B → 1 st ⁡ B = 1 st ⁡ A ↔ 2 nd ⁡ B − 1 = 2 nd ⁡ A − 1
11 10 adantr ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ∧ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ B = 1 st ⁡ A ↔ 2 nd ⁡ B − 1 = 2 nd ⁡ A − 1
12 7 11 mpbird ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ∧ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ B = 1 st ⁡ A
13 12 anim2i ⊢ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A ∧ 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
14 13 exp44 ⊢ 1 st ⁡ A ∈ ℕ 0 → 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B → 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
15 3 14 mpcom ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → 1 st ⁡ B Walks ⁡ G 2 nd ⁡ B → 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
16 2 15 biimtrid ⊢ 1 st ⁡ A Walks ⁡ G 2 nd ⁡ A → B ∈ Walks ⁡ G → 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
17 1 16 sylbi ⊢ A ∈ Walks ⁡ G → B ∈ Walks ⁡ G → 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
18 17 imp31 ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
19 18 3adant1 ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A
20 simpl ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → G ∈ USHGraph
21 simpl ⊢ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → 1 st ⁡ A ∈ ℕ 0
22 20 21 anim12i ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → G ∈ USHGraph ∧ 1 st ⁡ A ∈ ℕ 0
23 simpl ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → A ∈ Walks ⁡ G
24 23 adantl ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → A ∈ Walks ⁡ G
25 eqidd ⊢ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → 1 st ⁡ A = 1 st ⁡ A
26 24 25 anim12i ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → A ∈ Walks ⁡ G ∧ 1 st ⁡ A = 1 st ⁡ A
27 simpr ⊢ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → B ∈ Walks ⁡ G
28 27 adantl ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → B ∈ Walks ⁡ G
29 simpr ⊢ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → 1 st ⁡ B = 1 st ⁡ A
30 28 29 anim12i ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → B ∈ Walks ⁡ G ∧ 1 st ⁡ B = 1 st ⁡ A
31 uspgr2wlkeq2 ⊢ G ∈ USHGraph ∧ 1 st ⁡ A ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = 1 st ⁡ A ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = 1 st ⁡ A → 2 nd ⁡ A = 2 nd ⁡ B → A = B
32 22 26 30 31 syl3anc ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → 2 nd ⁡ A = 2 nd ⁡ B → A = B
33 32 ex ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → 2 nd ⁡ A = 2 nd ⁡ B → A = B
34 33 com23 ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G → 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → A = B
35 34 3impia ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 2 nd ⁡ A = 2 nd ⁡ B → 1 st ⁡ A ∈ ℕ 0 ∧ 1 st ⁡ B = 1 st ⁡ A → A = B
36 19 35 mpd ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ 2 nd ⁡ A = 2 nd ⁡ B → A = B