Metamath Proof Explorer

Theorem uspgr2wlkeq2

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 Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 14-Apr-2021)

Ref Expression
Assertion uspgr2wlkeq2 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → 2 nd ⁡ A = 2 nd ⁡ B → A = B

Proof

Step Hyp Ref Expression
1 simpr ⊢ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → 1 st ⁡ B = N
2 1 eqcomd ⊢ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → N = 1 st ⁡ B
3 2 3ad2ant3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → N = 1 st ⁡ B
4 3 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → N = 1 st ⁡ B
5 fveq1 ⊢ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ A ⁡ i = 2 nd ⁡ B ⁡ i
6 5 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → 2 nd ⁡ A ⁡ i = 2 nd ⁡ B ⁡ i
7 6 ralrimivw ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → ∀ i ∈ 0 … N 2 nd ⁡ A ⁡ i = 2 nd ⁡ B ⁡ i
8 simpl1l ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → G ∈ USHGraph
9 simpl ⊢ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N → A ∈ Walks ⁡ G
10 simpl ⊢ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → B ∈ Walks ⁡ G
11 9 10 anim12i ⊢ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G
12 11 3adant1 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G
13 12 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G
14 simpr ⊢ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N → 1 st ⁡ A = N
15 14 eqcomd ⊢ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N → N = 1 st ⁡ A
16 15 3ad2ant2 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → N = 1 st ⁡ A
17 16 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → N = 1 st ⁡ A
18 uspgr2wlkeq ⊢ G ∈ USHGraph ∧ A ∈ Walks ⁡ G ∧ B ∈ Walks ⁡ G ∧ N = 1 st ⁡ A → A = B ↔ N = 1 st ⁡ B ∧ ∀ i ∈ 0 … N 2 nd ⁡ A ⁡ i = 2 nd ⁡ B ⁡ i
19 8 13 17 18 syl3anc ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → A = B ↔ N = 1 st ⁡ B ∧ ∀ i ∈ 0 … N 2 nd ⁡ A ⁡ i = 2 nd ⁡ B ⁡ i
20 4 7 19 mpbir2and ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N ∧ 2 nd ⁡ A = 2 nd ⁡ B → A = B
21 20 ex ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ A ∈ Walks ⁡ G ∧ 1 st ⁡ A = N ∧ B ∈ Walks ⁡ G ∧ 1 st ⁡ B = N → 2 nd ⁡ A = 2 nd ⁡ B → A = B