This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2wlkd

Description: Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018) (Revised by AV, 23-Jan-2021) (Proof shortened by AV, 14-Feb-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
2wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
2wlkd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2wlkd.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion 2wlkd ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4 2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
5 2wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
6 2wlkd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
7 2wlkd.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
8 s3cli ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V
9 1 8 eqeltri ⊢ 𝑃 ∈ Word V
10 9 a1i ⊢ ( 𝜑 → 𝑃 ∈ Word V )
11 s2cli ⊢ ⟨“ 𝐽 𝐾 ”⟩ ∈ Word V
12 2 11 eqeltri ⊢ 𝐹 ∈ Word V
13 12 a1i ⊢ ( 𝜑 → 𝐹 ∈ Word V )
14 1 2 2wlkdlem1 ⊢ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 )
15 14 a1i ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
16 1 2 3 4 5 2wlkdlem10 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
17 1 2 3 4 2wlkdlem5 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
18 6 1vgrex ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ V )
19 18 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐺 ∈ V )
20 3 19 syl ⊢ ( 𝜑 → 𝐺 ∈ V )
21 1 2 3 2wlkdlem4 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
22 10 13 15 16 17 20 6 7 21 wlkd ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )