Theorem wwlksnprcl

Description: Derivation of the length of a word W whose concatenation with a singleton word represents a walk of a fixed length N (a partial reverse closure theorem). (Contributed by AV, 4-Mar-2022)

	Ref	Expression
Assertion	wwlksnprcl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		iswwlksn	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
2	1	adantl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) ) )
3		ccatws1lenp1b	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
4	3	biimpd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
5	4	adantld	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )
6	2 5	sylbid	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )