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 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ) ) )