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 ( ( 𝐴 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑀 ) ∧ 𝐵 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑀 + 𝑁 ) ) )

Proof

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