Metamath Proof Explorer

Theorem clwwlknonccat

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

Ref Expression
Assertion clwwlknonccat ⊢ A ∈ X ClWWalksNOn ⁡ G M ∧ B ∈ X ClWWalksNOn ⁡ G N → A ++ B ∈ X ClWWalksNOn ⁡ G M + N

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X → A ∈ M ClWWalksN G
2 1 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ∈ M ClWWalksN G
3 simpl ⊢ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → B ∈ N ClWWalksN G
4 3 adantl ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → B ∈ N ClWWalksN G
5 simpr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X → A ⁡ 0 = X
6 5 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ⁡ 0 = X
7 simpr ⊢ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → B ⁡ 0 = X
8 7 eqcomd ⊢ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → X = B ⁡ 0
9 8 adantl ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → X = B ⁡ 0
10 6 9 eqtrd ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ⁡ 0 = B ⁡ 0
11 clwwlknccat ⊢ A ∈ M ClWWalksN G ∧ B ∈ N ClWWalksN G ∧ A ⁡ 0 = B ⁡ 0 → A ++ B ∈ M + N ClWWalksN G
12 2 4 10 11 syl3anc ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ++ B ∈ M + N ClWWalksN G
13 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
14 13 clwwlknwrd ⊢ A ∈ M ClWWalksN G → A ∈ Word Vtx ⁡ G
15 14 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X → A ∈ Word Vtx ⁡ G
16 15 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ∈ Word Vtx ⁡ G
17 13 clwwlknwrd ⊢ B ∈ N ClWWalksN G → B ∈ Word Vtx ⁡ G
18 17 adantr ⊢ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → B ∈ Word Vtx ⁡ G
19 18 adantl ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → B ∈ Word Vtx ⁡ G
20 clwwlknnn ⊢ A ∈ M ClWWalksN G → M ∈ ℕ
21 clwwlknlen ⊢ A ∈ M ClWWalksN G → A = M
22 nngt0 ⊢ M ∈ ℕ → 0 < M
23 breq2 ⊢ A = M → 0 < A ↔ 0 < M
24 22 23 syl5ibrcom ⊢ M ∈ ℕ → A = M → 0 < A
25 20 21 24 sylc ⊢ A ∈ M ClWWalksN G → 0 < A
26 25 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X → 0 < A
27 26 adantr ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → 0 < A
28 ccatfv0 ⊢ A ∈ Word Vtx ⁡ G ∧ B ∈ Word Vtx ⁡ G ∧ 0 < A → A ++ B ⁡ 0 = A ⁡ 0
29 16 19 27 28 syl3anc ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ++ B ⁡ 0 = A ⁡ 0
30 29 6 eqtrd ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ++ B ⁡ 0 = X
31 12 30 jca ⊢ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X → A ++ B ∈ M + N ClWWalksN G ∧ A ++ B ⁡ 0 = X
32 isclwwlknon ⊢ A ∈ X ClWWalksNOn ⁡ G M ↔ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X
33 isclwwlknon ⊢ B ∈ X ClWWalksNOn ⁡ G N ↔ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X
34 32 33 anbi12i ⊢ A ∈ X ClWWalksNOn ⁡ G M ∧ B ∈ X ClWWalksNOn ⁡ G N ↔ A ∈ M ClWWalksN G ∧ A ⁡ 0 = X ∧ B ∈ N ClWWalksN G ∧ B ⁡ 0 = X
35 isclwwlknon ⊢ A ++ B ∈ X ClWWalksNOn ⁡ G M + N ↔ A ++ B ∈ M + N ClWWalksN G ∧ A ++ B ⁡ 0 = X
36 31 34 35 3imtr4i ⊢ A ∈ X ClWWalksNOn ⁡ G M ∧ B ∈ X ClWWalksNOn ⁡ G N → A ++ B ∈ X ClWWalksNOn ⁡ G M + N