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	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) )

Proof

Step	Hyp	Ref	Expression
1		isclwwlkn	|- ( A e. ( M ClWWalksN G ) <-> ( A e. ( ClWWalks ` G ) /\ ( # ` A ) = M ) )
2		isclwwlkn	|- ( B e. ( N ClWWalksN G ) <-> ( B e. ( ClWWalks ` G ) /\ ( # ` B ) = N ) )
3		biid	|- ( ( A ` 0 ) = ( B ` 0 ) <-> ( A ` 0 ) = ( B ` 0 ) )
4		simpl	|- ( ( A e. ( ClWWalks ` G ) /\ ( # ` A ) = M ) -> A e. ( ClWWalks ` G ) )
5		simpl	|- ( ( B e. ( ClWWalks ` G ) /\ ( # ` B ) = N ) -> B e. ( ClWWalks ` G ) )
6		id	|- ( ( A ` 0 ) = ( B ` 0 ) -> ( A ` 0 ) = ( B ` 0 ) )
7		clwwlkccat	|- ( ( A e. ( ClWWalks ` G ) /\ B e. ( ClWWalks ` G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ClWWalks ` G ) )
8	4 5 6 7	syl3an	|- ( ( ( A e. ( ClWWalks ` G ) /\ ( # ` A ) = M ) /\ ( B e. ( ClWWalks ` G ) /\ ( # ` B ) = N ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ClWWalks ` G ) )
9	1 2 3 8	syl3anb	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ClWWalks ` G ) )
10		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
11	10	clwwlknwrd	|- ( A e. ( M ClWWalksN G ) -> A e. Word ( Vtx ` G ) )
12	10	clwwlknwrd	|- ( B e. ( N ClWWalksN G ) -> B e. Word ( Vtx ` G ) )
13		ccatlen	|- ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
14	11 12 13	syl2an	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
15		clwwlknlen	|- ( A e. ( M ClWWalksN G ) -> ( # ` A ) = M )
16		clwwlknlen	|- ( B e. ( N ClWWalksN G ) -> ( # ` B ) = N )
17	15 16	oveqan12d	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) ) -> ( ( # ` A ) + ( # ` B ) ) = ( M + N ) )
18	14 17	eqtrd	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) ) -> ( # ` ( A ++ B ) ) = ( M + N ) )
19	18	3adant3	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( # ` ( A ++ B ) ) = ( M + N ) )
20		isclwwlkn	|- ( ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) <-> ( ( A ++ B ) e. ( ClWWalks ` G ) /\ ( # ` ( A ++ B ) ) = ( M + N ) ) )
21	9 19 20	sylanbrc	|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) )