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 
|- ( ( A e. ( ClWWalks ` G ) /\ B e. ( ClWWalks ` G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ClWWalks ` G ) )

Proof

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