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

Metamath Proof Explorer

Theorem ewlkinedg

Description: The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion ewlkinedg ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 𝐾 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 ewlkprop ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
3 fvoveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝐹 ‘ ( 𝑘 − 1 ) ) = ( 𝐹 ‘ ( 𝐾 − 1 ) ) )
4 3 fveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) )
5 2fveq3 ⊢ ( 𝑘 = 𝐾 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) )
6 4 5 ineq12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) )
7 6 fveq2d ⊢ ( 𝑘 = 𝐾 → ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) )
8 7 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) ) )
9 8 rspccv ⊢ ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( 𝐾 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) ) )
10 9 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) → ( 𝐾 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) ) )
11 2 10 syl ⊢ ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) → ( 𝐾 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) ) )
12 11 imp ⊢ ( ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ∧ 𝐾 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝐾 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) )