MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wlkres Structured version   Visualization version   GIF version

Theorem wlkres 27444
Description: The restriction 𝐻, 𝑄 of a walk 𝐹, 𝑃 to an initial segment of the walk (of length 𝑁) forms a walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 27986. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
Hypotheses
Ref Expression
wlkres.v 𝑉 = (Vtx‘𝐺)
wlkres.i 𝐼 = (iEdg‘𝐺)
wlkres.d (𝜑𝐹(Walks‘𝐺)𝑃)
wlkres.n (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
wlkres.s (𝜑 → (Vtx‘𝑆) = 𝑉)
wlkres.e (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
wlkres.h 𝐻 = (𝐹 prefix 𝑁)
wlkres.q 𝑄 = (𝑃 ↾ (0...𝑁))
Assertion
Ref Expression
wlkres (𝜑𝐻(Walks‘𝑆)𝑄)

Proof of Theorem wlkres
Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wlkres.d . . . 4 (𝜑𝐹(Walks‘𝐺)𝑃)
2 wlkres.i . . . . 5 𝐼 = (iEdg‘𝐺)
32wlkf 27388 . . . 4 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
4 pfxwrdsymb 14043 . . . 4 (𝐹 ∈ Word dom 𝐼 → (𝐹 prefix 𝑁) ∈ Word (𝐹 “ (0..^𝑁)))
51, 3, 43syl 18 . . 3 (𝜑 → (𝐹 prefix 𝑁) ∈ Word (𝐹 “ (0..^𝑁)))
6 wlkres.h . . . 4 𝐻 = (𝐹 prefix 𝑁)
76a1i 11 . . 3 (𝜑𝐻 = (𝐹 prefix 𝑁))
8 wlkres.e . . . . . 6 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
98dmeqd 5767 . . . . 5 (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
101, 3syl 17 . . . . . . 7 (𝜑𝐹 ∈ Word dom 𝐼)
11 wrdf 13858 . . . . . . 7 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
12 fimass 6548 . . . . . . 7 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼)
1310, 11, 123syl 18 . . . . . 6 (𝜑 → (𝐹 “ (0..^𝑁)) ⊆ dom 𝐼)
14 ssdmres 5869 . . . . . 6 ((𝐹 “ (0..^𝑁)) ⊆ dom 𝐼 ↔ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁)))
1513, 14sylib 220 . . . . 5 (𝜑 → dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = (𝐹 “ (0..^𝑁)))
169, 15eqtrd 2854 . . . 4 (𝜑 → dom (iEdg‘𝑆) = (𝐹 “ (0..^𝑁)))
17 wrdeq 13878 . . . 4 (dom (iEdg‘𝑆) = (𝐹 “ (0..^𝑁)) → Word dom (iEdg‘𝑆) = Word (𝐹 “ (0..^𝑁)))
1816, 17syl 17 . . 3 (𝜑 → Word dom (iEdg‘𝑆) = Word (𝐹 “ (0..^𝑁)))
195, 7, 183eltr4d 2926 . 2 (𝜑𝐻 ∈ Word dom (iEdg‘𝑆))
20 wlkres.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
2120wlkp 27390 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
221, 21syl 17 . . . . . 6 (𝜑𝑃:(0...(♯‘𝐹))⟶𝑉)
23 wlkres.s . . . . . . 7 (𝜑 → (Vtx‘𝑆) = 𝑉)
2423feq3d 6494 . . . . . 6 (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
2522, 24mpbird 259 . . . . 5 (𝜑𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆))
26 fzossfz 13048 . . . . . . 7 (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
27 wlkres.n . . . . . . 7 (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
2826, 27sseldi 3963 . . . . . 6 (𝜑𝑁 ∈ (0...(♯‘𝐹)))
29 elfzuz3 12897 . . . . . 6 (𝑁 ∈ (0...(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
30 fzss2 12939 . . . . . 6 ((♯‘𝐹) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹)))
3128, 29, 303syl 18 . . . . 5 (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹)))
3225, 31fssresd 6538 . . . 4 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
336fveq2i 6666 . . . . . . 7 (♯‘𝐻) = (♯‘(𝐹 prefix 𝑁))
34 pfxlen 14037 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = 𝑁)
3510, 28, 34syl2anc 586 . . . . . . 7 (𝜑 → (♯‘(𝐹 prefix 𝑁)) = 𝑁)
3633, 35syl5eq 2866 . . . . . 6 (𝜑 → (♯‘𝐻) = 𝑁)
3736oveq2d 7164 . . . . 5 (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
3837feq2d 6493 . . . 4 (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
3932, 38mpbird 259 . . 3 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
40 wlkres.q . . . 4 𝑄 = (𝑃 ↾ (0...𝑁))
4140feq1i 6498 . . 3 (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
4239, 41sylibr 236 . 2 (𝜑𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆))
4320, 2wlkprop 27385 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
441, 43syl 17 . . . . 5 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
4544adantr 483 . . . 4 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
4636oveq2d 7164 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
4746eleq2d 2896 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
4840fveq1i 6664 . . . . . . . . . . . . 13 (𝑄𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
49 fzossfz 13048 . . . . . . . . . . . . . . . 16 (0..^𝑁) ⊆ (0...𝑁)
5049a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
5150sselda 3965 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
5251fvresd 6683 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃𝑥))
5348, 52syl5req 2867 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃𝑥) = (𝑄𝑥))
5440fveq1i 6664 . . . . . . . . . . . . 13 (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
55 fzofzp1 13126 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
5655adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
5756fvresd 6683 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
5854, 57syl5req 2867 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
5953, 58jca 514 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
6059ex 415 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
6147, 60sylbid 242 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
6261imp 409 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
6310ancli 551 . . . . . . . . . . . . . 14 (𝜑 → (𝜑𝐹 ∈ Word dom 𝐼))
6411ffund 6511 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
6564adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
6665adantr 483 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
67 fdm 6515 . . . . . . . . . . . . . . . . . 18 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹)))
68 elfzouz2 13044 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
69 fzoss2 13057 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐹) ∈ (ℤ𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
7027, 68, 693syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
71 sseq2 3991 . . . . . . . . . . . . . . . . . . 19 (dom 𝐹 = (0..^(♯‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(♯‘𝐹))))
7270, 71syl5ibr 248 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 = (0..^(♯‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
7311, 67, 723syl 18 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
7473impcom 410 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
7574adantr 483 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
76 simpr 487 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
7766, 75, 76resfvresima 6989 . . . . . . . . . . . . . 14 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
7863, 77sylan 582 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
7978eqcomd 2825 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
8079ex 415 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
8147, 80sylbid 242 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
8281imp 409 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
838adantr 483 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
846fveq1i 6664 . . . . . . . . . . 11 (𝐻𝑥) = ((𝐹 prefix 𝑁)‘𝑥)
8510adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → 𝐹 ∈ Word dom 𝐼)
8628adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → 𝑁 ∈ (0...(♯‘𝐹)))
87 pfxres 14033 . . . . . . . . . . . . 13 ((𝐹 ∈ Word dom 𝐼𝑁 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁)))
8885, 86, 87syl2anc 586 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁)))
8988fveq1d 6665 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((𝐹 prefix 𝑁)‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
9084, 89syl5eq 2866 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
9183, 90fveq12d 6670 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
9282, 91eqtr4d 2857 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
9362, 92jca 514 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))))
9427, 68syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘𝐹) ∈ (ℤ𝑁))
9536fveq2d 6667 . . . . . . . . . . 11 (𝜑 → (ℤ‘(♯‘𝐻)) = (ℤ𝑁))
9694, 95eleqtrrd 2914 . . . . . . . . . 10 (𝜑 → (♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)))
97 fzoss2 13057 . . . . . . . . . 10 ((♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
9896, 97syl 17 . . . . . . . . 9 (𝜑 → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
9998sselda 3965 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹)))
100 wkslem1 27381 . . . . . . . . 9 (𝑘 = 𝑥 → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
101100rspcv 3616 . . . . . . . 8 (𝑥 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
10299, 101syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
103 eqeq12 2833 . . . . . . . . . 10 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
104103adantr 483 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
105 simpr 487 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
106 sneq 4569 . . . . . . . . . . . 12 ((𝑃𝑥) = (𝑄𝑥) → {(𝑃𝑥)} = {(𝑄𝑥)})
107106adantr 483 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥)} = {(𝑄𝑥)})
108107adantr 483 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥)} = {(𝑄𝑥)})
109105, 108eqeq12d 2835 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}))
110 preq12 4663 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
111110adantr 483 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
112111, 105sseq12d 3998 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)) ↔ {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
113104, 109, 112ifpbi123d 1071 . . . . . . . 8 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) ↔ if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
114113biimpd 231 . . . . . . 7 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
11593, 102, 114sylsyld 61 . . . . . 6 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
116115com12 32 . . . . 5 (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
1171163ad2ant3 1129 . . . 4 ((𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))) → ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
11845, 117mpcom 38 . . 3 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
119118ralrimiva 3180 . 2 (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
12020, 2, 1, 27, 23wlkreslem 27443 . . 3 (𝜑𝑆 ∈ V)
121 eqid 2819 . . . 4 (Vtx‘𝑆) = (Vtx‘𝑆)
122 eqid 2819 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
123121, 122iswlkg 27387 . . 3 (𝑆 ∈ V → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
124120, 123syl 17 . 2 (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
12519, 42, 119, 124mpbir3and 1336 1 (𝜑𝐻(Walks‘𝑆)𝑄)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  if-wif 1056  w3a 1081   = wceq 1530  wcel 2107  wral 3136  Vcvv 3493  wss 3934  {csn 4559  {cpr 4561   class class class wbr 5057  dom cdm 5548  cres 5550  cima 5551  Fun wfun 6342  wf 6344  cfv 6348  (class class class)co 7148  0cc0 10529  1c1 10530   + caddc 10532  cuz 12235  ...cfz 12884  ..^cfzo 13025  chash 13682  Word cword 13853   prefix cpfx 14024  Vtxcvtx 26773  iEdgciedg 26774  Walkscwlks 27370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1057  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12885  df-fzo 13026  df-hash 13683  df-word 13854  df-substr 13995  df-pfx 14025  df-wlks 27373
This theorem is referenced by:  trlres  27474  eupthres  27986
  Copyright terms: Public domain W3C validator