This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 ) )