Metamath Proof Explorer

Theorem lfgrwlkprop

Description: Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021)

Ref Expression
Hypothesis lfgrwlkprop.i ⊢ I = iEdg ⁡ G
Assertion lfgrwlkprop ⊢ F Walks ⁡ G P ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i ⊢ I = iEdg ⁡ G
2 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 1 iswlk ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 2 4 syl ⊢ F Walks ⁡ G P → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
6 ifptru ⊢ P ⁡ k = P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ I ⁡ F ⁡ k = P ⁡ k
7 6 adantr ⊢ P ⁡ k = P ⁡ k + 1 ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ I ⁡ F ⁡ k = P ⁡ k
8 simplr ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x
9 wrdsymbcl ⊢ F ∈ Word dom ⁡ I ∧ k ∈ 0 ..^ F → F ⁡ k ∈ dom ⁡ I
10 9 ad4ant14 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → F ⁡ k ∈ dom ⁡ I
11 8 10 ffvelcdmd ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I ⁡ F ⁡ k ∈ x ∈ 𝒫 V | 2 ≤ x
12 fveq2 ⊢ x = I ⁡ F ⁡ k → x = I ⁡ F ⁡ k
13 12 breq2d ⊢ x = I ⁡ F ⁡ k → 2 ≤ x ↔ 2 ≤ I ⁡ F ⁡ k
14 13 elrab ⊢ I ⁡ F ⁡ k ∈ x ∈ 𝒫 V | 2 ≤ x ↔ I ⁡ F ⁡ k ∈ 𝒫 V ∧ 2 ≤ I ⁡ F ⁡ k
15 fveq2 ⊢ I ⁡ F ⁡ k = P ⁡ k → I ⁡ F ⁡ k = P ⁡ k
16 15 breq2d ⊢ I ⁡ F ⁡ k = P ⁡ k → 2 ≤ I ⁡ F ⁡ k ↔ 2 ≤ P ⁡ k
17 fvex ⊢ P ⁡ k ∈ V
18 hashsng ⊢ P ⁡ k ∈ V → P ⁡ k = 1
19 17 18 ax-mp ⊢ P ⁡ k = 1
20 19 breq2i ⊢ 2 ≤ P ⁡ k ↔ 2 ≤ 1
21 1lt2 ⊢ 1 < 2
22 1re ⊢ 1 ∈ ℝ
23 2re ⊢ 2 ∈ ℝ
24 22 23 ltnlei ⊢ 1 < 2 ↔ ¬ 2 ≤ 1
25 pm2.21 ⊢ ¬ 2 ≤ 1 → 2 ≤ 1 → P ⁡ k ≠ P ⁡ k + 1
26 24 25 sylbi ⊢ 1 < 2 → 2 ≤ 1 → P ⁡ k ≠ P ⁡ k + 1
27 21 26 ax-mp ⊢ 2 ≤ 1 → P ⁡ k ≠ P ⁡ k + 1
28 20 27 sylbi ⊢ 2 ≤ P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
29 16 28 biimtrdi ⊢ I ⁡ F ⁡ k = P ⁡ k → 2 ≤ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
30 29 com12 ⊢ 2 ≤ I ⁡ F ⁡ k → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
31 30 adantl ⊢ I ⁡ F ⁡ k ∈ 𝒫 V ∧ 2 ≤ I ⁡ F ⁡ k → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
32 31 a1i ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I ⁡ F ⁡ k ∈ 𝒫 V ∧ 2 ≤ I ⁡ F ⁡ k → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
33 14 32 biimtrid ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I ⁡ F ⁡ k ∈ x ∈ 𝒫 V | 2 ≤ x → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
34 11 33 mpd ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
35 34 adantl ⊢ P ⁡ k = P ⁡ k + 1 ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → I ⁡ F ⁡ k = P ⁡ k → P ⁡ k ≠ P ⁡ k + 1
36 7 35 sylbid ⊢ P ⁡ k = P ⁡ k + 1 ∧ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
37 36 ex ⊢ P ⁡ k = P ⁡ k + 1 → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
38 neqne ⊢ ¬ P ⁡ k = P ⁡ k + 1 → P ⁡ k ≠ P ⁡ k + 1
39 38 2a1d ⊢ ¬ P ⁡ k = P ⁡ k + 1 → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
40 37 39 pm2.61i ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ k ∈ 0 ..^ F → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ≠ P ⁡ k + 1
41 40 ralimdva ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
42 41 ex ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
43 42 com23 ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
44 43 3impia ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
45 5 44 biimtrdi ⊢ F Walks ⁡ G P → F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
46 45 pm2.43i ⊢ F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
47 46 imp ⊢ F Walks ⁡ G P ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1