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

Theorem wlkres 26794
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 27387. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.)
Hypotheses
Ref Expression
wlkres.v 𝑉 = (Vtx‘𝐺)
wlkres.i 𝐼 = (iEdg‘𝐺)
wlkres.d (𝜑𝐹(Walks‘𝐺)𝑃)
wlkres.n (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
wlkres.s (𝜑 → (Vtx‘𝑆) = 𝑉)
wlkres.e (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
wlkres.h 𝐻 = (𝐹 ↾ (0..^𝑁))
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.h . . 3 𝐻 = (𝐹 ↾ (0..^𝑁))
2 wlkres.d . . . . . . . 8 (𝜑𝐹(Walks‘𝐺)𝑃)
3 wlkres.i . . . . . . . . 9 𝐼 = (iEdg‘𝐺)
43wlkf 26737 . . . . . . . 8 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
5 wrdfn 13526 . . . . . . . 8 (𝐹 ∈ Word dom 𝐼𝐹 Fn (0..^(♯‘𝐹)))
62, 4, 53syl 18 . . . . . . 7 (𝜑𝐹 Fn (0..^(♯‘𝐹)))
7 wlkres.n . . . . . . . 8 (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
8 elfzouz2 12704 . . . . . . . 8 (𝑁 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
9 fzoss2 12716 . . . . . . . 8 ((♯‘𝐹) ∈ (ℤ𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
107, 8, 93syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
11 fnssres 6211 . . . . . . 7 ((𝐹 Fn (0..^(♯‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
126, 10, 11syl2anc 575 . . . . . 6 (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13 simpr 473 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14 fveqeq2 6413 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
1514adantl 469 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16 fvres 6423 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1716adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1817eqcomd 2812 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
1913, 15, 18rspcedvd 3509 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
206adantr 468 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(♯‘𝐹)))
2110adantr 468 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
2220, 21fvelimabd 6471 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
2319, 22mpbird 248 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
242, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ Word dom 𝐼)
25 wrdf 13517 . . . . . . . . . . . . . 14 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
26 ffvelrn 6575 . . . . . . . . . . . . . . . . 17 ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐼𝑥 ∈ (0..^(♯‘𝐹))) → (𝐹𝑥) ∈ dom 𝐼)
2726expcom 400 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(♯‘𝐹)) → (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹𝑥) ∈ dom 𝐼))
2810sselda 3798 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝐹)))
2927, 28syl11 33 . . . . . . . . . . . . . . 15 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼))
3029expd 402 . . . . . . . . . . . . . 14 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3125, 30syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3224, 31mpcom 38 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼))
3332imp 395 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼)
3417, 33eqeltrd 2885 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
3523, 34elind 3997 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
36 dmres 5622 . . . . . . . . 9 dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
3735, 36syl6eleqr 2896 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
38 wlkres.e . . . . . . . . . . 11 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
3938dmeqd 5527 . . . . . . . . . 10 (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
4039eleq2d 2871 . . . . . . . . 9 (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4140adantr 468 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4237, 41mpbird 248 . . . . . . 7 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
4342ralrimiva 3154 . . . . . 6 (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
44 ffnfv 6606 . . . . . 6 ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
4512, 43, 44sylanbrc 574 . . . . 5 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
46 fzossfz 12708 . . . . . . . . 9 (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
4746, 7sseldi 3796 . . . . . . . 8 (𝜑𝑁 ∈ (0...(♯‘𝐹)))
48 wlkreslem0 26792 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
4924, 47, 48syl2anc 575 . . . . . . 7 (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
5049oveq2d 6886 . . . . . 6 (𝜑 → (0..^(♯‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
5150feq2d 6238 . . . . 5 (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
5245, 51mpbird 248 . . . 4 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
53 iswrdb 13518 . . . 4 ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
5452, 53sylibr 225 . . 3 (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
551, 54syl5eqel 2889 . 2 (𝜑𝐻 ∈ Word dom (iEdg‘𝑆))
56 wlkres.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
5756wlkp 26739 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
582, 57syl 17 . . . . . 6 (𝜑𝑃:(0...(♯‘𝐹))⟶𝑉)
59 wlkres.s . . . . . . 7 (𝜑 → (Vtx‘𝑆) = 𝑉)
6059feq3d 6239 . . . . . 6 (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
6158, 60mpbird 248 . . . . 5 (𝜑𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆))
62 elfzuz3 12558 . . . . . 6 (𝑁 ∈ (0...(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
63 fzss2 12600 . . . . . 6 ((♯‘𝐹) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹)))
6447, 62, 633syl 18 . . . . 5 (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹)))
6561, 64fssresd 6282 . . . 4 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
661fveq2i 6407 . . . . . . 7 (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁)))
6766, 49syl5eq 2852 . . . . . 6 (𝜑 → (♯‘𝐻) = 𝑁)
6867oveq2d 6886 . . . . 5 (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
6968feq2d 6238 . . . 4 (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
7065, 69mpbird 248 . . 3 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
71 wlkres.q . . . 4 𝑄 = (𝑃 ↾ (0...𝑁))
7271feq1i 6243 . . 3 (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
7370, 72sylibr 225 . 2 (𝜑𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆))
74 wlkv 26735 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
7556, 3iswlk 26733 . . . . . . . 8 ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))))
7675biimpd 220 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))))
7774, 76mpcom 38 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
782, 77syl 17 . . . . 5 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
7978adantr 468 . . . 4 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
8067oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
8180eleq2d 2871 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
8271fveq1i 6405 . . . . . . . . . . . . 13 (𝑄𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
83 fzossfz 12708 . . . . . . . . . . . . . . . 16 (0..^𝑁) ⊆ (0...𝑁)
8483a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
8584sselda 3798 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
8685fvresd 6424 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃𝑥))
8782, 86syl5req 2853 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃𝑥) = (𝑄𝑥))
8871fveq1i 6405 . . . . . . . . . . . . 13 (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
89 fzofzp1 12785 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
9089adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
9190fvresd 6424 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
9288, 91syl5req 2853 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
9387, 92jca 503 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9493ex 399 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9581, 94sylbid 231 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9695imp 395 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9724ancli 540 . . . . . . . . . . . . . 14 (𝜑 → (𝜑𝐹 ∈ Word dom 𝐼))
9825ffund 6256 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
9998adantl 469 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
10099adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
101 fdm 6260 . . . . . . . . . . . . . . . . . 18 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹)))
102 sseq2 3824 . . . . . . . . . . . . . . . . . . 19 (dom 𝐹 = (0..^(♯‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(♯‘𝐹))))
10310, 102syl5ibr 237 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 = (0..^(♯‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
10425, 101, 1033syl 18 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
105104impcom 396 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
106105adantr 468 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
107 simpr 473 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
108100, 106, 107resfvresima 6715 . . . . . . . . . . . . . 14 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
10997, 108sylan 571 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
110109eqcomd 2812 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
111110ex 399 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
11281, 111sylbid 231 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
113112imp 395 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
11438adantr 468 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
1151fveq1i 6405 . . . . . . . . . . 11 (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
116115a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
117114, 116fveq12d 6411 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
118113, 117eqtr4d 2843 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
11996, 118jca 503 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))))
1207, 8syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘𝐹) ∈ (ℤ𝑁))
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝐹 ↾ (0..^𝑁)))
122121fveq2d 6408 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁))))
123122, 49eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐻) = 𝑁)
124123fveq2d 6408 . . . . . . . . . . 11 (𝜑 → (ℤ‘(♯‘𝐻)) = (ℤ𝑁))
125120, 124eleqtrrd 2888 . . . . . . . . . 10 (𝜑 → (♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)))
126 fzoss2 12716 . . . . . . . . . 10 ((♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
127125, 126syl 17 . . . . . . . . 9 (𝜑 → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
128127sselda 3798 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹)))
129 wkslem1 26730 . . . . . . . . 9 (𝑘 = 𝑥 → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
130129rspcv 3498 . . . . . . . 8 (𝑥 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
131128, 130syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
132 eqeq12 2819 . . . . . . . . . 10 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
133132adantr 468 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
134 simpr 473 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
135 sneq 4380 . . . . . . . . . . . 12 ((𝑃𝑥) = (𝑄𝑥) → {(𝑃𝑥)} = {(𝑄𝑥)})
136135adantr 468 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥)} = {(𝑄𝑥)})
137136adantr 468 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥)} = {(𝑄𝑥)})
138134, 137eqeq12d 2821 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}))
139 preq12 4461 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
140139adantr 468 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
141140, 134sseq12d 3831 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)) ↔ {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
142133, 138, 141ifpbi123d 1093 . . . . . . . 8 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) ↔ if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
143142biimpd 220 . . . . . . 7 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
144119, 131, 143sylsyld 61 . . . . . 6 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
145144com12 32 . . . . 5 (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
1461453ad2ant3 1158 . . . 4 ((𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))) → ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
14779, 146mpcom 38 . . 3 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
148147ralrimiva 3154 . 2 (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
14956, 3, 2, 7, 59, 38, 1, 71wlkreslem 26793 . . 3 (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
150 eqid 2806 . . . 4 (Vtx‘𝑆) = (Vtx‘𝑆)
151 eqid 2806 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
152150, 151iswlk 26733 . . 3 ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
153149, 152syl 17 . 2 (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
15455, 73, 148, 153mpbir3and 1435 1 (𝜑𝐻(Walks‘𝑆)𝑄)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  if-wif 1078  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  Vcvv 3391  cin 3768  wss 3769  {csn 4370  {cpr 4372   class class class wbr 4844  dom cdm 5311  cres 5313  cima 5314  Fun wfun 6091   Fn wfn 6092  wf 6093  cfv 6097  (class class class)co 6870  0cc0 10217  1c1 10218   + caddc 10220  cuz 11900  ...cfz 12545  ..^cfzo 12685  chash 13333  Word cword 13498  Vtxcvtx 26087  iEdgciedg 26088  Walkscwlks 26719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-ifp 1079  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-map 8090  df-pm 8091  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-n0 11556  df-z 11640  df-uz 11901  df-fz 12546  df-fzo 12686  df-hash 13334  df-word 13506  df-substr 13510  df-wlks 26722
This theorem is referenced by:  trlres  26824  eupthres  27387
  Copyright terms: Public domain W3C validator