clwwlkwwlksb - Metamath Proof Explorer

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

Theorem clwwlkwwlksb 30645

Description: A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022.)

**Hypothesis**
Ref	Expression
clwwlkwwlksb.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
clwwlkwwlksb	⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺)))

Proof of Theorem clwwlkwwlksb Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fstwrdne 14700	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)
2	1	s1cld 14750	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)
3		ccatlen 14720	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)))
4	2, 3	syldan 603	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)))
5		s1len 14753	. . . . . . . . 9 ⊢ (♯‘⟨“(𝑊‘0)”⟩) = 1
6	5	oveq2i 7431	. . . . . . . 8 ⊢ ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + 1)
7	4, 6	eqtrdi 2812	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + 1))
8	7	oveq1d 7435	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
9		lencl 14678	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
10	9	nn0cnd 12669	. . . . . . . 8 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ)
11	10	adantr 486	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℂ)
12		1cnd 11302	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 1 ∈ ℂ)
13	11, 12, 12	addsubd 11690	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (((♯‘𝑊) + 1) − 1) = (((♯‘𝑊) − 1) + 1))
14	8, 13	eqtrd 2796	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1) = (((♯‘𝑊) − 1) + 1))
15	14	oveq2d 7436	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)) = (0..^(((♯‘𝑊) − 1) + 1)))
16	15	raleqdv 3320	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
17		lennncl 14679	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
18		nnm1nn0 12647	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ ℕ₀)
19	17, 18	syl 18	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ ℕ₀)
20		elnn0uz 13006	. . . . . . 7 ⊢ (((♯‘𝑊) − 1) ∈ ℕ₀ ↔ ((♯‘𝑊) − 1) ∈ (ℤ_≥‘0))
21	19, 20	sylib 221	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ (ℤ_≥‘0))
22		fzosplitsn 13911	. . . . . 6 ⊢ (((♯‘𝑊) − 1) ∈ (ℤ_≥‘0) → (0..^(((♯‘𝑊) − 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}))
23	21, 22	syl 18	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (0..^(((♯‘𝑊) − 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}))
24	23	raleqdv 3320	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
25		ralunb 4143	. . . 4 ⊢ (∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
26	24, 25	bitrdi 290	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
27		simpl 488	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝑉)
28	9	nn0zd 12718	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
29	28	adantr 486	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℤ)
30		elfzom1elfzo 13868	. . . . . . . . 9 ⊢ (((♯‘𝑊) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ (0..^(♯‘𝑊)))
31	29, 30	sylan 592	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ (0..^(♯‘𝑊)))
32		ccats1val1 14774	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = (𝑊‘𝑖))
33	27, 31, 32	syl2an2r 698	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = (𝑊‘𝑖))
34		elfzom1elp1fzo 13867	. . . . . . . . 9 ⊢ (((♯‘𝑊) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
35	29, 34	sylan 592	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
36		ccats1val1 14774	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
37	27, 35, 36	syl2an2r 698	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
38	33, 37	preq12d 4702	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
39	38	eleq1d 2846	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
40	39	ralbidva 3184	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
41		ovex 7453	. . . . . 6 ⊢ ((♯‘𝑊) − 1) ∈ V
42		fveq2 6885	. . . . . . . 8 ⊢ (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)))
43		fvoveq1 7443	. . . . . . . 8 ⊢ (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)))
44	42, 43	preq12d 4702	. . . . . . 7 ⊢ (𝑖 = ((♯‘𝑊) − 1) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))})
45	44	eleq1d 2846	. . . . . 6 ⊢ (𝑖 = ((♯‘𝑊) − 1) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺)))
46	41, 45	ralsn 4642	. . . . 5 ⊢ (∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺))
47		fzo0end 13893	. . . . . . . . . 10 ⊢ ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
48	17, 47	syl 18	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
49		ccats1val1 14774	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
50	48, 49	syldan 603	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
51		lsw 14709	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
52	51	adantr 486	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
53	50, 52	eqtr4d 2799	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
54		npcan1 11741	. . . . . . . . . . 11 ⊢ ((♯‘𝑊) ∈ ℂ → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
55	10, 54	syl 18	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
56	55	adantr 486	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
57	56	fveq2d 6889	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)))
58		eqidd 2762	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) = (♯‘𝑊))
59		ccats1val2 14775	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)) = (𝑊‘0))
60	27, 1, 58, 59	syl3anc 1398	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)) = (𝑊‘0))
61	57, 60	eqtrd 2796	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)) = (𝑊‘0))
62	53, 61	preq12d 4702	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} = {(lastS‘𝑊), (𝑊‘0)})
63	62	eleq1d 2846	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
64	46, 63	bitrid 286	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
65	40, 64	anbi12d 644	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
66	16, 26, 65	3bitrd 308	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
67	27, 2	jca 521	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉))
68		ccat0 14721	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) = ∅ ↔ (𝑊 = ∅ ∧ ⟨“(𝑊‘0)”⟩ = ∅)))
69		simpl 488	. . . . . . . 8 ⊢ ((𝑊 = ∅ ∧ ⟨“(𝑊‘0)”⟩ = ∅) → 𝑊 = ∅)
70	68, 69	biimtrdi 256	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) = ∅ → 𝑊 = ∅))
71	70	necon3d 2977	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → (𝑊 ≠ ∅ → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅))
72	71	adantld 496	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅))
73	67, 72	mpcom 39	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅)
74		wrdv 14674	. . . . . . 7 ⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V)
75		s1cli 14752	. . . . . . 7 ⊢ ⟨“(𝑊‘0)”⟩ ∈ Word V
76		ccatalpha 14740	. . . . . . 7 ⊢ ((𝑊 ∈ Word V ∧ ⟨“(𝑊‘0)”⟩ ∈ Word V) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
77	74, 75, 76	sylancl 598	. . . . . 6 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
78	77	adantr 486	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
79	27, 2, 78	mpbir2and 726	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉)
80	73, 79	jca 521	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉))
81		clwwlkwwlksb.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
82		eqid 2761	. . . . . 6 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
83	81, 82	iswwlks 30425	. . . . 5 ⊢ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
84		df-3an 1105	. . . . 5 ⊢ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
85	83, 84	bitri 278	. . . 4 ⊢ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
86	85	a1i 11	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
87	80, 86	mpbirand 720	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
88	81, 82	isclwwlk 30575	. . . 4 ⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
89		3anass 1111	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
90	88, 89	bitri 278	. . 3 ⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
91	90	baib 545	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
92	66, 87, 91	3bitr4rd 315	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 Vcvv 3451 ∪ cun 3897 ∅c0 4279 {csn 4584 {cpr 4586 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 0cc0 11200 1c1 11201 + caddc 11203 − cmin 11541 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ..^cfzo 13788 ♯chash 14474 Word cword 14658 lastSclsw 14707 ++ cconcat 14715 ⟨“cs1 14742 Vtxcvtx 29574 Edgcedg 29625 WWalkscwwlks 30414 ClWWalkscclwwlk 30572

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-er 8717 df-map 8849 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-n0 12607 df-xnn0 12680 df-z 12694 df-uz 12966 df-fz 13640 df-fzo 13789 df-hash 14475 df-word 14659 df-lsw 14708 df-concat 14716 df-s1 14743 df-wwlks 30419 df-clwwlk 30573

This theorem is used by: clwwlknwwlksnb 30646

W3C validator