Metamath Proof Explorer

Theorem wlksoneq1eq2

Description: Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021)

Ref Expression
Assertion wlksoneq1eq2 ⊢ F A WalksOn ⁡ G B P ∧ H C WalksOn ⁡ G D P → A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 wlkonprop ⊢ F A WalksOn ⁡ G B P → G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
3 1 wlkonprop ⊢ H C WalksOn ⁡ G D P → G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ H ∈ V ∧ P ∈ V ∧ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D
4 simp2 ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ 0 = A
5 4 eqcomd ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A = P ⁡ 0
6 simp2 ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → P ⁡ 0 = C
7 5 6 sylan9eqr ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A = C
8 simp3 ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = B
9 8 eqcomd ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → B = P ⁡ F
10 9 adantl ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → B = P ⁡ F
11 wlklenvm1 ⊢ H Walks ⁡ G P → H = P − 1
12 wlklenvm1 ⊢ F Walks ⁡ G P → F = P − 1
13 eqtr3 ⊢ F = P − 1 ∧ H = P − 1 → F = H
14 13 fveq2d ⊢ F = P − 1 ∧ H = P − 1 → P ⁡ F = P ⁡ H
15 14 ex ⊢ F = P − 1 → H = P − 1 → P ⁡ F = P ⁡ H
16 12 15 syl ⊢ F Walks ⁡ G P → H = P − 1 → P ⁡ F = P ⁡ H
17 16 3ad2ant1 ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → H = P − 1 → P ⁡ F = P ⁡ H
18 17 com12 ⊢ H = P − 1 → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = P ⁡ H
19 11 18 syl ⊢ H Walks ⁡ G P → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = P ⁡ H
20 19 3ad2ant1 ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = P ⁡ H
21 20 imp ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ F = P ⁡ H
22 simpl3 ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → P ⁡ H = D
23 10 21 22 3eqtrd ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → B = D
24 7 23 jca ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A = C ∧ B = D
25 24 ex ⊢ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A = C ∧ B = D
26 25 3ad2ant3 ⊢ G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ H ∈ V ∧ P ∈ V ∧ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → A = C ∧ B = D
27 26 com12 ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ H ∈ V ∧ P ∈ V ∧ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → A = C ∧ B = D
28 27 3ad2ant3 ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ H ∈ V ∧ P ∈ V ∧ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → A = C ∧ B = D
29 28 imp ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B ∧ G ∈ V ∧ C ∈ Vtx ⁡ G ∧ D ∈ Vtx ⁡ G ∧ H ∈ V ∧ P ∈ V ∧ H Walks ⁡ G P ∧ P ⁡ 0 = C ∧ P ⁡ H = D → A = C ∧ B = D
30 2 3 29 syl2an ⊢ F A WalksOn ⁡ G B P ∧ H C WalksOn ⁡ G D P → A = C ∧ B = D