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 ⊢ W ∈ Word Vtx ⁡ G → F W ++ ⟨“ W ⁡ 0 ”⟩ ∈ Walks ⁡ G → F = W

Proof

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