MPE Home 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