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

Theorem clwwlkinwwlkOLD 27430
 Description: Obsolete version of clwwlkinwwlk 27429 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 23-Jan-2022.) (Proof shortened by AV, 23-Mar-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
clwwlkinwwlkOLD (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))

Proof of Theorem clwwlkinwwlkOLD
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 eqid 2777 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2777 . . 3 (Edg‘𝐺) = (Edg‘𝐺)
31, 2wwlknp 27192 . 2 (𝑊 ∈ (𝑀 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
4 swrdcl 13735 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
54adantr 474 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
65adantr 474 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
7 simpll 757 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑊 ∈ Word (Vtx‘𝐺))
8 simprl 761 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℕ)
9 eluz2 11998 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀))
10 zre 11732 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
11 zre 11732 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
12 id 22 . . . . . . . . . . . . . . . . 17 (𝑁𝑀𝑁𝑀)
1310, 11, 123anim123i 1151 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
149, 13sylbi 209 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ𝑁) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
15 letrp1 11219 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀) → 𝑁 ≤ (𝑀 + 1))
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ𝑁) → 𝑁 ≤ (𝑀 + 1))
1716adantl 475 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ≤ (𝑀 + 1))
1817adantl 475 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (𝑀 + 1))
19 breq2 4890 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2019ad2antlr 717 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2118, 20mpbird 249 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (♯‘𝑊))
22 swrdn0OLD 13747 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅)
237, 8, 21, 22syl3anc 1439 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅)
246, 23jca 507 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
25243adantl3 1170 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
2625adantr 474 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
27 nnz 11751 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
28 1nn0 11660 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
29 eluzmn 11999 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 1 ∈ ℕ0) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
3027, 28, 29sylancl 580 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
31 uzss 12013 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3332sselda 3820 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ‘(𝑁 − 1)))
34 fzoss2 12815 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
3533, 34syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
36353ad2ant3 1126 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
37 ssralv 3884 . . . . . . . . . . . . 13 ((0..^(𝑁 − 1)) ⊆ (0..^𝑀) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
3836, 37syl 17 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
39383exp 1109 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
4039com34 91 . . . . . . . . . 10 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
41403imp1 1409 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
4241adantr 474 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
43 nnnn0 11650 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
44 elnn0uz 12031 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
4543, 44sylib 210 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
46 eluzfz 12654 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘0) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
4745, 46sylan 575 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
48 fzelp1 12710 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (0...𝑀) → 𝑁 ∈ (0...(𝑀 + 1)))
4947, 48syl 17 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...(𝑀 + 1)))
5049adantl 475 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
51 oveq2 6930 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑊) = (𝑀 + 1) → (0...(♯‘𝑊)) = (0...(𝑀 + 1)))
5251eleq2d 2844 . . . . . . . . . . . . . . . . 17 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5352ad2antlr 717 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5450, 53mpbird 249 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
55 swrd0lenOLD 13738 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
567, 54, 55syl2anc 579 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
5756oveq1d 6937 . . . . . . . . . . . . 13 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1) = (𝑁 − 1))
5857oveq2d 6938 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
5958raleqdv 3339 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
607adantr 474 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑊 ∈ Word (Vtx‘𝐺))
6154adantr 474 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑊)))
6230ad2antrl 718 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
63 fzoss2 12815 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6564sselda 3820 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 swrd0fvOLD 13758 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑊𝑖))
6760, 61, 65, 66syl3anc 1439 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑊𝑖))
6827ad2antrl 718 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℤ)
69 elfzom1elp1fzo 12854 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7068, 69sylan 575 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71 swrd0fvOLD 13758 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7260, 61, 70, 71syl3anc 1439 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7367, 72preq12d 4507 . . . . . . . . . . . . 13 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} = {(𝑊𝑖), (𝑊‘(𝑖 + 1))})
7473eleq1d 2843 . . . . . . . . . . . 12 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7574ralbidva 3166 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7659, 75bitrd 271 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77763adantl3 1170 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877adantr 474 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7942, 78mpbird 249 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
80 elfz1uz 12728 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...𝑀))
81 fzelp1 12710 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...𝑀) → 𝑁 ∈ (1...(𝑀 + 1)))
8280, 81syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...(𝑀 + 1)))
8382adantl 475 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(𝑀 + 1)))
84 oveq2 6930 . . . . . . . . . . . . . 14 ((♯‘𝑊) = (𝑀 + 1) → (1...(♯‘𝑊)) = (1...(𝑀 + 1)))
8584eleq2d 2844 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8685ad2antlr 717 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8783, 86mpbird 249 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(♯‘𝑊)))
88 swrd0fvlswOLD 13762 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 substr ⟨0, 𝑁⟩)) = (𝑊‘(𝑁 − 1)))
89 swrd0fv0OLD 13759 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 substr ⟨0, 𝑁⟩)‘0) = (𝑊‘0))
9088, 89preq12d 4507 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
917, 87, 90syl2anc 579 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
92913adantl3 1170 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
9392adantr 474 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
94 fz1fzo0m1 12835 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1...𝑀) → (𝑁 − 1) ∈ (0..^𝑀))
9580, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑁 − 1) ∈ (0..^𝑀))
96953ad2ant3 1126 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 − 1) ∈ (0..^𝑀))
97 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → 𝑖 = (𝑁 − 1))
9897fveq2d 6450 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊𝑖) = (𝑊‘(𝑁 − 1)))
99 oveq1 6929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
100 nncn 11383 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
101 npcan1 10800 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
10399, 102sylan9eqr 2835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑖 + 1) = 𝑁)
104103fveq2d 6450 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊𝑁))
10598, 104preq12d 4507 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊𝑁)})
106105eleq1d 2843 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
107106ex 403 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
108107adantr 474 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
1091083ad2ant3 1126 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
110109imp 397 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
11196, 110rspcdv 3513 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
1121113exp 1109 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
113112com34 91 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
1141133imp1 1409 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
115114adantr 474 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
116 preq2 4500 . . . . . . . . . . 11 ((𝑊𝑁) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
117116eleq1d 2843 . . . . . . . . . 10 ((𝑊𝑁) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
118117adantl 475 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
119115, 118mpbid 224 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))
12093, 119eqeltrd 2858 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
12126, 79, 1203jca 1119 . . . . . 6 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
122121exp31 412 . . . . 5 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → ((𝑊𝑁) = (𝑊‘0) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))))
1231223imp21 1102 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
1241, 2isclwwlk 27364 . . . 4 ((𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
125123, 124sylibr 226 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺))
12647adantl 475 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...𝑀))
127126, 48syl 17 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
128127, 53mpbird 249 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
1297, 128jca 507 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
130129ex 403 . . . . . . 7 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
1311303adant3 1123 . . . . . 6 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
132131impcom 398 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1331323adant3 1123 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
134133, 55syl 17 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
135 isclwwlkn 27416 . . 3 ((𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁))
136125, 134, 135sylanbrc 578 . 2 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
1373, 136syl3an2 1164 1 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2106   ≠ wne 2968  ∀wral 3089   ⊆ wss 3791  ∅c0 4140  {cpr 4399  ⟨cop 4403   class class class wbr 4886  ‘cfv 6135  (class class class)co 6922  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273   + caddc 10275   ≤ cle 10412   − cmin 10606  ℕcn 11374  ℕ0cn0 11642  ℤcz 11728  ℤ≥cuz 11992  ...cfz 12643  ..^cfzo 12784  ♯chash 13435  Word cword 13599  lastSclsw 13652   substr csubstr 13730  Vtxcvtx 26344  Edgcedg 26395   WWalksN cwwlksn 27175  ClWWalkscclwwlk 27361   ClWWalksN cclwwlkn 27413 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-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-lsw 13653  df-substr 13731  df-wwlks 27179  df-wwlksn 27180  df-clwwlk 27362  df-clwwlkn 27414 This theorem is referenced by:  clwwnrepclwwnOLD  27754
 Copyright terms: Public domain W3C validator