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 ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐻 ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wlkonprop ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
3 1 wlkonprop ⊢ ( 𝐻 ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐻 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ) )
4 simp2 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
5 4 eqcomd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → 𝐴 = ( 𝑃 ‘ 0 ) )
6 simp2 ⊢ ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) → ( 𝑃 ‘ 0 ) = 𝐶 )
7 5 6 sylan9eqr ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → 𝐴 = 𝐶 )
8 simp3 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 )
9 8 eqcomd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → 𝐵 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
10 9 adantl ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → 𝐵 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
11 wlklenvm1 ⊢ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
12 wlklenvm1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
13 eqtr3 ⊢ ( ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ∧ ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐻 ) )
14 13 fveq2d ⊢ ( ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ∧ ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) )
15 14 ex ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
16 12 15 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
17 16 3ad2ant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
18 17 com12 ⊢ ( ( ♯ ‘ 𝐻 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
19 11 18 syl ⊢ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) ) )
21 20 imp ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) )
22 simpl3 ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 )
23 10 21 22 3eqtrd ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → 𝐵 = 𝐷 )
24 7 23 jca ⊢ ( ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
25 24 ex ⊢ ( ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
26 25 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐻 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
27 26 com12 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ( 𝐺 ∈ V ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐻 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
28 27 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( ( 𝐺 ∈ V ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐻 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
29 28 imp ⊢ ( ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐻 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐻 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐶 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐻 ) ) = 𝐷 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
30 2 3 29 syl2an ⊢ ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐻 ( 𝐶 ( WalksOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )