# Metamath Proof Explorer

## Theorem clwwlkccat

Description: The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion clwwlkccat ${⊢}\left({A}\in \mathrm{ClWWalks}\left({G}\right)\wedge {B}\in \mathrm{ClWWalks}\left({G}\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{ClWWalks}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 simp1l ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to {A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
2 simp1l ${⊢}\left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
3 ccatcl ${⊢}\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
4 1 2 3 syl2an ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
5 ccat0 ${⊢}\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({A}\mathrm{++}{B}=\varnothing ↔\left({A}=\varnothing \wedge {B}=\varnothing \right)\right)$
6 5 adantlr ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({A}\mathrm{++}{B}=\varnothing ↔\left({A}=\varnothing \wedge {B}=\varnothing \right)\right)$
7 simpr ${⊢}\left({A}=\varnothing \wedge {B}=\varnothing \right)\to {B}=\varnothing$
8 6 7 syl6bi ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({A}\mathrm{++}{B}=\varnothing \to {B}=\varnothing \right)$
9 8 necon3d ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\right)\to \left({B}\ne \varnothing \to {A}\mathrm{++}{B}\ne \varnothing \right)$
10 9 impr ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\right)\to {A}\mathrm{++}{B}\ne \varnothing$
11 10 3ad2antr1 ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {A}\mathrm{++}{B}\ne \varnothing$
12 11 3ad2antl1 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {A}\mathrm{++}{B}\ne \varnothing$
13 4 12 jca ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left({A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\mathrm{++}{B}\ne \varnothing \right)$
14 13 3adant3 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left({A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\mathrm{++}{B}\ne \varnothing \right)$
15 clwwlkccatlem ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \forall {i}\in \left(0..^\left|{A}\mathrm{++}{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({A}\mathrm{++}{B}\right)\left({i}\right),\left({A}\mathrm{++}{B}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)$
16 simpl1l ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
17 simpr1l ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)$
18 simpr1r ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to {B}\ne \varnothing$
19 lswccatn0lsw ${⊢}\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\to \mathrm{lastS}\left({A}\mathrm{++}{B}\right)=\mathrm{lastS}\left({B}\right)$
20 16 17 18 19 syl3anc ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \mathrm{lastS}\left({A}\mathrm{++}{B}\right)=\mathrm{lastS}\left({B}\right)$
21 20 3adant3 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \mathrm{lastS}\left({A}\mathrm{++}{B}\right)=\mathrm{lastS}\left({B}\right)$
22 hashgt0 ${⊢}\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\to 0<\left|{A}\right|$
23 22 3ad2ant1 ${⊢}\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to 0<\left|{A}\right|$
24 23 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to 0<\left|{A}\right|$
25 ccatfv0 ${⊢}\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 0<\left|{A}\right|\right)\to \left({A}\mathrm{++}{B}\right)\left(0\right)={A}\left(0\right)$
26 16 17 24 25 syl3anc ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)\to \left({A}\mathrm{++}{B}\right)\left(0\right)={A}\left(0\right)$
27 26 3adant3 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left({A}\mathrm{++}{B}\right)\left(0\right)={A}\left(0\right)$
28 simp3 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to {A}\left(0\right)={B}\left(0\right)$
29 27 28 eqtrd ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left({A}\mathrm{++}{B}\right)\left(0\right)={B}\left(0\right)$
30 21 29 preq12d ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left\{\mathrm{lastS}\left({A}\mathrm{++}{B}\right),\left({A}\mathrm{++}{B}\right)\left(0\right)\right\}=\left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}$
31 simp23 ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)$
32 30 31 eqeltrd ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left\{\mathrm{lastS}\left({A}\mathrm{++}{B}\right),\left({A}\mathrm{++}{B}\right)\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)$
33 14 15 32 3jca ${⊢}\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to \left(\left({A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\mathrm{++}{B}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\mathrm{++}{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({A}\mathrm{++}{B}\right)\left({i}\right),\left({A}\mathrm{++}{B}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\mathrm{++}{B}\right),\left({A}\mathrm{++}{B}\right)\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
34 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
35 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
36 34 35 isclwwlk ${⊢}{A}\in \mathrm{ClWWalks}\left({G}\right)↔\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
37 34 35 isclwwlk ${⊢}{B}\in \mathrm{ClWWalks}\left({G}\right)↔\left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
38 biid ${⊢}{A}\left(0\right)={B}\left(0\right)↔{A}\left(0\right)={B}\left(0\right)$
39 36 37 38 3anbi123i ${⊢}\left({A}\in \mathrm{ClWWalks}\left({G}\right)\wedge {B}\in \mathrm{ClWWalks}\left({G}\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)↔\left(\left(\left({A}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{A}\left({i}\right),{A}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\right),{A}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge \left(\left({B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {B}\ne \varnothing \right)\wedge \forall {j}\in \left(0..^\left|{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{B}\left({j}\right),{B}\left({j}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({B}\right),{B}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)$
40 34 35 isclwwlk ${⊢}{A}\mathrm{++}{B}\in \mathrm{ClWWalks}\left({G}\right)↔\left(\left({A}\mathrm{++}{B}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge {A}\mathrm{++}{B}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{A}\mathrm{++}{B}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{\left({A}\mathrm{++}{B}\right)\left({i}\right),\left({A}\mathrm{++}{B}\right)\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({A}\mathrm{++}{B}\right),\left({A}\mathrm{++}{B}\right)\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
41 33 39 40 3imtr4i ${⊢}\left({A}\in \mathrm{ClWWalks}\left({G}\right)\wedge {B}\in \mathrm{ClWWalks}\left({G}\right)\wedge {A}\left(0\right)={B}\left(0\right)\right)\to {A}\mathrm{++}{B}\in \mathrm{ClWWalks}\left({G}\right)$