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

Theorem clwwlknonwwlknonb 27649
 Description: A word over vertices represents a closed walk of a fixed length 𝑁 on vertex 𝑋 iff the word concatenated with 𝑋 represents a walk of length 𝑁 on 𝑋 and 𝑋. This theorem would not hold for 𝑁 = 0 and 𝑊 = ∅, see clwwlknwwlksnb 27593. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.)
Hypothesis
Ref Expression
clwwlknonwwlknonb.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
clwwlknonwwlknonb ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋)))

Proof of Theorem clwwlknonwwlknonb
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 s1eq 13761 . . . . . . . . . 10 ((𝑊‘0) = 𝑋 → ⟨“(𝑊‘0)”⟩ = ⟨“𝑋”⟩)
21oveq2d 6990 . . . . . . . . 9 ((𝑊‘0) = 𝑋 → (𝑊 ++ ⟨“(𝑊‘0)”⟩) = (𝑊 ++ ⟨“𝑋”⟩))
32eleq1d 2843 . . . . . . . 8 ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺)))
43biimpac 471 . . . . . . 7 (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺))
54adantl 474 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺))
6 fvexd 6511 . . . . . . . . . . . 12 ((𝑊‘0) = 𝑋 → (𝑊‘0) ∈ V)
7 eleq1 2846 . . . . . . . . . . . 12 ((𝑊‘0) = 𝑋 → ((𝑊‘0) ∈ V ↔ 𝑋 ∈ V))
86, 7mpbid 224 . . . . . . . . . . 11 ((𝑊‘0) = 𝑋𝑋 ∈ V)
9 clwwlknonwwlknonb.v . . . . . . . . . . . . . . 15 𝑉 = (Vtx‘𝐺)
10 eqid 2771 . . . . . . . . . . . . . . 15 (Edg‘𝐺) = (Edg‘𝐺)
119, 10wwlknp 27344 . . . . . . . . . . . . . 14 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑋”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑋”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
12 simprrl 769 . . . . . . . . . . . . . . . . 17 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → 𝑊 ∈ Word 𝑉)
13 simpl 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → 𝑊 ∈ Word 𝑉)
1413anim2i 608 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (𝑋 ∈ V ∧ 𝑊 ∈ Word 𝑉))
1514ancomd 454 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (𝑊 ∈ Word 𝑉𝑋 ∈ V))
16 ccats1alpha 13780 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ∈ Word 𝑉𝑋 ∈ V) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉𝑋𝑉)))
1715, 16syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉𝑋𝑉)))
18 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉𝑋𝑉) → 𝑋𝑉)
1917, 18syl6bi 245 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉𝑋𝑉))
2019com12 32 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → 𝑋𝑉))
2120adantr 473 . . . . . . . . . . . . . . . . . 18 (((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → 𝑋𝑉))
2221imp 398 . . . . . . . . . . . . . . . . 17 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → 𝑋𝑉)
23 nnnn0 11713 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
24 ccatws1lenp1b 13782 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ↔ (♯‘𝑊) = 𝑁))
2523, 24sylan2 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ↔ (♯‘𝑊) = 𝑁))
2625biimpd 221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) → (♯‘𝑊) = 𝑁))
2726adantl 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) → (♯‘𝑊) = 𝑁))
2827com12 32 . . . . . . . . . . . . . . . . . . . 20 ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (♯‘𝑊) = 𝑁))
2928adantl 474 . . . . . . . . . . . . . . . . . . 19 (((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (♯‘𝑊) = 𝑁))
3029imp 398 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (♯‘𝑊) = 𝑁)
3130eqcomd 2777 . . . . . . . . . . . . . . . . 17 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → 𝑁 = (♯‘𝑊))
3212, 22, 313jca 1109 . . . . . . . . . . . . . . . 16 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))
3332ex 405 . . . . . . . . . . . . . . 15 (((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1)) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊))))
34333adant3 1113 . . . . . . . . . . . . . 14 (((𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉 ∧ (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑋”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑋”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊))))
3511, 34syl 17 . . . . . . . . . . . . 13 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊))))
3635expd 408 . . . . . . . . . . . 12 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → (𝑋 ∈ V → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))))
3736com12 32 . . . . . . . . . . 11 (𝑋 ∈ V → ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))))
388, 37syl 17 . . . . . . . . . 10 ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))))
393, 38sylbid 232 . . . . . . . . 9 ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))))
4039com13 88 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊‘0) = 𝑋 → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))))
4140imp32 411 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))
42 ccats1val2 13788 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋)
4341, 42syl 17 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋)
44 ccat1st1st 13789 . . . . . . . . 9 (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0))
4544ad2antrr 714 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0))
462fveq1d 6498 . . . . . . . . . 10 ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = ((𝑊 ++ ⟨“𝑋”⟩)‘0))
4746eqeq1d 2773 . . . . . . . . 9 ((𝑊‘0) = 𝑋 → (((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0) ↔ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0)))
4847ad2antll 717 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → (((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0) ↔ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0)))
4945, 48mpbid 224 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → ((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0))
50 simpr 477 . . . . . . . 8 (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊‘0) = 𝑋)
5150adantl 474 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → (𝑊‘0) = 𝑋)
5249, 51eqtrd 2807 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋)
535, 43, 52jca31 507 . . . . 5 (((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) ∧ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋))
5453ex 405 . . . 4 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋)))
55 fvexd 6511 . . . . . . . 8 (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → ((𝑊 ++ ⟨“𝑋”⟩)‘0) ∈ V)
56 eleq1 2846 . . . . . . . 8 (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (((𝑊 ++ ⟨“𝑋”⟩)‘0) ∈ V ↔ 𝑋 ∈ V))
5755, 56mpbid 224 . . . . . . 7 (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋𝑋 ∈ V)
5835imp 398 . . . . . . . . . . . . . . . 16 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)))
59 idd 24 . . . . . . . . . . . . . . . . 17 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑊 ∈ Word 𝑉𝑊 ∈ Word 𝑉))
60 idd 24 . . . . . . . . . . . . . . . . 17 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑋𝑉𝑋𝑉))
61 eleq1 2846 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 = (♯‘𝑊) → (𝑁 ∈ ℕ ↔ (♯‘𝑊) ∈ ℕ))
62 lbfzo0 12890 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ (0..^(♯‘𝑊)) ↔ (♯‘𝑊) ∈ ℕ)
6362biimpri 220 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑊) ∈ ℕ → 0 ∈ (0..^(♯‘𝑊)))
6461, 63syl6bi 245 . . . . . . . . . . . . . . . . . . . 20 (𝑁 = (♯‘𝑊) → (𝑁 ∈ ℕ → 0 ∈ (0..^(♯‘𝑊))))
6564com12 32 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 = (♯‘𝑊) → 0 ∈ (0..^(♯‘𝑊))))
6665adantl 474 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑁 = (♯‘𝑊) → 0 ∈ (0..^(♯‘𝑊))))
6766ad2antll 717 . . . . . . . . . . . . . . . . 17 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑁 = (♯‘𝑊) → 0 ∈ (0..^(♯‘𝑊))))
6859, 60, 673anim123d 1423 . . . . . . . . . . . . . . . 16 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → ((𝑊 ∈ Word 𝑉𝑋𝑉𝑁 = (♯‘𝑊)) → (𝑊 ∈ Word 𝑉𝑋𝑉 ∧ 0 ∈ (0..^(♯‘𝑊)))))
6958, 68mpd 15 . . . . . . . . . . . . . . 15 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (𝑊 ∈ Word 𝑉𝑋𝑉 ∧ 0 ∈ (0..^(♯‘𝑊))))
70 ccats1val1 13787 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word 𝑉𝑋𝑉 ∧ 0 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0))
7169, 70syl 17 . . . . . . . . . . . . . 14 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → ((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0))
7271eqeq1d 2773 . . . . . . . . . . . . 13 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ↔ (𝑊‘0) = 𝑋))
7372biimpd 221 . . . . . . . . . . . 12 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ))) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑊‘0) = 𝑋))
7473ex 405 . . . . . . . . . . 11 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑊‘0) = 𝑋)))
7574adantr 473 . . . . . . . . . 10 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) → ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑊‘0) = 𝑋)))
7675com12 32 . . . . . . . . 9 ((𝑋 ∈ V ∧ (𝑊 ∈ Word 𝑉𝑁 ∈ ℕ)) → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑊‘0) = 𝑋)))
7776expcom 406 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑋 ∈ V → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑊‘0) = 𝑋))))
7877com14 96 . . . . . . 7 (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (𝑋 ∈ V → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊‘0) = 𝑋))))
7957, 78mpd 15 . . . . . 6 (((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊‘0) = 𝑋)))
8079impcom 399 . . . . 5 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋) → ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊‘0) = 𝑋))
81 s1eq 13761 . . . . . . . . . . . 12 (𝑋 = (𝑊‘0) → ⟨“𝑋”⟩ = ⟨“(𝑊‘0)”⟩)
8281eqcoms 2779 . . . . . . . . . . 11 ((𝑊‘0) = 𝑋 → ⟨“𝑋”⟩ = ⟨“(𝑊‘0)”⟩)
8382oveq2d 6990 . . . . . . . . . 10 ((𝑊‘0) = 𝑋 → (𝑊 ++ ⟨“𝑋”⟩) = (𝑊 ++ ⟨“(𝑊‘0)”⟩))
8483eleq1d 2843 . . . . . . . . 9 ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺)))
8584biimpac 471 . . . . . . . 8 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺))
86 simpr 477 . . . . . . . 8 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊‘0) = 𝑋)
8785, 86jca 504 . . . . . . 7 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋))
8887ex 405 . . . . . 6 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
8988ad2antrr 714 . . . . 5 ((((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋) → ((𝑊‘0) = 𝑋 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
9080, 89syldc 48 . . . 4 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
9154, 90impbid 204 . . 3 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ↔ (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋)))
929clwwlknwwlksnb 27593 . . . 4 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺)))
9392anbi1d 621 . . 3 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) ↔ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
94 3anan32 1079 . . . 4 (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ↔ (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋))
9594a1i 11 . . 3 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ↔ (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋)))
9691, 93, 953bitr4rd 304 . 2 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
97 wwlknon 27358 . . 3 ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋) ↔ ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋))
9897a1i 11 . 2 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋) ↔ ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) = 𝑋)))
99 isclwwlknon 27634 . . 3 (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋))
10099a1i 11 . 2 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)))
10196, 98, 1003bitr4rd 304 1 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  ∀wral 3081  Vcvv 3408  {cpr 4437  ‘cfv 6185  (class class class)co 6974  0cc0 10333  1c1 10334   + caddc 10336  ℕcn 11437  ℕ0cn0 11705  ..^cfzo 12847  ♯chash 13503  Word cword 13670   ++ cconcat 13731  ⟨“cs1 13756  Vtxcvtx 26499  Edgcedg 26550   WWalksN cwwlksn 27327   WWalksNOn cwwlksnon 27328   ClWWalksN cclwwlkn 27554  ClWWalksNOncclwwlknon 27630 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-nel 3067  df-ral 3086  df-rex 3087  df-reu 3088  df-rmo 3089  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7499  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-oadd 7907  df-er 8087  df-map 8206  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-dju 9122  df-card 9160  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-nn 11438  df-2 11501  df-n0 11706  df-xnn0 11778  df-z 11792  df-uz 12057  df-fz 12707  df-fzo 12848  df-hash 13504  df-word 13671  df-lsw 13724  df-concat 13732  df-s1 13757  df-wwlks 27331  df-wwlksn 27332  df-wwlksnon 27333  df-clwwlk 27503  df-clwwlkn 27555  df-clwwlknon 27631 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator