Step | Hyp | Ref
| Expression |
1 | | wlkres.d |
. . . 4
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
2 | | wlkres.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 2 | wlkf 27981 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
4 | | pfxwrdsymb 14402 |
. . . 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 5814 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
10 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
11 | | wrdf 14222 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) |
12 | | fimass 6621 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼) |
14 | | ssdmres 5914 |
. . . . . 6
⊢ ((𝐹 “ (0..^𝑁)) ⊆ dom 𝐼 ↔ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁))) |
15 | 13, 14 | sylib 217 |
. . . . 5
⊢ (𝜑 → dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁))) |
16 | 9, 15 | eqtrd 2778 |
. . . 4
⊢ (𝜑 → dom (iEdg‘𝑆) = (𝐹 “ (0..^𝑁))) |
17 | | wrdeq 14239 |
. . . 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 2854 |
. 2
⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆)) |
20 | | wlkres.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
21 | 20 | wlkp 27983 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
22 | 1, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
23 | | wlkres.s |
. . . . . . 7
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
24 | 23 | feq3d 6587 |
. . . . . 6
⊢ (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉)) |
25 | 22, 24 | mpbird 256 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆)) |
26 | | fzossfz 13406 |
. . . . . . 7
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) |
27 | | wlkres.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) |
28 | 26, 27 | sselid 3919 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝐹))) |
29 | | elfzuz3 13253 |
. . . . . 6
⊢ (𝑁 ∈
(0...(♯‘𝐹))
→ (♯‘𝐹)
∈ (ℤ≥‘𝑁)) |
30 | | fzss2 13296 |
. . . . . 6
⊢
((♯‘𝐹)
∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹))) |
31 | 28, 29, 30 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹))) |
32 | 25, 31 | fssresd 6641 |
. . . 4
⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)) |
33 | 6 | fveq2i 6777 |
. . . . . . 7
⊢
(♯‘𝐻) =
(♯‘(𝐹 prefix
𝑁)) |
34 | | pfxlen 14396 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = 𝑁) |
35 | 10, 28, 34 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐹 prefix 𝑁)) = 𝑁) |
36 | 33, 35 | eqtrid 2790 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐻) = 𝑁) |
37 | 36 | oveq2d 7291 |
. . . . 5
⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁)) |
38 | 37 | feq2d 6586 |
. . . 4
⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))) |
39 | 32, 38 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
40 | | wlkres.q |
. . . 4
⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) |
41 | 40 | feq1i 6591 |
. . 3
⊢ (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
42 | 39, 41 | sylibr 233 |
. 2
⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
43 | 20, 2 | wlkprop 27978 |
. . . . . 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 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
46 | 36 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁)) |
47 | 46 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁))) |
48 | 40 | fveq1i 6775 |
. . . . . . . . . . . . 13
⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥) |
49 | | fzossfz 13406 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝑁) ⊆
(0...𝑁) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁)) |
51 | 50 | sselda 3921 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁)) |
52 | 51 | fvresd 6794 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥)) |
53 | 48, 52 | eqtr2id 2791 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥)) |
54 | 40 | fveq1i 6775 |
. . . . . . . . . . . . 13
⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) |
55 | | fzofzp1 13484 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁)) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁)) |
57 | 56 | fvresd 6794 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1))) |
58 | 54, 57 | eqtr2id 2791 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) |
59 | 53, 58 | jca 512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))) |
60 | 59 | ex 413 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))) |
61 | 47, 60 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))) |
62 | 61 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))) |
63 | 10 | ancli 549 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼)) |
64 | 11 | ffund 6604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹) |
67 | | fdm 6609 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹))) |
68 | | elfzouz2 13402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(0..^(♯‘𝐹))
→ (♯‘𝐹)
∈ (ℤ≥‘𝑁)) |
69 | | fzoss2 13415 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹)
∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹))) |
70 | 27, 68, 69 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹))) |
71 | | sseq2 3947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
𝐹 =
(0..^(♯‘𝐹))
→ ((0..^𝑁) ⊆ dom
𝐹 ↔ (0..^𝑁) ⊆
(0..^(♯‘𝐹)))) |
72 | 70, 71 | syl5ibr 245 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 =
(0..^(♯‘𝐹))
→ (𝜑 → (0..^𝑁) ⊆ dom 𝐹)) |
73 | 11, 67, 72 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹)) |
74 | 73 | impcom 408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹) |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹) |
76 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁)) |
77 | 66, 75, 76 | resfvresima 7111 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
78 | 63, 77 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
79 | 78 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
80 | 79 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))) |
81 | 47, 80 | sylbid 239 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))) |
82 | 81 | imp 407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
83 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) |
84 | 6 | fveq1i 6775 |
. . . . . . . . . . 11
⊢ (𝐻‘𝑥) = ((𝐹 prefix 𝑁)‘𝑥) |
85 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝐹 ∈ Word dom 𝐼) |
86 | 28 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝑁 ∈ (0...(♯‘𝐹))) |
87 | | pfxres 14392 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) |
88 | 85, 86, 87 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) |
89 | 88 | fveq1d 6776 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((𝐹 prefix 𝑁)‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)) |
90 | 84, 89 | eqtrid 2790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)) |
91 | 83, 90 | fveq12d 6781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))) |
92 | 82, 91 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) |
93 | 62, 92 | jca 512 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
94 | 27, 68 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐹) ∈
(ℤ≥‘𝑁)) |
95 | 36 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘(♯‘𝐻)) = (ℤ≥‘𝑁)) |
96 | 94, 95 | eleqtrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐹) ∈
(ℤ≥‘(♯‘𝐻))) |
97 | | fzoss2 13415 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ (ℤ≥‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆
(0..^(♯‘𝐹))) |
98 | 96, 97 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(♯‘𝐻)) ⊆
(0..^(♯‘𝐹))) |
99 | 98 | sselda 3921 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹))) |
100 | | wkslem1 27974 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))))) |
101 | 100 | rspcv 3557 |
. . . . . . . 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 2755 |
. . . . . . . . . 10
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1)))) |
104 | 103 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1)))) |
105 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) |
106 | | sneq 4571 |
. . . . . . . . . . . 12
⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
107 | 106 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
108 | 107 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)}) |
109 | 105, 108 | eqeq12d 2754 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)})) |
110 | | preq12 4671 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))}) |
111 | 110 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))}) |
112 | 111, 105 | sseq12d 3954 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
113 | 104, 109,
112 | ifpbi123d 1077 |
. . . . . . . 8
⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) ↔ if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))) |
114 | 113 | biimpd 228 |
. . . . . . 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 1134 |
. . . 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 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))) |
120 | 20, 2, 1, 27, 23 | wlkreslem 28037 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
121 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
122 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
123 | 121, 122 | iswlkg 27980 |
. . 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 1341 |
1
⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) |