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 ⊢ I = iEdg ⁡ G
Assertion ewlkinedg ⊢ F ∈ G EdgWalks S ∧ K ∈ 1 ..^ F → S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K

Proof

Step Hyp Ref Expression
1 ewlksfval.i ⊢ I = iEdg ⁡ G
2 1 ewlkprop ⊢ F ∈ G EdgWalks S → G ∈ V ∧ S ∈ ℕ 0 * ∧ F ∈ Word dom ⁡ I ∧ ∀ k ∈ 1 ..^ F S ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k
3 fvoveq1 ⊢ k = K → F ⁡ k − 1 = F ⁡ K − 1
4 3 fveq2d ⊢ k = K → I ⁡ F ⁡ k − 1 = I ⁡ F ⁡ K − 1
5 2fveq3 ⊢ k = K → I ⁡ F ⁡ k = I ⁡ F ⁡ K
6 4 5 ineq12d ⊢ k = K → I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k = I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
7 6 fveq2d ⊢ k = K → I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k = I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
8 7 breq2d ⊢ k = K → S ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k ↔ S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
9 8 rspccv ⊢ ∀ k ∈ 1 ..^ F S ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k → K ∈ 1 ..^ F → S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
10 9 3ad2ant3 ⊢ G ∈ V ∧ S ∈ ℕ 0 * ∧ F ∈ Word dom ⁡ I ∧ ∀ k ∈ 1 ..^ F S ≤ I ⁡ F ⁡ k − 1 ∩ I ⁡ F ⁡ k → K ∈ 1 ..^ F → S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
11 2 10 syl ⊢ F ∈ G EdgWalks S → K ∈ 1 ..^ F → S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K
12 11 imp ⊢ F ∈ G EdgWalks S ∧ K ∈ 1 ..^ F → S ≤ I ⁡ F ⁡ K − 1 ∩ I ⁡ F ⁡ K