clwwlkwwlksb

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)

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

Proof

Step	Hyp	Ref	Expression
1		clwwlkwwlksb.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fstwrdne	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
3	2	s1cld	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 )
4		ccatlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
5	3 4	syldan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
6		s1len	⊢ ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = 1
7	6	oveq2i	⊢ ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 )
8	5 7	eqtrdi	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
9	8	oveq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) )
10		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ₀ )
11	10	nn0cnd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
12	11	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
13		1cnd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 1 ∈ ℂ )
14	12 13 13	addsubd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) )
15	9 14	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) )
16	15	oveq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) )
17	16	raleqdv	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
18		lennncl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
19		nnm1nn0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ₀ )
20	18 19	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ₀ )
21		elnn0uz	⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ₀ ↔ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ_≥ ‘ 0 ) )
22	20 21	sylib	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ_≥ ‘ 0 ) )
23		fzosplitsn	⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ_≥ ‘ 0 ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
24	22 23	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) )
25	24	raleqdv	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
26		ralunb	⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) } ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
27	25 26	bitrdi	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
28		simpl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 𝑊 ∈ Word 𝑉 )
29	10	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
30	29	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
31		elfzom1elfzo	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32	30 31	sylan	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
33		ccats1val1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
34	28 32 33	syl2an2r	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
35		elfzom1elp1fzo	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36	30 35	sylan	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37		ccats1val1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
38	28 36 37	syl2an2r	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) )
39	34 38	preq12d	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } )
40	39	eleq1d	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
41	40	ralbidva	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
42		ovex	⊢ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ V
43		fveq2	⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
44		fvoveq1	⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) )
45	43 44	preq12d	⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } )
46	45	eleq1d	⊢ ( 𝑖 = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
47	42 46	ralsn	⊢ ( ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
48		fzo0end	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
49	18 48	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
50		ccats1val1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
51	49 50	syldan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
52		lsw	⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
53	52	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
54	51 53	eqtr4d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
55		npcan1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
56	11 55	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
57	56	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
58	57	fveq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) )
59		eqidd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
60		ccats1val2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( 𝑊 ‘ 0 ) )
61	28 2 59 60	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ♯ ‘ 𝑊 ) ) = ( 𝑊 ‘ 0 ) )
62	58 61	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) = ( 𝑊 ‘ 0 ) )
63	54 62	preq12d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } = { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } )
64	63	eleq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
65	47 64	syl5bb	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
66	41 65	anbi12d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑊 ) − 1 ) } { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
67	17 27 66	3bitrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
68	28 3	jca	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) )
69		ccat0	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ∅ ↔ ( 𝑊 = ∅ ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ∅ ) ) )
70		simpl	⊢ ( ( 𝑊 = ∅ ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ∅ ) → 𝑊 = ∅ )
71	69 70	syl6bi	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = ∅ → 𝑊 = ∅ ) )
72	71	necon3d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( 𝑊 ≠ ∅ → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ) )
73	72	adantld	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ) )
74	68 73	mpcom	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ )
75		wrdv	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V )
76		s1cli	⊢ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V
77		ccatalpha	⊢ ( ( 𝑊 ∈ Word V ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
78	75 76 77	sylancl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
79	78	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word 𝑉 ) ) )
80	28 3 79	mpbir2and	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 )
81	74 80	jca	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) )
82		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
83	1 82	iswwlks	⊢ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
84		df-3an	⊢ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
85	83 84	bitri	⊢ ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
86	85	a1i	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ≠ ∅ ∧ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ Word 𝑉 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
87	81 86	mpbirand	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) { ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ 𝑖 ) , ( ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
88	1 82	isclwwlk	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
89		3anass	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
90	88 89	bitri	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
91	90	baib	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
92	67 87 91	3bitr4rd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ) )

Metamath Proof Explorer

Theorem clwwlkwwlksb

Proof