Metamath Proof Explorer

Theorem lfgriswlk

Description: Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021)

Ref Expression
Hypotheses lfgrwlkprop.i ⊢ I = iEdg ⁡ G
lfgriswlk.v ⊢ V = Vtx ⁡ G
Assertion lfgriswlk ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i ⊢ I = iEdg ⁡ G
2 lfgriswlk.v ⊢ V = Vtx ⁡ G
3 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
4 3 adantl ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → F ∈ Word dom ⁡ I
5 2 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ V
6 5 adantl ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → P : 0 … F ⟶ V
7 1 lfgrwlkprop ⊢ F Walks ⁡ G P ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
8 7 expcom ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
9 8 adantl ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
10 9 imp ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
11 1 wlkvtxeledg ⊢ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
12 11 adantl ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
13 r19.26 ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
14 10 12 13 sylanbrc ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
15 4 6 14 3jca ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
16 simpr1 ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F ∈ Word dom ⁡ I
17 simpr2 ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P : 0 … F ⟶ V
18 df-ne ⊢ P ⁡ k ≠ P ⁡ k + 1 ↔ ¬ P ⁡ k = P ⁡ k + 1
19 ifpfal ⊢ ¬ P ⁡ k = P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
20 18 19 sylbi ⊢ P ⁡ k ≠ P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
21 20 biimpar ⊢ P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
22 21 ralimi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
23 22 3ad2ant3 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
24 23 adantl ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
25 2 1 iswlkg ⊢ G ∈ W → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
26 25 ad2antrr ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
27 16 17 24 26 mpbir3and ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F Walks ⁡ G P
28 15 27 impbida ⊢ G ∈ W ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k