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

Theorem clwwlkinwwlk 27825
Description: If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 23-Jan-2022.) (Revised by AV, 30-Oct-2022.)
Assertion
Ref Expression
clwwlkinwwlk (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))

Proof of Theorem clwwlkinwwlk
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 eqid 2798 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2798 . . 3 (Edg‘𝐺) = (Edg‘𝐺)
31, 2wwlknp 27629 . 2 (𝑊 ∈ (𝑀 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
4 pfxcl 14030 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
54adantr 484 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
65adantr 484 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
7 simpll 766 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑊 ∈ Word (Vtx‘𝐺))
8 simprl 770 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℕ)
9 eluz2 12237 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀))
10 zre 11973 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
11 zre 11973 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
12 id 22 . . . . . . . . . . . . . . . . 17 (𝑁𝑀𝑁𝑀)
1310, 11, 123anim123i 1148 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
149, 13sylbi 220 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ𝑁) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
15 letrp1 11473 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀) → 𝑁 ≤ (𝑀 + 1))
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ𝑁) → 𝑁 ≤ (𝑀 + 1))
1716adantl 485 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ≤ (𝑀 + 1))
1817adantl 485 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (𝑀 + 1))
19 breq2 5034 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2019ad2antlr 726 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2118, 20mpbird 260 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (♯‘𝑊))
22 pfxn0 14039 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 prefix 𝑁) ≠ ∅)
237, 8, 21, 22syl3anc 1368 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 prefix 𝑁) ≠ ∅)
246, 23jca 515 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
25243adantl3 1165 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
2625adantr 484 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
27 nnz 11992 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
28 1nn0 11901 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
29 eluzmn 12238 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 1 ∈ ℕ0) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
3027, 28, 29sylancl 589 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
31 uzss 12253 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3332sselda 3915 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ‘(𝑁 − 1)))
34 fzoss2 13060 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
3533, 34syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
36353ad2ant3 1132 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
37 ssralv 3981 . . . . . . . . . . . . 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 1116 . . . . . . . . . . 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 1344 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
4241adantr 484 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
43 nnnn0 11892 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
44 elnn0uz 12271 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
4543, 44sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
46 eluzfz 12897 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘0) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
4745, 46sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
48 fzelp1 12954 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (0...𝑀) → 𝑁 ∈ (0...(𝑀 + 1)))
4947, 48syl 17 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...(𝑀 + 1)))
5049adantl 485 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
51 oveq2 7143 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑊) = (𝑀 + 1) → (0...(♯‘𝑊)) = (0...(𝑀 + 1)))
5251eleq2d 2875 . . . . . . . . . . . . . . . . 17 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5352ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5450, 53mpbird 260 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
55 pfxlen 14036 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁)
567, 54, 55syl2anc 587 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁)
5756oveq1d 7150 . . . . . . . . . . . . 13 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((♯‘(𝑊 prefix 𝑁)) − 1) = (𝑁 − 1))
5857oveq2d 7151 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^((♯‘(𝑊 prefix 𝑁)) − 1)) = (0..^(𝑁 − 1)))
5958raleqdv 3364 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
607adantr 484 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑊 ∈ Word (Vtx‘𝐺))
6154adantr 484 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑊)))
6230ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
63 fzoss2 13060 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6564sselda 3915 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 pfxfv 14035 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊𝑖))
6760, 61, 65, 66syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊𝑖))
6827ad2antrl 727 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℤ)
69 elfzom1elp1fzo 13099 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7068, 69sylan 583 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71 pfxfv 14035 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7260, 61, 70, 71syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7367, 72preq12d 4637 . . . . . . . . . . . . 13 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} = {(𝑊𝑖), (𝑊‘(𝑖 + 1))})
7473eleq1d 2874 . . . . . . . . . . . 12 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7574ralbidva 3161 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7659, 75bitrd 282 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77763adantl3 1165 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877adantr 484 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7942, 78mpbird 260 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
80 elfz1uz 12972 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...𝑀))
81 fzelp1 12954 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...𝑀) → 𝑁 ∈ (1...(𝑀 + 1)))
8280, 81syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...(𝑀 + 1)))
8382adantl 485 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(𝑀 + 1)))
84 oveq2 7143 . . . . . . . . . . . . . 14 ((♯‘𝑊) = (𝑀 + 1) → (1...(♯‘𝑊)) = (1...(𝑀 + 1)))
8584eleq2d 2875 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8685ad2antlr 726 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8783, 86mpbird 260 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(♯‘𝑊)))
88 pfxfvlsw 14048 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 prefix 𝑁)) = (𝑊‘(𝑁 − 1)))
89 pfxfv0 14045 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝑁)‘0) = (𝑊‘0))
9088, 89preq12d 4637 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
917, 87, 90syl2anc 587 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
92913adantl3 1165 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
9392adantr 484 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
94 fz1fzo0m1 13080 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1...𝑀) → (𝑁 − 1) ∈ (0..^𝑀))
9580, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑁 − 1) ∈ (0..^𝑀))
96953ad2ant3 1132 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 − 1) ∈ (0..^𝑀))
97 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → 𝑖 = (𝑁 − 1))
9897fveq2d 6649 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊𝑖) = (𝑊‘(𝑁 − 1)))
99 oveq1 7142 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
100 nncn 11633 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
101 npcan1 11054 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
10399, 102sylan9eqr 2855 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑖 + 1) = 𝑁)
104103fveq2d 6649 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊𝑁))
10598, 104preq12d 4637 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊𝑁)})
106105eleq1d 2874 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
107106ex 416 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
108107adantr 484 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
1091083ad2ant3 1132 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
110109imp 410 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
11196, 110rspcdv 3563 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
1121113exp 1116 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
113112com34 91 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
1141133imp1 1344 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
115114adantr 484 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
116 preq2 4630 . . . . . . . . . . 11 ((𝑊𝑁) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
117116eleq1d 2874 . . . . . . . . . 10 ((𝑊𝑁) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
118117adantl 485 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
119115, 118mpbid 235 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))
12093, 119eqeltrd 2890 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))
12126, 79, 1203jca 1125 . . . . . 6 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))
122121exp31 423 . . . . 5 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → ((𝑊𝑁) = (𝑊‘0) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))))
1231223imp21 1111 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))
1241, 2isclwwlk 27769 . . . 4 ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))
125123, 124sylibr 237 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺))
12647adantl 485 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...𝑀))
127126, 48syl 17 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
128127, 53mpbird 260 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
1297, 128jca 515 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
130129ex 416 . . . . . . 7 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
1311303adant3 1129 . . . . . 6 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
132131impcom 411 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1331323adant3 1129 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
134133, 55syl 17 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (♯‘(𝑊 prefix 𝑁)) = 𝑁)
135 isclwwlkn 27812 . . 3 ((𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝑊 prefix 𝑁)) = 𝑁))
136125, 134, 135sylanbrc 586 . 2 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
1373, 136syl3an2 1161 1 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2111  wne 2987  wral 3106  wss 3881  c0 4243  {cpr 4527   class class class wbr 5030  cfv 6324  (class class class)co 7135  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529  cle 10665  cmin 10859  cn 11625  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  ..^cfzo 13028  chash 13686  Word cword 13857  lastSclsw 13905   prefix cpfx 14023  Vtxcvtx 26789  Edgcedg 26840   WWalksN cwwlksn 27612  ClWWalkscclwwlk 27766   ClWWalksN cclwwlkn 27809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-hash 13687  df-word 13858  df-lsw 13906  df-substr 13994  df-pfx 14024  df-wwlks 27616  df-wwlksn 27617  df-clwwlk 27767  df-clwwlkn 27810
This theorem is referenced by:  clwwnrepclwwn  28129
  Copyright terms: Public domain W3C validator