Metamath Proof Explorer

Theorem wlklenvclwlk

Description: The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018) (Revised by AV, 2-May-2021) (Revised by JJ, 14-Jan-2024)

Ref Expression
Assertion wlklenvclwlk ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ↔ ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) )
2 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
3 wlklenvp1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
4 2 3 jca ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
5 1 4 sylbir ⊢ ( ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
6 ccatws1len ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
7 6 eqeq1d ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
8 eqcom ⊢ ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
9 7 8 bitrdi ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
10 9 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
11 nn0cn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
12 11 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ∈ ℂ )
13 lencl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
14 13 nn0cnd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
15 14 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
16 1cnd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → 1 ∈ ℂ )
17 12 15 16 addcan2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
18 17 biimpd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
19 10 18 sylbid ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
20 19 expimpd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
21 5 20 syl5 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )