# Metamath Proof Explorer

## Theorem 2clwwlk2clwwlk

Description: An element of the value of operation C , i.e., a word being a double loop of length N on vertex X , is composed of two closed walks. (Contributed by AV, 28-Apr-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypothesis 2clwwlk.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
Assertion 2clwwlk2clwwlk ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\in \left({X}{C}{N}\right)↔\exists {a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\phantom{\rule{.4em}{0ex}}{W}={a}\mathrm{++}{b}\right)$

### Proof

Step Hyp Ref Expression
1 2clwwlk.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\ge 2}⟼\left\{{w}\in \left({v}\mathrm{ClWWalksNOn}\left({G}\right){n}\right)|{w}\left({n}-2\right)={v}\right\}\right)$
2 uzuzle23 ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}\in {ℤ}_{\ge 2}$
3 1 2clwwlkel ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({W}\in \left({X}{C}{N}\right)↔\left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)$
4 2 3 sylan2 ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\in \left({X}{C}{N}\right)↔\left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)$
5 simpr ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}\in {ℤ}_{\ge 3}$
6 5 anim1i ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to \left({N}\in {ℤ}_{\ge 3}\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)$
7 3anass ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge {W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)↔\left({N}\in {ℤ}_{\ge 3}\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)$
8 6 7 sylibr ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to \left({N}\in {ℤ}_{\ge 3}\wedge {W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)$
9 clwwnonrepclwwnon ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge {W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\to {W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)$
10 8 9 syl ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)$
11 5 adantr ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {N}\in {ℤ}_{\ge 3}$
12 simprl ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)$
13 simprr ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}\left({N}-2\right)={X}$
14 isclwwlknon ${⊢}{W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)$
15 simpr ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)\to {W}\left(0\right)={X}$
16 15 eqcomd ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)\to {X}={W}\left(0\right)$
17 14 16 sylbi ${⊢}{W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\to {X}={W}\left(0\right)$
18 17 ad2antrl ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {X}={W}\left(0\right)$
19 13 18 eqtrd ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}\left({N}-2\right)={W}\left(0\right)$
20 2clwwlk2clwwlklem ${⊢}\left({N}\in {ℤ}_{\ge 3}\wedge {W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={W}\left(0\right)\right)\to {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)$
21 11 12 19 20 syl3anc ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)$
22 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
23 22 clwwlknbp ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)$
24 opeq2 ${⊢}{N}=\left|{W}\right|\to ⟨{N}-2,{N}⟩=⟨{N}-2,\left|{W}\right|⟩$
25 24 oveq2d ${⊢}{N}=\left|{W}\right|\to {W}\mathrm{substr}⟨{N}-2,{N}⟩={W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩$
26 25 oveq2d ${⊢}{N}=\left|{W}\right|\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩\right)$
27 26 eqcoms ${⊢}\left|{W}\right|={N}\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩\right)$
28 27 ad2antlr ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩\right)$
29 simpl ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
30 fz1ssfz0 ${⊢}\left(1\dots {N}\right)\subseteq \left(0\dots {N}\right)$
31 ige3m2fz ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2\in \left(1\dots {N}\right)$
32 30 31 sseldi ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2\in \left(0\dots {N}\right)$
33 32 adantl ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}-2\in \left(0\dots {N}\right)$
34 33 adantl ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to {N}-2\in \left(0\dots {N}\right)$
35 oveq2 ${⊢}\left|{W}\right|={N}\to \left(0\dots \left|{W}\right|\right)=\left(0\dots {N}\right)$
36 35 eleq2d ${⊢}\left|{W}\right|={N}\to \left({N}-2\in \left(0\dots \left|{W}\right|\right)↔{N}-2\in \left(0\dots {N}\right)\right)$
37 36 ad2antlr ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({N}-2\in \left(0\dots \left|{W}\right|\right)↔{N}-2\in \left(0\dots {N}\right)\right)$
38 34 37 mpbird ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to {N}-2\in \left(0\dots \left|{W}\right|\right)$
39 pfxcctswrd ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {N}-2\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩\right)={W}$
40 29 38 39 syl2an2r ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,\left|{W}\right|⟩\right)={W}$
41 28 40 eqtrd ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}$
42 23 41 sylan ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}$
43 42 ex ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}\right)$
44 43 adantr ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}\right)$
45 14 44 sylbi ${⊢}{W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}\right)$
46 45 adantr ${⊢}\left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}\right)$
47 46 impcom ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)={W}$
48 47 eqcomd ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to {W}=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)$
49 10 21 48 3jca ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\wedge {W}=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)\right)$
50 49 ex ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge {W}\left({N}-2\right)={X}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\wedge {W}=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)\right)\right)$
51 4 50 sylbid ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\in \left({X}{C}{N}\right)\to \left({W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\wedge {W}=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)\right)\right)$
52 rspceov ${⊢}\left({W}\mathrm{prefix}\left({N}-2\right)\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {W}\mathrm{substr}⟨{N}-2,{N}⟩\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\wedge {W}=\left({W}\mathrm{prefix}\left({N}-2\right)\right)\mathrm{++}\left({W}\mathrm{substr}⟨{N}-2,{N}⟩\right)\right)\to \exists {a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\phantom{\rule{.4em}{0ex}}{W}={a}\mathrm{++}{b}$
53 51 52 syl6 ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\in \left({X}{C}{N}\right)\to \exists {a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\phantom{\rule{.4em}{0ex}}{W}={a}\mathrm{++}{b}\right)$
54 eluzelcn ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}\in ℂ$
55 2cnd ${⊢}{N}\in {ℤ}_{\ge 3}\to 2\in ℂ$
56 54 55 npcand ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2+2={N}$
57 56 adantl ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {N}-2+2={N}$
58 57 oveq2d ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to {X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2+2\right)={X}\mathrm{ClWWalksNOn}\left({G}\right){N}$
59 58 eleq2d ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2+2\right)\right)↔{a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\right)$
60 59 biimpd ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2+2\right)\right)\to {a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\right)$
61 clwwlknonccat ${⊢}\left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\to {a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2+2\right)\right)$
62 60 61 impel ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\right)\to {a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)$
63 isclwwlknon ${⊢}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)↔\left({b}\in \left(2\mathrm{ClWWalksN}{G}\right)\wedge {b}\left(0\right)={X}\right)$
64 clwwlkn2 ${⊢}{b}\in \left(2\mathrm{ClWWalksN}{G}\right)↔\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{b}\left(0\right),{b}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
65 isclwwlknon ${⊢}{a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)↔\left({a}\in \left(\left({N}-2\right)\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)$
66 22 clwwlknbp ${⊢}{a}\in \left(\left({N}-2\right)\mathrm{ClWWalksN}{G}\right)\to \left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{a}\right|={N}-2\right)$
67 simpl ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\to {a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
68 simprr ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\to {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
69 2nn ${⊢}2\in ℕ$
70 lbfzo0 ${⊢}0\in \left(0..^2\right)↔2\in ℕ$
71 69 70 mpbir ${⊢}0\in \left(0..^2\right)$
72 oveq2 ${⊢}\left|{b}\right|=2\to \left(0..^\left|{b}\right|\right)=\left(0..^2\right)$
73 71 72 eleqtrrid ${⊢}\left|{b}\right|=2\to 0\in \left(0..^\left|{b}\right|\right)$
74 73 ad2antrl ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\to 0\in \left(0..^\left|{b}\right|\right)$
75 67 68 74 3jca ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\to \left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 0\in \left(0..^\left|{b}\right|\right)\right)$
76 75 adantr ${⊢}\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\to \left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 0\in \left(0..^\left|{b}\right|\right)\right)$
77 76 adantr ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 0\in \left(0..^\left|{b}\right|\right)\right)$
78 ccatval3 ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 0\in \left(0..^\left|{b}\right|\right)\right)\to \left({a}\mathrm{++}{b}\right)\left(0+\left|{a}\right|\right)={b}\left(0\right)$
79 77 78 syl ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({a}\mathrm{++}{b}\right)\left(0+\left|{a}\right|\right)={b}\left(0\right)$
80 simpr ${⊢}\left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\to \left|{a}\right|={N}-2$
81 80 oveq2d ${⊢}\left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\to 0+\left|{a}\right|=0+{N}-2$
82 81 adantl ${⊢}\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\to 0+\left|{a}\right|=0+{N}-2$
83 54 55 subcld ${⊢}{N}\in {ℤ}_{\ge 3}\to {N}-2\in ℂ$
84 83 addid2d ${⊢}{N}\in {ℤ}_{\ge 3}\to 0+{N}-2={N}-2$
85 84 adantl ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to 0+{N}-2={N}-2$
86 82 85 sylan9eq ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to 0+\left|{a}\right|={N}-2$
87 86 eqcomd ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to {N}-2=0+\left|{a}\right|$
88 87 fveq2d ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)=\left({a}\mathrm{++}{b}\right)\left(0+\left|{a}\right|\right)$
89 simpl ${⊢}\left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\to {b}\left(0\right)={X}$
90 89 eqcomd ${⊢}\left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\to {X}={b}\left(0\right)$
91 90 ad2antlr ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to {X}={b}\left(0\right)$
92 79 88 91 3eqtr4d ${⊢}\left(\left(\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\right)\wedge \left({b}\left(0\right)={X}\wedge \left|{a}\right|={N}-2\right)\right)\wedge \left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}$
93 92 exp53 ${⊢}{a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({b}\left(0\right)={X}\to \left(\left|{a}\right|={N}-2\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)\right)$
94 93 com24 ${⊢}{a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(\left|{a}\right|={N}-2\to \left({b}\left(0\right)={X}\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)\right)$
95 94 imp ${⊢}\left({a}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{a}\right|={N}-2\right)\to \left({b}\left(0\right)={X}\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
96 66 95 syl ${⊢}{a}\in \left(\left({N}-2\right)\mathrm{ClWWalksN}{G}\right)\to \left({b}\left(0\right)={X}\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
97 96 adantr ${⊢}\left({a}\in \left(\left({N}-2\right)\mathrm{ClWWalksN}{G}\right)\wedge {a}\left(0\right)={X}\right)\to \left({b}\left(0\right)={X}\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
98 65 97 sylbi ${⊢}{a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left({b}\left(0\right)={X}\to \left(\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
99 98 com13 ${⊢}\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({b}\left(0\right)={X}\to \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
100 99 3adant3 ${⊢}\left(\left|{b}\right|=2\wedge {b}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left\{{b}\left(0\right),{b}\left(1\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left({b}\left(0\right)={X}\to \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
101 64 100 sylbi ${⊢}{b}\in \left(2\mathrm{ClWWalksN}{G}\right)\to \left({b}\left(0\right)={X}\to \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)\right)$
102 101 imp ${⊢}\left({b}\in \left(2\mathrm{ClWWalksN}{G}\right)\wedge {b}\left(0\right)={X}\right)\to \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)$
103 63 102 sylbi ${⊢}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\to \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)$
104 103 impcom ${⊢}\left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\to \left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)$
105 104 impcom ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\right)\to \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}$
106 1 2clwwlkel ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({a}\mathrm{++}{b}\in \left({X}{C}{N}\right)↔\left({a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)$
107 2 106 sylan2 ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({a}\mathrm{++}{b}\in \left({X}{C}{N}\right)↔\left({a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)$
108 107 adantr ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\right)\to \left({a}\mathrm{++}{b}\in \left({X}{C}{N}\right)↔\left({a}\mathrm{++}{b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)\wedge \left({a}\mathrm{++}{b}\right)\left({N}-2\right)={X}\right)\right)$
109 62 105 108 mpbir2and ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\right)\to {a}\mathrm{++}{b}\in \left({X}{C}{N}\right)$
110 eleq1 ${⊢}{W}={a}\mathrm{++}{b}\to \left({W}\in \left({X}{C}{N}\right)↔{a}\mathrm{++}{b}\in \left({X}{C}{N}\right)\right)$
111 109 110 syl5ibrcom ${⊢}\left(\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\wedge \left({a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\wedge {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\right)\right)\to \left({W}={a}\mathrm{++}{b}\to {W}\in \left({X}{C}{N}\right)\right)$
112 111 rexlimdvva ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left(\exists {a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\phantom{\rule{.4em}{0ex}}{W}={a}\mathrm{++}{b}\to {W}\in \left({X}{C}{N}\right)\right)$
113 53 112 impbid ${⊢}\left({X}\in {V}\wedge {N}\in {ℤ}_{\ge 3}\right)\to \left({W}\in \left({X}{C}{N}\right)↔\exists {a}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)\left({N}-2\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right)2\right)\phantom{\rule{.4em}{0ex}}{W}={a}\mathrm{++}{b}\right)$