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

Theorem clwwlkinwwlk 30069
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 2735 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2735 . . 3 (Edg‘𝐺) = (Edg‘𝐺)
31, 2wwlknp 29873 . 2 (𝑊 ∈ (𝑀 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
4 pfxcl 14712 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
54adantr 480 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
65adantr 480 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺))
7 simpll 767 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑊 ∈ Word (Vtx‘𝐺))
8 simprl 771 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℕ)
9 eluz2 12882 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀))
10 zre 12615 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
11 zre 12615 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
12 id 22 . . . . . . . . . . . . . . . . 17 (𝑁𝑀𝑁𝑀)
1310, 11, 123anim123i 1150 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
149, 13sylbi 217 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ𝑁) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
15 letrp1 12109 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀) → 𝑁 ≤ (𝑀 + 1))
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ𝑁) → 𝑁 ≤ (𝑀 + 1))
1716adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ≤ (𝑀 + 1))
1817adantl 481 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (𝑀 + 1))
19 breq2 5152 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2019ad2antlr 727 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2118, 20mpbird 257 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (♯‘𝑊))
22 pfxn0 14721 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 prefix 𝑁) ≠ ∅)
237, 8, 21, 22syl3anc 1370 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 prefix 𝑁) ≠ ∅)
246, 23jca 511 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
25243adantl3 1167 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
2625adantr 480 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅))
27 nnz 12632 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
28 1nn0 12540 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
29 eluzmn 12883 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 1 ∈ ℕ0) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
3027, 28, 29sylancl 586 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
31 uzss 12899 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3332sselda 3995 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ‘(𝑁 − 1)))
34 fzoss2 13724 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
3533, 34syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
36353ad2ant3 1134 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
37 ssralv 4064 . . . . . . . . . . . . 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 1118 . . . . . . . . . . 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 1346 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
4241adantr 480 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
43 nnnn0 12531 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
44 elnn0uz 12921 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
4543, 44sylib 218 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
46 eluzfz 13556 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘0) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
4745, 46sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
48 fzelp1 13613 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (0...𝑀) → 𝑁 ∈ (0...(𝑀 + 1)))
4947, 48syl 17 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...(𝑀 + 1)))
5049adantl 481 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
51 oveq2 7439 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑊) = (𝑀 + 1) → (0...(♯‘𝑊)) = (0...(𝑀 + 1)))
5251eleq2d 2825 . . . . . . . . . . . . . . . . 17 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5352ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5450, 53mpbird 257 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
55 pfxlen 14718 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁)
567, 54, 55syl2anc 584 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (♯‘(𝑊 prefix 𝑁)) = 𝑁)
5756oveq1d 7446 . . . . . . . . . . . . 13 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((♯‘(𝑊 prefix 𝑁)) − 1) = (𝑁 − 1))
5857oveq2d 7447 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^((♯‘(𝑊 prefix 𝑁)) − 1)) = (0..^(𝑁 − 1)))
5958raleqdv 3324 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
607adantr 480 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑊 ∈ Word (Vtx‘𝐺))
6154adantr 480 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑊)))
6230ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
63 fzoss2 13724 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6564sselda 3995 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 pfxfv 14717 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊𝑖))
6760, 61, 65, 66syl3anc 1370 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘𝑖) = (𝑊𝑖))
6827ad2antrl 728 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℤ)
69 elfzom1elp1fzo 13768 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7068, 69sylan 580 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71 pfxfv 14717 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7260, 61, 70, 71syl3anc 1370 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 prefix 𝑁)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7367, 72preq12d 4746 . . . . . . . . . . . . 13 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} = {(𝑊𝑖), (𝑊‘(𝑖 + 1))})
7473eleq1d 2824 . . . . . . . . . . . 12 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7574ralbidva 3174 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7659, 75bitrd 279 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77763adantl3 1167 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877adantr 480 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7942, 78mpbird 257 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
80 elfz1uz 13631 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...𝑀))
81 fzelp1 13613 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...𝑀) → 𝑁 ∈ (1...(𝑀 + 1)))
8280, 81syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...(𝑀 + 1)))
8382adantl 481 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(𝑀 + 1)))
84 oveq2 7439 . . . . . . . . . . . . . 14 ((♯‘𝑊) = (𝑀 + 1) → (1...(♯‘𝑊)) = (1...(𝑀 + 1)))
8584eleq2d 2825 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8685ad2antlr 727 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8783, 86mpbird 257 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(♯‘𝑊)))
88 pfxfvlsw 14730 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 prefix 𝑁)) = (𝑊‘(𝑁 − 1)))
89 pfxfv0 14727 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 prefix 𝑁)‘0) = (𝑊‘0))
9088, 89preq12d 4746 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
917, 87, 90syl2anc 584 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
92913adantl3 1167 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
9392adantr 480 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
94 fz1fzo0m1 13747 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1...𝑀) → (𝑁 − 1) ∈ (0..^𝑀))
9580, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑁 − 1) ∈ (0..^𝑀))
96953ad2ant3 1134 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 − 1) ∈ (0..^𝑀))
97 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → 𝑖 = (𝑁 − 1))
9897fveq2d 6911 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊𝑖) = (𝑊‘(𝑁 − 1)))
99 oveq1 7438 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
100 nncn 12272 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
101 npcan1 11686 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
10399, 102sylan9eqr 2797 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑖 + 1) = 𝑁)
104103fveq2d 6911 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊𝑁))
10598, 104preq12d 4746 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊𝑁)})
106105eleq1d 2824 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
107106ex 412 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
108107adantr 480 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
1091083ad2ant3 1134 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
110109imp 406 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
11196, 110rspcdv 3614 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
1121113exp 1118 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
113112com34 91 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
1141133imp1 1346 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
115114adantr 480 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
116 preq2 4739 . . . . . . . . . . 11 ((𝑊𝑁) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
117116eleq1d 2824 . . . . . . . . . 10 ((𝑊𝑁) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
118117adantl 481 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
119115, 118mpbid 232 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))
12093, 119eqeltrd 2839 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺))
12126, 79, 1203jca 1127 . . . . . 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 419 . . . . 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 1113 . . . 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 30013 . . . 4 ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 prefix 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 prefix 𝑁) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix 𝑁)) − 1)){((𝑊 prefix 𝑁)‘𝑖), ((𝑊 prefix 𝑁)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 prefix 𝑁)), ((𝑊 prefix 𝑁)‘0)} ∈ (Edg‘𝐺)))
125123, 124sylibr 234 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺))
12647adantl 481 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...𝑀))
127126, 48syl 17 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
128127, 53mpbird 257 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
1297, 128jca 511 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
130129ex 412 . . . . . . 7 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
1311303adant3 1131 . . . . . 6 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
132131impcom 407 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1331323adant3 1131 . . . 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 30056 . . 3 ((𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 prefix 𝑁) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝑊 prefix 𝑁)) = 𝑁))
136125, 134, 135sylanbrc 583 . 2 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
1373, 136syl3an2 1163 1 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  wss 3963  c0 4339  {cpr 4633   class class class wbr 5148  cfv 6563  (class class class)co 7431  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156  cle 11294  cmin 11490  cn 12264  0cn0 12524  cz 12611  cuz 12876  ...cfz 13544  ..^cfzo 13691  chash 14366  Word cword 14549  lastSclsw 14597   prefix cpfx 14705  Vtxcvtx 29028  Edgcedg 29079   WWalksN cwwlksn 29856  ClWWalkscclwwlk 30010   ClWWalksN cclwwlkn 30053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545  df-fzo 13692  df-hash 14367  df-word 14550  df-lsw 14598  df-substr 14676  df-pfx 14706  df-wwlks 29860  df-wwlksn 29861  df-clwwlk 30011  df-clwwlkn 30054
This theorem is referenced by:  clwwnrepclwwn  30373
  Copyright terms: Public domain W3C validator