# 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 ${⊢}\left({X}\in \mathrm{Vtx}\left({G}\right)\wedge {W}\in \left({N}\mathrm{WWalksN}{G}\right)\wedge \mathrm{lastS}\left({W}\right)\ne {W}\left(0\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\left(0\right)={W}\left(0\right)\wedge \left({W}\mathrm{++}⟨“{X}”⟩\right)\left({N}\right)\ne {W}\left(0\right)\right)$

### Proof

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