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

Theorem wlkres 26561
 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 27068. (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 26504 . . . . . . . 8 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
5 wrdfn 13314 . . . . . . . 8 (𝐹 ∈ Word dom 𝐼𝐹 Fn (0..^(#‘𝐹)))
62, 4, 53syl 18 . . . . . . 7 (𝜑𝐹 Fn (0..^(#‘𝐹)))
7 wlkres.n . . . . . . . 8 (𝜑𝑁 ∈ (0..^(#‘𝐹)))
8 elfzouz2 12480 . . . . . . . 8 (𝑁 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈ (ℤ𝑁))
9 fzoss2 12492 . . . . . . . 8 ((#‘𝐹) ∈ (ℤ𝑁) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
107, 8, 93syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
11 fnssres 6002 . . . . . . 7 ((𝐹 Fn (0..^(#‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(#‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
126, 10, 11syl2anc 693 . . . . . 6 (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14 fveq2 6189 . . . . . . . . . . . . . 14 (𝑖 = 𝑥 → (𝐹𝑖) = (𝐹𝑥))
1514eqeq1d 2623 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
1615adantl 482 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
17 fvres 6205 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1817adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1918eqcomd 2627 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
2013, 16, 19rspcedvd 3315 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
216adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(#‘𝐹)))
2210adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
2321, 22fvelimabd 6252 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
2420, 23mpbird 247 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
252, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ Word dom 𝐼)
26 wrdf 13305 . . . . . . . . . . . . . 14 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
27 ffvelrn 6355 . . . . . . . . . . . . . . . . 17 ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼𝑥 ∈ (0..^(#‘𝐹))) → (𝐹𝑥) ∈ dom 𝐼)
2827expcom 451 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(#‘𝐹)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝐹𝑥) ∈ dom 𝐼))
2910sselda 3601 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(#‘𝐹)))
3028, 29syl11 33 . . . . . . . . . . . . . . 15 (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼))
3130expd 452 . . . . . . . . . . . . . 14 (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3226, 31syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3325, 32mpcom 38 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼))
3433imp 445 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼)
3518, 34eqeltrd 2700 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
3624, 35elind 3796 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
37 dmres 5417 . . . . . . . . 9 dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
3836, 37syl6eleqr 2711 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
39 wlkres.e . . . . . . . . . . 11 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
4039dmeqd 5324 . . . . . . . . . 10 (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
4140eleq2d 2686 . . . . . . . . 9 (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4241adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4338, 42mpbird 247 . . . . . . 7 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
4443ralrimiva 2965 . . . . . 6 (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
45 ffnfv 6386 . . . . . 6 ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
4612, 44, 45sylanbrc 698 . . . . 5 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
47 fzossfz 12484 . . . . . . . . 9 (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
4847, 7sseldi 3599 . . . . . . . 8 (𝜑𝑁 ∈ (0...(#‘𝐹)))
49 wlkreslem0 26559 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 ∈ (0...(#‘𝐹))) → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
5025, 48, 49syl2anc 693 . . . . . . 7 (𝜑 → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
5150oveq2d 6663 . . . . . 6 (𝜑 → (0..^(#‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
5251feq2d 6029 . . . . 5 (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
5346, 52mpbird 247 . . . 4 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
54 iswrdb 13306 . . . 4 ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
5553, 54sylibr 224 . . 3 (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
561, 55syl5eqel 2704 . 2 (𝜑𝐻 ∈ Word dom (iEdg‘𝑆))
57 wlkres.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
5857wlkp 26506 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
592, 58syl 17 . . . . . 6 (𝜑𝑃:(0...(#‘𝐹))⟶𝑉)
60 wlkres.s . . . . . . 7 (𝜑 → (Vtx‘𝑆) = 𝑉)
6160feq3d 6030 . . . . . 6 (𝜑 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(#‘𝐹))⟶𝑉))
6259, 61mpbird 247 . . . . 5 (𝜑𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆))
63 elfzuz3 12336 . . . . . 6 (𝑁 ∈ (0...(#‘𝐹)) → (#‘𝐹) ∈ (ℤ𝑁))
64 fzss2 12378 . . . . . 6 ((#‘𝐹) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...(#‘𝐹)))
6548, 63, 643syl 18 . . . . 5 (𝜑 → (0...𝑁) ⊆ (0...(#‘𝐹)))
6662, 65fssresd 6069 . . . 4 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
671fveq2i 6192 . . . . . . 7 (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁)))
6867, 50syl5eq 2667 . . . . . 6 (𝜑 → (#‘𝐻) = 𝑁)
6968oveq2d 6663 . . . . 5 (𝜑 → (0...(#‘𝐻)) = (0...𝑁))
7069feq2d 6029 . . . 4 (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
7166, 70mpbird 247 . . 3 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
72 wlkres.q . . . 4 𝑄 = (𝑃 ↾ (0...𝑁))
7372feq1i 6034 . . 3 (𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
7471, 73sylibr 224 . 2 (𝜑𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆))
75 wlkv 26502 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
7657, 3iswlk 26500 . . . . . . . 8 ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))))
7776biimpd 219 . . . . . . 7 ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))))
7875, 77mpcom 38 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
792, 78syl 17 . . . . 5 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
8079adantr 481 . . . 4 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
8168oveq2d 6663 . . . . . . . . . . 11 (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁))
8281eleq2d 2686 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
8372fveq1i 6190 . . . . . . . . . . . . 13 (𝑄𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
84 fzossfz 12484 . . . . . . . . . . . . . . . 16 (0..^𝑁) ⊆ (0...𝑁)
8584a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
8685sselda 3601 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
8786fvresd 6206 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃𝑥))
8883, 87syl5req 2668 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃𝑥) = (𝑄𝑥))
8972fveq1i 6190 . . . . . . . . . . . . 13 (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
90 fzofzp1 12561 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
9190adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
9291fvresd 6206 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
9389, 92syl5req 2668 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
9488, 93jca 554 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9594ex 450 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9682, 95sylbid 230 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9796imp 445 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9825ancli 574 . . . . . . . . . . . . . 14 (𝜑 → (𝜑𝐹 ∈ Word dom 𝐼))
9926ffund 6047 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
10099adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
101100adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
102 fdm 6049 . . . . . . . . . . . . . . . . . 18 (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(#‘𝐹)))
103 sseq2 3625 . . . . . . . . . . . . . . . . . . 19 (dom 𝐹 = (0..^(#‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(#‘𝐹))))
10410, 103syl5ibr 236 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 = (0..^(#‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
10526, 102, 1043syl 18 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
106105impcom 446 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
107106adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
108 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
109101, 107, 108resfvresima 6491 . . . . . . . . . . . . . 14 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
11098, 109sylan 488 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
111110eqcomd 2627 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
112111ex 450 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
11382, 112sylbid 230 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
114113imp 445 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
11539adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
1161fveq1i 6190 . . . . . . . . . . 11 (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
117116a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
118115, 117fveq12d 6195 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → ((iEdg‘𝑆)‘(𝐻𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
119114, 118eqtr4d 2658 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
12097, 119jca 554 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))))
1217, 8syl 17 . . . . . . . . . . 11 (𝜑 → (#‘𝐹) ∈ (ℤ𝑁))
1221a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝐹 ↾ (0..^𝑁)))
123122fveq2d 6193 . . . . . . . . . . . . 13 (𝜑 → (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁))))
124123, 50eqtrd 2655 . . . . . . . . . . . 12 (𝜑 → (#‘𝐻) = 𝑁)
125124fveq2d 6193 . . . . . . . . . . 11 (𝜑 → (ℤ‘(#‘𝐻)) = (ℤ𝑁))
126121, 125eleqtrrd 2703 . . . . . . . . . 10 (𝜑 → (#‘𝐹) ∈ (ℤ‘(#‘𝐻)))
127 fzoss2 12492 . . . . . . . . . 10 ((#‘𝐹) ∈ (ℤ‘(#‘𝐻)) → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
128126, 127syl 17 . . . . . . . . 9 (𝜑 → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
129128sselda 3601 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → 𝑥 ∈ (0..^(#‘𝐹)))
130 wkslem1 26497 . . . . . . . . 9 (𝑘 = 𝑥 → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
131130rspcv 3303 . . . . . . . 8 (𝑥 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
132129, 131syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
133 eqeq12 2634 . . . . . . . . . 10 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
134133adantr 481 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
135 simpr 477 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
136 sneq 4185 . . . . . . . . . . . 12 ((𝑃𝑥) = (𝑄𝑥) → {(𝑃𝑥)} = {(𝑄𝑥)})
137136adantr 481 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥)} = {(𝑄𝑥)})
138137adantr 481 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥)} = {(𝑄𝑥)})
139135, 138eqeq12d 2636 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}))
140 preq12 4268 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
141140adantr 481 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
142141, 135sseq12d 3632 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)) ↔ {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
143134, 139, 142ifpbi123d 1027 . . . . . . . 8 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) ↔ if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
144143biimpd 219 . . . . . . 7 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
145120, 132, 144sylsyld 61 . . . . . 6 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
146145com12 32 . . . . 5 (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
1471463ad2ant3 1083 . . . 4 ((𝐹 ∈ Word dom 𝐼𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))) → ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
14880, 147mpcom 38 . . 3 ((𝜑𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
149148ralrimiva 2965 . 2 (𝜑 → ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
15057, 3, 2, 7, 60, 39, 1, 72wlkreslem 26560 . . 3 (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
151 eqid 2621 . . . 4 (Vtx‘𝑆) = (Vtx‘𝑆)
152 eqid 2621 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
153151, 152iswlk 26500 . . 3 ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
154150, 153syl 17 . 2 (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))))
15556, 74, 149, 154mpbir3and 1244 1 (𝜑𝐻(Walks‘𝑆)𝑄)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  if-wif 1012   ∧ w3a 1037   = wceq 1482   ∈ wcel 1989  ∀wral 2911  ∃wrex 2912  Vcvv 3198   ∩ cin 3571   ⊆ wss 3572  {csn 4175  {cpr 4177   class class class wbr 4651  dom cdm 5112   ↾ cres 5114   “ cima 5115  Fun wfun 5880   Fn wfn 5881  ⟶wf 5882  ‘cfv 5886  (class class class)co 6647  0cc0 9933  1c1 9934   + caddc 9936  ℤ≥cuz 11684  ...cfz 12323  ..^cfzo 12461  #chash 13112  Word cword 13286  Vtxcvtx 25868  iEdgciedg 25869  Walkscwlks 26486 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-card 8762  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-nn 11018  df-n0 11290  df-z 11375  df-uz 11685  df-fz 12324  df-fzo 12462  df-hash 13113  df-word 13294  df-substr 13298  df-wlks 26489 This theorem is referenced by:  trlres  26591  eupthres  27068
 Copyright terms: Public domain W3C validator