| Step | Hyp | Ref
| Expression |
| 1 | | wlkp1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | wlkp1.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
| 3 | | wlkp1.f |
. . . 4
⊢ (𝜑 → Fun 𝐼) |
| 4 | | wlkp1.a |
. . . 4
⊢ (𝜑 → 𝐼 ∈ Fin) |
| 5 | | wlkp1.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 6 | | wlkp1.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 7 | | wlkp1.d |
. . . 4
⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) |
| 8 | | wlkp1.w |
. . . 4
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
| 9 | | wlkp1.n |
. . . 4
⊢ 𝑁 = (♯‘𝐹) |
| 10 | | wlkp1.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
| 11 | | wlkp1.x |
. . . 4
⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) |
| 12 | | wlkp1.u |
. . . 4
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
| 13 | | wlkp1.h |
. . . 4
⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) |
| 14 | | wlkp1.q |
. . . 4
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
| 15 | | wlkp1.s |
. . . 4
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
| 16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem5 29695 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) |
| 17 | | elfzofz 13715 |
. . . . . . 7
⊢ (𝑘 ∈ (0..^𝑁) → 𝑘 ∈ (0...𝑁)) |
| 18 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝑘 ∈ (0...𝑁)) |
| 19 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑄‘𝑥) = (𝑄‘𝑘)) |
| 20 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘)) |
| 21 | 19, 20 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((𝑄‘𝑥) = (𝑃‘𝑥) ↔ (𝑄‘𝑘) = (𝑃‘𝑘))) |
| 22 | 21 | rspcv 3618 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥) → (𝑄‘𝑘) = (𝑃‘𝑘))) |
| 23 | 18, 22 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥) → (𝑄‘𝑘) = (𝑃‘𝑘))) |
| 24 | 23 | imp 406 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) → (𝑄‘𝑘) = (𝑃‘𝑘)) |
| 25 | | fzofzp1 13803 |
. . . . . . 7
⊢ (𝑘 ∈ (0..^𝑁) → (𝑘 + 1) ∈ (0...𝑁)) |
| 26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝑘 + 1) ∈ (0...𝑁)) |
| 27 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝑄‘𝑥) = (𝑄‘(𝑘 + 1))) |
| 28 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1))) |
| 29 | 27, 28 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((𝑄‘𝑥) = (𝑃‘𝑥) ↔ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)))) |
| 30 | 29 | rspcv 3618 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)))) |
| 31 | 26, 30 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)))) |
| 32 | 31 | imp 406 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) → (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) |
| 33 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
| 34 | 13 | fveq1i 6907 |
. . . . . . . 8
⊢ (𝐻‘𝑘) = ((𝐹 ∪ {〈𝑁, 𝐵〉})‘𝑘) |
| 35 | | fzonel 13713 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑁 ∈ (0..^𝑁) |
| 36 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = 𝑘 → (𝑁 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0..^𝑁))) |
| 37 | 35, 36 | mtbii 326 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 𝑘 → ¬ 𝑘 ∈ (0..^𝑁)) |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 = 𝑘 → ¬ 𝑘 ∈ (0..^𝑁))) |
| 39 | 38 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) → ¬ 𝑁 = 𝑘)) |
| 40 | 39 | imp 406 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ¬ 𝑁 = 𝑘) |
| 41 | 40 | neqned 2947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝑁 ≠ 𝑘) |
| 42 | | fvunsn 7199 |
. . . . . . . . 9
⊢ (𝑁 ≠ 𝑘 → ((𝐹 ∪ {〈𝑁, 𝐵〉})‘𝑘) = (𝐹‘𝑘)) |
| 43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐹 ∪ {〈𝑁, 𝐵〉})‘𝑘) = (𝐹‘𝑘)) |
| 44 | 34, 43 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐻‘𝑘) = (𝐹‘𝑘)) |
| 45 | 33, 44 | fveq12d 6913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = ((𝐼 ∪ {〈𝐵, 𝐸〉})‘(𝐹‘𝑘))) |
| 46 | 9 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝑁) =
(0..^(♯‘𝐹)) |
| 47 | 46 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0..^𝑁) ↔ 𝑘 ∈ (0..^(♯‘𝐹))) |
| 48 | 2 | wlkf 29632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 49 | 8, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
| 50 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝐹‘𝑘) ∈ dom 𝐼) |
| 51 | 50 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Word dom 𝐼 → (𝑘 ∈ (0..^(♯‘𝐹)) → (𝐹‘𝑘) ∈ dom 𝐼)) |
| 52 | 49, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (0..^(♯‘𝐹)) → (𝐹‘𝑘) ∈ dom 𝐼)) |
| 53 | 47, 52 | biimtrid 242 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) → (𝐹‘𝑘) ∈ dom 𝐼)) |
| 54 | 53 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐹‘𝑘) ∈ dom 𝐼) |
| 55 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝐵 = (𝐹‘𝑘) → (𝐵 ∈ dom 𝐼 ↔ (𝐹‘𝑘) ∈ dom 𝐼)) |
| 56 | 54, 55 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (𝐵 = (𝐹‘𝑘) → 𝐵 ∈ dom 𝐼)) |
| 57 | 56 | con3d 152 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → (¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = (𝐹‘𝑘))) |
| 58 | 57 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) → (¬ 𝐵 ∈ dom 𝐼 → ¬ 𝐵 = (𝐹‘𝑘)))) |
| 59 | 7, 58 | mpid 44 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ (0..^𝑁) → ¬ 𝐵 = (𝐹‘𝑘))) |
| 60 | 59 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ¬ 𝐵 = (𝐹‘𝑘)) |
| 61 | 60 | neqned 2947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → 𝐵 ≠ (𝐹‘𝑘)) |
| 62 | | fvunsn 7199 |
. . . . . . 7
⊢ (𝐵 ≠ (𝐹‘𝑘) → ((𝐼 ∪ {〈𝐵, 𝐸〉})‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑘))) |
| 63 | 61, 62 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝐼 ∪ {〈𝐵, 𝐸〉})‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑘))) |
| 64 | 45, 63 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) |
| 65 | 64 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) |
| 66 | 24, 32, 65 | 3jca 1129 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) ∧ ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) → ((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) |
| 67 | 16, 66 | mpidan 689 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑁)) → ((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) |
| 68 | 67 | ralrimiva 3146 |
1
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) |