| Step | Hyp | Ref
| Expression |
| 1 | | wlkres.d |
. . . 4
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
| 2 | | wlkres.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
| 3 | 2 | wlkf 29632 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 4 | | pfxwrdsymb 14727 |
. . . 4
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 prefix 𝑁) ∈ Word (𝐹 “ (0..^𝑁))) |
| 5 | 1, 3, 4 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝐹 prefix 𝑁) ∈ Word (𝐹 “ (0..^𝑁))) |
| 6 | | wlkres.h |
. . . 4
⊢ 𝐻 = (𝐹 prefix 𝑁) |
| 7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐻 = (𝐹 prefix 𝑁)) |
| 8 | | wlkres.e |
. . . . . 6
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
| 9 | 8 | dmeqd 5916 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
| 10 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
| 11 | | wrdf 14557 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) |
| 12 | | fimass 6756 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼) |
| 13 | 10, 11, 12 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼) |
| 14 | | ssdmres 6031 |
. . . . . 6
⊢ ((𝐹 “ (0..^𝑁)) ⊆ dom 𝐼 ↔ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁))) |
| 15 | 13, 14 | sylib 218 |
. . . . 5
⊢ (𝜑 → dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁))) |
| 16 | 9, 15 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → dom (iEdg‘𝑆) = (𝐹 “ (0..^𝑁))) |
| 17 | | wrdeq 14574 |
. . . 4
⊢ (dom
(iEdg‘𝑆) = (𝐹 “ (0..^𝑁)) → Word dom (iEdg‘𝑆) = Word (𝐹 “ (0..^𝑁))) |
| 18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → Word dom (iEdg‘𝑆) = Word (𝐹 “ (0..^𝑁))) |
| 19 | 5, 7, 18 | 3eltr4d 2856 |
. 2
⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆)) |
| 20 | | wlkres.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 21 | 20 | wlkp 29634 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 22 | 1, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 23 | | wlkres.s |
. . . . . . 7
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
| 24 | 23 | feq3d 6723 |
. . . . . 6
⊢ (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉)) |
| 25 | 22, 24 | mpbird 257 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆)) |
| 26 | | fzossfz 13718 |
. . . . . . 7
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) |
| 27 | | wlkres.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) |
| 28 | 26, 27 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝐹))) |
| 29 | | elfzuz3 13561 |
. . . . . 6
⊢ (𝑁 ∈
(0...(♯‘𝐹))
→ (♯‘𝐹)
∈ (ℤ≥‘𝑁)) |
| 30 | | fzss2 13604 |
. . . . . 6
⊢
((♯‘𝐹)
∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹))) |
| 31 | 28, 29, 30 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹))) |
| 32 | 25, 31 | fssresd 6775 |
. . . 4
⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)) |
| 33 | 6 | fveq2i 6909 |
. . . . . . 7
⊢
(♯‘𝐻) =
(♯‘(𝐹 prefix
𝑁)) |
| 34 | | pfxlen 14721 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = 𝑁) |
| 35 | 10, 28, 34 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐹 prefix 𝑁)) = 𝑁) |
| 36 | 33, 35 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐻) = 𝑁) |
| 37 | 36 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁)) |
| 38 | 37 | feq2d 6722 |
. . . 4
⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))) |
| 39 | 32, 38 | mpbird 257 |
. . 3
⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
| 40 | | wlkres.q |
. . . 4
⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) |
| 41 | 40 | feq1i 6727 |
. . 3
⊢ (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
| 42 | 39, 41 | sylibr 234 |
. 2
⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
| 43 | 20, 2 | wlkprop 29629 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
| 44 | 1, 43 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
| 45 | 44 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
| 46 | 36 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁)) |
| 47 | 46 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁))) |
| 48 | 40 | fveq1i 6907 |
. . . . . . . . . . . . 13
⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥) |
| 49 | | fzossfz 13718 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝑁) ⊆
(0...𝑁) |
| 50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁)) |
| 51 | 50 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁)) |
| 52 | 51 | fvresd 6926 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥)) |
| 53 | 48, 52 | eqtr2id 2790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥)) |
| 54 | 40 | fveq1i 6907 |
. . . . . . . . . . . . 13
⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) |
| 55 | | fzofzp1 13803 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁)) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁)) |
| 57 | 56 | fvresd 6926 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1))) |
| 58 | 54, 57 | eqtr2id 2790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) |
| 59 | 53, 58 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))) |
| 60 | 59 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))) |
| 61 | 47, 60 | sylbid 240 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))) |
| 62 | 61 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))) |
| 63 | 10 | ancli 548 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼)) |
| 64 | 11 | ffund 6740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹) |
| 67 | | fdm 6745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹))) |
| 68 | | elfzouz2 13714 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(0..^(♯‘𝐹))
→ (♯‘𝐹)
∈ (ℤ≥‘𝑁)) |
| 69 | | fzoss2 13727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹)
∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹))) |
| 70 | 27, 68, 69 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹))) |
| 71 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
𝐹 =
(0..^(♯‘𝐹))
→ ((0..^𝑁) ⊆ dom
𝐹 ↔ (0..^𝑁) ⊆
(0..^(♯‘𝐹)))) |
| 72 | 70, 71 | imbitrrid 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 =
(0..^(♯‘𝐹))
→ (𝜑 → (0..^𝑁) ⊆ dom 𝐹)) |
| 73 | 11, 67, 72 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹)) |
| 74 | 73 | impcom 407 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹) |
| 76 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁)) |
| 77 | 66, 75, 76 | resfvresima 7255 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
| 78 | 63, 77 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
| 79 | 78 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
| 80 | 79 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))) |
| 81 | 47, 80 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))) |
| 82 | 81 | imp 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
| 83 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
| 84 | 6 | fveq1i 6907 |
. . . . . . . . . . 11
⊢ (𝐻‘𝑥) = ((𝐹 prefix 𝑁)‘𝑥) |
| 85 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝐹 ∈ Word dom 𝐼) |
| 86 | 28 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝑁 ∈ (0...(♯‘𝐹))) |
| 87 | | pfxres 14717 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) |
| 88 | 85, 86, 87 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) |
| 89 | 88 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((𝐹 prefix 𝑁)‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)) |
| 90 | 84, 89 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)) |
| 91 | 83, 90 | fveq12d 6913 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
| 92 | 82, 91 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) |
| 93 | 62, 92 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
| 94 | 27, 68 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐹) ∈
(ℤ≥‘𝑁)) |
| 95 | 36 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘(♯‘𝐻)) = (ℤ≥‘𝑁)) |
| 96 | 94, 95 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐹) ∈
(ℤ≥‘(♯‘𝐻))) |
| 97 | | fzoss2 13727 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ (ℤ≥‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆
(0..^(♯‘𝐹))) |
| 98 | 96, 97 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(♯‘𝐻)) ⊆
(0..^(♯‘𝐹))) |
| 99 | 98 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹))) |
| 100 | | wkslem1 29625 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))))) |
| 101 | 100 | rspcv 3618 |
. . . . . . . 8
⊢ (𝑥 ∈
(0..^(♯‘𝐹))
→ (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))))) |
| 102 | 99, 101 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))))) |
| 103 | | eqeq12 2754 |
. . . . . . . . . 10
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1)))) |
| 104 | 103 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1)))) |
| 105 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) |
| 106 | | sneq 4636 |
. . . . . . . . . . . 12
⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
| 107 | 106 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
| 108 | 107 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
| 109 | 105, 108 | eqeq12d 2753 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)})) |
| 110 | | preq12 4735 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))}) |
| 111 | 110 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))}) |
| 112 | 111, 105 | sseq12d 4017 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
| 113 | 104, 109,
112 | ifpbi123d 1079 |
. . . . . . . 8
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) ↔ if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
| 114 | 113 | biimpd 229 |
. . . . . . 7
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
| 115 | 93, 102, 114 | sylsyld 61 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
| 116 | 115 | com12 32 |
. . . . 5
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
| 117 | 116 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
| 118 | 45, 117 | mpcom 38 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
| 119 | 118 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
| 120 | 20, 2, 1, 27, 23 | wlkreslem 29687 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
| 121 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 122 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
| 123 | 121, 122 | iswlkg 29631 |
. . 3
⊢ (𝑆 ∈ V → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))) |
| 124 | 120, 123 | syl 17 |
. 2
⊢ (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))) |
| 125 | 19, 42, 119, 124 | mpbir3and 1343 |
1
⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) |