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 \in (X ClWWalksNOn (G) M) \land B \in (X ClWWalksNOn (G) N)) \to A ++ B \in (X ClWWalksNOn (G) (M + N))$

Proof

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

Metamath Proof Explorer

Theorem clwwlknonccat

Proof