Metamath Proof Explorer

Theorem numclwwlk2lem1lem

Description: Lemma for numclwwlk2lem1 . (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-May-2021) (Revised by AV, 15-Mar-2022)

Ref Expression
Assertion numclwwlk2lem1lem ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
2 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
3 s1cl ⊢ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ⟨“ 𝑋 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
4 3 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → ⟨“ 𝑋 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
5 nn0p1gt0 ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
6 5 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 < ( 𝑁 + 1 ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → 0 < ( 𝑁 + 1 ) )
8 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
11 7 10 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → 0 < ( ♯ ‘ 𝑊 ) )
12 ccatfv0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ 𝑋 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
13 2 4 11 12 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
14 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
15 14 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
16 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
17 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18 16 17 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
19 18 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
20 15 19 eqtr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
21 20 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑁 = ( ( ♯ ‘ 𝑊 ) − 1 ) )
22 21 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) = ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
23 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
24 3 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ⟨“ 𝑋 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
25 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → 0 < ( 𝑁 + 1 ) )
26 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 0 < ( 𝑁 + 1 ) ) )
27 25 26 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
28 hashneq0 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
29 28 bicomd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 ≠ ∅ ↔ 0 < ( ♯ ‘ 𝑊 ) ) )
30 29 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ≠ ∅ ↔ 0 < ( ♯ ‘ 𝑊 ) ) )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 ≠ ∅ ↔ 0 < ( ♯ ‘ 𝑊 ) ) )
32 27 31 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑊 ≠ ∅ )
33 ccatval1lsw ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ 𝑋 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
34 23 24 32 33 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( lastS ‘ 𝑊 ) )
35 22 34 eqtr2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( lastS ‘ 𝑊 ) = ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) )
36 35 neeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
37 36 biimpd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
38 37 impr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) )
39 13 38 jca ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )
40 39 exp32 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) ) ) )
41 1 40 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) → ( ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) ) ) )
42 41 3imp21 ⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑊 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ‘ 𝑁 ) ≠ ( 𝑊 ‘ 0 ) ) )