Metamath Proof Explorer

Theorem wlklenvclwlkOLD

Description: Obsolete version of wlklenvclwlk as of 14-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ↔ ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) )
2 wlklenvp1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
3 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
4 wrdsymb1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
5 4 s1cld ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
6 ccatlenOLD ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
7 5 6 syldan ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) )
8 s1len ⊢ ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = 1
9 8 a1i ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = 1 )
10 9 oveq2d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) + ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
11 7 10 eqtrd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
12 11 eqeq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
13 lencl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
14 eqcom ⊢ ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ↔ ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
15 nn0cn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
16 15 adantl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ∈ ℂ )
17 nn0cn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
18 17 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
19 1cnd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → 1 ∈ ℂ )
20 16 18 19 addcan2d ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
21 20 biimpd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝐹 ) + 1 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
22 14 21 syl5bi ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
23 22 ex ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
24 23 com23 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
25 13 24 syl ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
26 25 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
27 12 26 sylbid ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
28 27 com3l ⊢ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) ) )
29 2 3 28 sylc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
30 1 29 sylbir ⊢ ( ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )
31 30 com12 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( ⟨ 𝐹 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝑊 ) ) )