Metamath Proof Explorer

Theorem clwwlknccat

Description: The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk with a length which is the sum of the lengths of the two walks. 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, 24-Apr-2022)

Ref Expression
Assertion clwwlknccat ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ( 𝑀 + 𝑁 ) ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 isclwwlkn ⊢ ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ↔ ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐴 ) = 𝑀 ) )
2 isclwwlkn ⊢ ( 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐵 ) = 𝑁 ) )
3 biid ⊢ ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ↔ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
4 simpl ⊢ ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐴 ) = 𝑀 ) → 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) )
5 simpl ⊢ ( ( 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) )
6 id ⊢ ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
7 clwwlkccat ⊢ ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) )
8 4 5 6 7 syl3an ⊢ ( ( ( 𝐴 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐴 ) = 𝑀 ) ∧ ( 𝐵 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐵 ) = 𝑁 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) )
9 1 2 3 8 syl3anb ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) )
10 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11 10 clwwlknwrd ⊢ ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) → 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) )
12 10 clwwlknwrd ⊢ ( 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
13 ccatlen ⊢ ( ( 𝐴 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
14 11 12 13 syl2an ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
15 clwwlknlen ⊢ ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝐴 ) = 𝑀 )
16 clwwlknlen ⊢ ( 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝐵 ) = 𝑁 )
17 15 16 oveqan12d ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝑀 + 𝑁 ) )
18 14 17 eqtrd ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( 𝑀 + 𝑁 ) )
19 18 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( 𝑀 + 𝑁 ) )
20 isclwwlkn ⊢ ( ( 𝐴 ++ 𝐵 ) ∈ ( ( 𝑀 + 𝑁 ) ClWWalksN 𝐺 ) ↔ ( ( 𝐴 ++ 𝐵 ) ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( 𝑀 + 𝑁 ) ) )
21 9 19 20 sylanbrc ⊢ ( ( 𝐴 ∈ ( 𝑀 ClWWalksN 𝐺 ) ∧ 𝐵 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) → ( 𝐴 ++ 𝐵 ) ∈ ( ( 𝑀 + 𝑁 ) ClWWalksN 𝐺 ) )