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

Theorem wlkresOLD 27021
 Description: Obsolete version of wlkres 27019 as of 30-Nov-2022. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
wlkresOLD.v 𝑉 = (Vtx‘𝐺)
wlkresOLD.i 𝐼 = (iEdg‘𝐺)
wlkresOLD.d (𝜑𝐹(Walks‘𝐺)𝑃)
wlkresOLD.n (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
wlkresOLD.s (𝜑 → (Vtx‘𝑆) = 𝑉)
wlkresOLD.e (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
wlkresOLD.h 𝐻 = (𝐹 ↾ (0..^𝑁))
wlkresOLD.q 𝑄 = (𝑃 ↾ (0...𝑁))
Assertion
Ref Expression
wlkresOLD (𝜑𝐻(Walks‘𝑆)𝑄)

Proof of Theorem wlkresOLD
Dummy variables 𝑘 𝑖 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wlkresOLD.h . . 3 𝐻 = (𝐹 ↾ (0..^𝑁))
2 wlkresOLD.d . . . . . . . 8 (𝜑𝐹(Walks‘𝐺)𝑃)
3 wlkresOLD.i . . . . . . . . 9 𝐼 = (iEdg‘𝐺)
43wlkf 26962 . . . . . . . 8 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
5 wrdfn 13614 . . . . . . . 8 (𝐹 ∈ Word dom 𝐼𝐹 Fn (0..^(♯‘𝐹)))
62, 4, 53syl 18 . . . . . . 7 (𝜑𝐹 Fn (0..^(♯‘𝐹)))
7 wlkresOLD.n . . . . . . . 8 (𝜑𝑁 ∈ (0..^(♯‘𝐹)))
8 elfzouz2 12803 . . . . . . . 8 (𝑁 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
9 fzoss2 12815 . . . . . . . 8 ((♯‘𝐹) ∈ (ℤ𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
107, 8, 93syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
11 fnssres 6250 . . . . . . 7 ((𝐹 Fn (0..^(♯‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
126, 10, 11syl2anc 579 . . . . . 6 (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13 simpr 479 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14 fveqeq2 6455 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
1514adantl 475 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16 fvres 6465 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1716adantl 475 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹𝑥))
1817eqcomd 2783 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
1913, 15, 18rspcedvd 3517 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
206adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(♯‘𝐹)))
2110adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
2220, 21fvelimabd 6514 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
2319, 22mpbird 249 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
242, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ Word dom 𝐼)
25 wrdf 13604 . . . . . . . . . . . . . 14 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
26 ffvelrn 6621 . . . . . . . . . . . . . . . . 17 ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐼𝑥 ∈ (0..^(♯‘𝐹))) → (𝐹𝑥) ∈ dom 𝐼)
2726expcom 404 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(♯‘𝐹)) → (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹𝑥) ∈ dom 𝐼))
2810sselda 3820 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝐹)))
2927, 28syl11 33 . . . . . . . . . . . . . . 15 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼))
3029expd 406 . . . . . . . . . . . . . 14 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3125, 30syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼)))
3224, 31mpcom 38 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹𝑥) ∈ dom 𝐼))
3332imp 397 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐹𝑥) ∈ dom 𝐼)
3417, 33eqeltrd 2858 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
3523, 34elind 4020 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
36 dmres 5668 . . . . . . . . 9 dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
3735, 36syl6eleqr 2869 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
38 wlkresOLD.e . . . . . . . . . . 11 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
3938dmeqd 5571 . . . . . . . . . 10 (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
4039eleq2d 2844 . . . . . . . . 9 (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4140adantr 474 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
4237, 41mpbird 249 . . . . . . 7 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
4342ralrimiva 3147 . . . . . 6 (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
44 ffnfv 6652 . . . . . 6 ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
4512, 43, 44sylanbrc 578 . . . . 5 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
46 fzossfz 12807 . . . . . . . . 9 (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
4746, 7sseldi 3818 . . . . . . . 8 (𝜑𝑁 ∈ (0...(♯‘𝐹)))
48 wlkreslem0OLD 27016 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
4924, 47, 48syl2anc 579 . . . . . . 7 (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
5049oveq2d 6938 . . . . . 6 (𝜑 → (0..^(♯‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
5150feq2d 6277 . . . . 5 (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
5245, 51mpbird 249 . . . 4 (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
53 iswrdb 13605 . . . 4 ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
5452, 53sylibr 226 . . 3 (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
551, 54syl5eqel 2862 . 2 (𝜑𝐻 ∈ Word dom (iEdg‘𝑆))
56 wlkresOLD.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
5756wlkp 26964 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
582, 57syl 17 . . . . . 6 (𝜑𝑃:(0...(♯‘𝐹))⟶𝑉)
59 wlkresOLD.s . . . . . . 7 (𝜑 → (Vtx‘𝑆) = 𝑉)
6059feq3d 6278 . . . . . 6 (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
6158, 60mpbird 249 . . . . 5 (𝜑𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆))
62 elfzuz3 12656 . . . . . 6 (𝑁 ∈ (0...(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ𝑁))
63 fzss2 12698 . . . . . 6 ((♯‘𝐹) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹)))
6447, 62, 633syl 18 . . . . 5 (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹)))
6561, 64fssresd 6321 . . . 4 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
661fveq2i 6449 . . . . . . 7 (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁)))
6766, 49syl5eq 2825 . . . . . 6 (𝜑 → (♯‘𝐻) = 𝑁)
6867oveq2d 6938 . . . . 5 (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
6968feq2d 6277 . . . 4 (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
7065, 69mpbird 249 . . 3 (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
71 wlkresOLD.q . . . 4 𝑄 = (𝑃 ↾ (0...𝑁))
7271feq1i 6282 . . 3 (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
7370, 72sylibr 226 . 2 (𝜑𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆))
74 wlkv 26960 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
7556, 3iswlk 26958 . . . . . . . 8 ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))))
7675biimpd 221 . . . . . . 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 474 . . . 4 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))))
8067oveq2d 6938 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
8180eleq2d 2844 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
8271fveq1i 6447 . . . . . . . . . . . . 13 (𝑄𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
83 fzossfz 12807 . . . . . . . . . . . . . . . 16 (0..^𝑁) ⊆ (0...𝑁)
8483a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
8584sselda 3820 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
8685fvresd 6466 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃𝑥))
8782, 86syl5req 2826 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃𝑥) = (𝑄𝑥))
8871fveq1i 6447 . . . . . . . . . . . . 13 (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
89 fzofzp1 12884 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
9089adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
9190fvresd 6466 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
9288, 91syl5req 2826 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
9387, 92jca 507 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9493ex 403 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9581, 94sylbid 232 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
9695imp 397 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
9724ancli 544 . . . . . . . . . . . . . 14 (𝜑 → (𝜑𝐹 ∈ Word dom 𝐼))
9825ffund 6295 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
9998adantl 475 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
10099adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
101 fdm 6299 . . . . . . . . . . . . . . . . . 18 (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹)))
102 sseq2 3845 . . . . . . . . . . . . . . . . . . 19 (dom 𝐹 = (0..^(♯‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(♯‘𝐹))))
10310, 102syl5ibr 238 . . . . . . . . . . . . . . . . . 18 (dom 𝐹 = (0..^(♯‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
10425, 101, 1033syl 18 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
105104impcom 398 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
106105adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
107 simpr 479 . . . . . . . . . . . . . . 15 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
108100, 106, 107resfvresima 6767 . . . . . . . . . . . . . 14 (((𝜑𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
10997, 108sylan 575 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹𝑥)))
110109eqcomd 2783 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
111110ex 403 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
11281, 111sylbid 232 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
113112imp 397 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
11438adantr 474 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
1151fveq1i 6447 . . . . . . . . . . 11 (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
116115a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
117114, 116fveq12d 6453 . . . . . . . . 9 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
118113, 117eqtr4d 2816 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
11996, 118jca 507 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))))
1207, 8syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘𝐹) ∈ (ℤ𝑁))
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐻 = (𝐹 ↾ (0..^𝑁)))
122121fveq2d 6450 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁))))
123122, 49eqtrd 2813 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐻) = 𝑁)
124123fveq2d 6450 . . . . . . . . . . 11 (𝜑 → (ℤ‘(♯‘𝐻)) = (ℤ𝑁))
125120, 124eleqtrrd 2861 . . . . . . . . . 10 (𝜑 → (♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)))
126 fzoss2 12815 . . . . . . . . . 10 ((♯‘𝐹) ∈ (ℤ‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
127125, 126syl 17 . . . . . . . . 9 (𝜑 → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
128127sselda 3820 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹)))
129 wkslem1 26955 . . . . . . . . 9 (𝑘 = 𝑥 → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
130129rspcv 3506 . . . . . . . 8 (𝑥 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
131128, 130syl 17 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) → if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)))))
132 eqeq12 2790 . . . . . . . . . 10 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
133132adantr 474 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝑃𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄𝑥) = (𝑄‘(𝑥 + 1))))
134 simpr 479 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥)))
135 sneq 4407 . . . . . . . . . . . 12 ((𝑃𝑥) = (𝑄𝑥) → {(𝑃𝑥)} = {(𝑄𝑥)})
136135adantr 474 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥)} = {(𝑄𝑥)})
137136adantr 474 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥)} = {(𝑄𝑥)})
138134, 137eqeq12d 2792 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}))
139 preq12 4501 . . . . . . . . . . 11 (((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
140139adantr 474 . . . . . . . . . 10 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄𝑥), (𝑄‘(𝑥 + 1))})
141140, 134sseq12d 3852 . . . . . . . . 9 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥)) ↔ {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
142133, 138, 141ifpbi123d 1061 . . . . . . . 8 ((((𝑃𝑥) = (𝑄𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹𝑥)) = ((iEdg‘𝑆)‘(𝐻𝑥))) → (if-((𝑃𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹𝑥)) = {(𝑃𝑥)}, {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹𝑥))) ↔ if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥)))))
143142biimpd 221 . . . . . . 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 1126 . . . 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 3147 . 2 (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻𝑥)) = {(𝑄𝑥)}, {(𝑄𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻𝑥))))
14956, 3, 2, 7, 59, 38, 1, 71wlkreslemOLD 27020 . . 3 (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
150 eqid 2777 . . . 4 (Vtx‘𝑆) = (Vtx‘𝑆)
151 eqid 2777 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
152150, 151iswlk 26958 . . 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 1399 1 (𝜑𝐻(Walks‘𝑆)𝑄)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  if-wif 1046   ∧ w3a 1071   = wceq 1601   ∈ wcel 2106  ∀wral 3089  ∃wrex 3090  Vcvv 3397   ∩ cin 3790   ⊆ wss 3791  {csn 4397  {cpr 4399   class class class wbr 4886  dom cdm 5355   ↾ cres 5357   “ cima 5358  Fun wfun 6129   Fn wfn 6130  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275  ℤ≥cuz 11992  ...cfz 12643  ..^cfzo 12784  ♯chash 13435  Word cword 13599  Vtxcvtx 26344  iEdgciedg 26345  Walkscwlks 26944 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ifp 1047  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-n0 11643  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-hash 13436  df-word 13600  df-substr 13731  df-pfx 13780  df-wlks 26947 This theorem is referenced by:  trlresOLD  27053  eupthresOLD  27632
 Copyright terms: Public domain W3C validator