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 ⊢ X ∈ Vtx ⁡ G ∧ W ∈ N WWalksN G ∧ lastS ⁡ W ≠ W ⁡ 0 → W ++ ⟨“ X ”⟩ ⁡ 0 = W ⁡ 0 ∧ W ++ ⟨“ X ”⟩ ⁡ N ≠ W ⁡ 0

Proof

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