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 ∈ ClWWalks ⁡ G ∧ B ∈ ClWWalks ⁡ G ∧ A ⁡ 0 = B ⁡ 0 → A ++ B ∈ ClWWalks ⁡ G

Proof

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