This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
2 simp1l ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
3 ccatcl ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) )
4 1 2 3 syl2an ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) )
5 ccat0 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝐴 ++ 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
6 5 adantlr ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝐴 ++ 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
7 simpr ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
8 6 7 biimtrdi ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝐴 ++ 𝐵 ) = ∅ → 𝐵 = ∅ ) )
9 8 necon3d ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝐵 ≠ ∅ → ( 𝐴 ++ 𝐵 ) ≠ ∅ ) )
10 9 impr ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ++ 𝐵 ) ≠ ∅ )
11 10 3ad2antr1 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐴 ++ 𝐵 ) ≠ ∅ )
12 11 3ad2antl1 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐴 ++ 𝐵 ) ≠ ∅ )
13 4 12 jca ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ++ 𝐵 ) ≠ ∅ ) )
14 13 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ++ 𝐵 ) ≠ ∅ ) )
15 clwwlkccatlem ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
16 simpl1l ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
17 simpr1l ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
18 simpr1r ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝐵 ≠ ∅ )
19 lswccatn0lsw ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) → ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) = ( lastS ‘ 𝐵 ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) = ( lastS ‘ 𝐵 ) )
21 20 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) = ( lastS ‘ 𝐵 ) )
22 hashgt0 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐴 ) )
23 22 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → 0 < ( ♯ ‘ 𝐴 ) )
24 23 adantr ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → 0 < ( ♯ ‘ 𝐴 ) )
25 ccatfv0 ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
26 16 17 24 25 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
27 26 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
28 simp3 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
29 27 28 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) = ( 𝐵 ‘ 0 ) )
30 21 29 preq12d ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → { ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) } = { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } )
31 simp23 ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
32 30 31 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → { ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
33 14 15 32 3jca ⊢ ( ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ( ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ++ 𝐵 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
34 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
35 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
36 34 35 isclwwlk ⊢ ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
37 34 35 isclwwlk ⊢ ( 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
38 biid ⊢ ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ↔ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
39 36 37 38 3anbi123i ⊢ ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ↔ ( ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) { ( 𝐴 ‘ 𝑖 ) , ( 𝐴 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐴 ) , ( 𝐴 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ≠ ∅ ) ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) { ( 𝐵 ‘ 𝑗 ) , ( 𝐵 ‘ ( 𝑗 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝐵 ) , ( 𝐵 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
40 34 35 isclwwlk ⊢ ( ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( ( 𝐴 ++ 𝐵 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝐴 ++ 𝐵 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) − 1 ) ) { ( ( 𝐴 ++ 𝐵 ) ‘ 𝑖 ) , ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝐴 ++ 𝐵 ) ) , ( ( 𝐴 ++ 𝐵 ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
41 33 39 40 3imtr4i ⊢ ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) )