2clwwlk2clwwlk

Description: An element of the value of operation C , i.e., a word being a double loop of length N on vertex X , is composed of two closed walks. (Contributed by AV, 28-Apr-2022) (Proof shortened by AV, 3-Nov-2022)

		Ref	Expression
	Hypothesis	2clwwlk.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	Assertion	2clwwlk2clwwlk	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X C N) \leftrightarrow \exists a \in (X ClWWalksNOn (G) (N - 2)) \exists b \in (X ClWWalksNOn (G) 2) W = a ++ b)$

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
2		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
3	1	2clwwlkel	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (W \in (X C N) \leftrightarrow (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X))$
4	2 3	sylan2	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X C N) \leftrightarrow (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X))$
5		simpr	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N \in ℤ_{\geq 3}$
6	5	anim1i	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to (N \in ℤ_{\geq 3} \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X))$
7		3anass	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X) \leftrightarrow (N \in ℤ_{\geq 3} \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X))$
8	6 7	sylibr	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)$
9		clwwnonrepclwwnon	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X) \to W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2))$
10	8 9	syl	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2))$
11	5	adantr	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to N \in ℤ_{\geq 3}$
12		simprl	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W \in (X ClWWalksNOn (G) N)$
13		simprr	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W (N - 2) = X$
14		isclwwlknon	$⊢ W \in (X ClWWalksNOn (G) N) \leftrightarrow (W \in (N ClWWalksN G) \land W (0) = X)$
15		simpr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to W (0) = X$
16	15	eqcomd	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to X = W (0)$
17	14 16	sylbi	$⊢ W \in (X ClWWalksNOn (G) N) \to X = W (0)$
18	17	ad2antrl	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to X = W (0)$
19	13 18	eqtrd	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W (N - 2) = W (0)$
20		2clwwlk2clwwlklem	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2)$
21	11 12 19 20	syl3anc	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2)$
22		eqid	$⊢ Vtx (G) = Vtx (G)$
23	22	clwwlknbp	$⊢ W \in (N ClWWalksN G) \to (W \in Word Vtx (G) \land \|W\| = N)$
24		opeq2	$⊢ N = \|W\| \to ⟨N - 2, N⟩ = ⟨N - 2, \|W\|⟩$
25	24	oveq2d	$⊢ N = \|W\| \to W substr ⟨N - 2, N⟩ = W substr ⟨N - 2, \|W\|⟩$
26	25	oveq2d	$⊢ N = \|W\| \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = (W prefix (N - 2)) ++ (W substr ⟨N - 2, \|W\|⟩)$
27	26	eqcoms	$⊢ \|W\| = N \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = (W prefix (N - 2)) ++ (W substr ⟨N - 2, \|W\|⟩)$
28	27	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = (W prefix (N - 2)) ++ (W substr ⟨N - 2, \|W\|⟩)$
29		simpl	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to W \in Word Vtx (G)$
30		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
31		ige3m2fz	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in (1 \dots N)$
32	30 31	sselid	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in (0 \dots N)$
33	32	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N - 2 \in (0 \dots N)$
34	33	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 2 \in (0 \dots N)$
35		oveq2	$⊢ \|W\| = N \to (0 \dots \|W\|) = (0 \dots N)$
36	35	eleq2d	$⊢ \|W\| = N \to (N - 2 \in (0 \dots \|W\|) \leftrightarrow N - 2 \in (0 \dots N))$
37	36	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to (N - 2 \in (0 \dots \|W\|) \leftrightarrow N - 2 \in (0 \dots N))$
38	34 37	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 2 \in (0 \dots \|W\|)$
39		pfxcctswrd	$⊢ (W \in Word Vtx (G) \land N - 2 \in (0 \dots \|W\|)) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, \|W\|⟩) = W$
40	29 38 39	syl2an2r	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, \|W\|⟩) = W$
41	28 40	eqtrd	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (X \in V \land N \in ℤ_{\geq 3})) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W$
42	23 41	sylan	$⊢ (W \in (N ClWWalksN G) \land (X \in V \land N \in ℤ_{\geq 3})) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W$
43	42	ex	$⊢ W \in (N ClWWalksN G) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W)$
44	43	adantr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W)$
45	14 44	sylbi	$⊢ W \in (X ClWWalksNOn (G) N) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W)$
46	45	adantr	$⊢ (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W)$
47	46	impcom	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩) = W$
48	47	eqcomd	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to W = (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩)$
49	10 21 48	3jca	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X)) \to (W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \land W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2) \land W = (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩))$
50	49	ex	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to ((W \in (X ClWWalksNOn (G) N) \land W (N - 2) = X) \to (W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \land W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2) \land W = (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩)))$
51	4 50	sylbid	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X C N) \to (W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \land W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2) \land W = (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩)))$
52		rspceov	$⊢ (W prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \land W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2) \land W = (W prefix (N - 2)) ++ (W substr ⟨N - 2, N⟩)) \to \exists a \in (X ClWWalksNOn (G) (N - 2)) \exists b \in (X ClWWalksNOn (G) 2) W = a ++ b$
53	51 52	syl6	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X C N) \to \exists a \in (X ClWWalksNOn (G) (N - 2)) \exists b \in (X ClWWalksNOn (G) 2) W = a ++ b)$
54		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
55		2cnd	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℂ$
56	54 55	npcand	$⊢ N \in ℤ_{\geq 3} \to N - 2 + 2 = N$
57	56	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N - 2 + 2 = N$
58	57	oveq2d	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to X ClWWalksNOn (G) (N - 2 + 2) = X ClWWalksNOn (G) N$
59	58	eleq2d	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b \in (X ClWWalksNOn (G) (N - 2 + 2)) \leftrightarrow a ++ b \in (X ClWWalksNOn (G) N))$
60	59	biimpd	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b \in (X ClWWalksNOn (G) (N - 2 + 2)) \to a ++ b \in (X ClWWalksNOn (G) N))$
61		clwwlknonccat	$⊢ (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2)) \to a ++ b \in (X ClWWalksNOn (G) (N - 2 + 2))$
62	60 61	impel	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2))) \to a ++ b \in (X ClWWalksNOn (G) N)$
63		isclwwlknon	$⊢ b \in (X ClWWalksNOn (G) 2) \leftrightarrow (b \in (2 ClWWalksN G) \land b (0) = X)$
64		clwwlkn2	$⊢ b \in (2 ClWWalksN G) \leftrightarrow (\|b\| = 2 \land b \in Word Vtx (G) \land \{b (0), b (1)\} \in Edg (G))$
65		isclwwlknon	$⊢ a \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow (a \in ((N - 2) ClWWalksN G) \land a (0) = X)$
66	22	clwwlknbp	$⊢ a \in ((N - 2) ClWWalksN G) \to (a \in Word Vtx (G) \land \|a\| = N - 2)$
67		simpl	$⊢ (a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \to a \in Word Vtx (G)$
68		simprr	$⊢ (a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \to b \in Word Vtx (G)$
69		2nn	$⊢ 2 \in ℕ$
70		lbfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow 2 \in ℕ$
71	69 70	mpbir	$⊢ 0 \in (0 ..^2)$
72		oveq2	$⊢ \|b\| = 2 \to (0 ..^\|b\|) = (0 ..^2)$
73	71 72	eleqtrrid	$⊢ \|b\| = 2 \to 0 \in (0 ..^\|b\|)$
74	73	ad2antrl	$⊢ (a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \to 0 \in (0 ..^\|b\|)$
75	67 68 74	3jca	$⊢ (a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \to (a \in Word Vtx (G) \land b \in Word Vtx (G) \land 0 \in (0 ..^\|b\|))$
76	75	adantr	$⊢ ((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \to (a \in Word Vtx (G) \land b \in Word Vtx (G) \land 0 \in (0 ..^\|b\|))$
77	76	adantr	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to (a \in Word Vtx (G) \land b \in Word Vtx (G) \land 0 \in (0 ..^\|b\|))$
78		ccatval3	$⊢ (a \in Word Vtx (G) \land b \in Word Vtx (G) \land 0 \in (0 ..^\|b\|)) \to (a ++ b) (0 + \|a\|) = b (0)$
79	77 78	syl	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to (a ++ b) (0 + \|a\|) = b (0)$
80		simpr	$⊢ (b (0) = X \land \|a\| = N - 2) \to \|a\| = N - 2$
81	80	oveq2d	$⊢ (b (0) = X \land \|a\| = N - 2) \to 0 + \|a\| = 0 + N - 2$
82	81	adantl	$⊢ ((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \to 0 + \|a\| = 0 + N - 2$
83	54 55	subcld	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℂ$
84	83	addid2d	$⊢ N \in ℤ_{\geq 3} \to 0 + N - 2 = N - 2$
85	84	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to 0 + N - 2 = N - 2$
86	82 85	sylan9eq	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to 0 + \|a\| = N - 2$
87	86	eqcomd	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 2 = 0 + \|a\|$
88	87	fveq2d	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to (a ++ b) (N - 2) = (a ++ b) (0 + \|a\|)$
89		simpl	$⊢ (b (0) = X \land \|a\| = N - 2) \to b (0) = X$
90	89	eqcomd	$⊢ (b (0) = X \land \|a\| = N - 2) \to X = b (0)$
91	90	ad2antlr	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to X = b (0)$
92	79 88 91	3eqtr4d	$⊢ (((a \in Word Vtx (G) \land (\|b\| = 2 \land b \in Word Vtx (G))) \land (b (0) = X \land \|a\| = N - 2)) \land (X \in V \land N \in ℤ_{\geq 3})) \to (a ++ b) (N - 2) = X$
93	92	exp53	$⊢ a \in Word Vtx (G) \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to (b (0) = X \to (\|a\| = N - 2 \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X))))$
94	93	com24	$⊢ a \in Word Vtx (G) \to (\|a\| = N - 2 \to (b (0) = X \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X))))$
95	94	imp	$⊢ (a \in Word Vtx (G) \land \|a\| = N - 2) \to (b (0) = X \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
96	66 95	syl	$⊢ a \in ((N - 2) ClWWalksN G) \to (b (0) = X \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
97	96	adantr	$⊢ (a \in ((N - 2) ClWWalksN G) \land a (0) = X) \to (b (0) = X \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
98	65 97	sylbi	$⊢ a \in (X ClWWalksNOn (G) (N - 2)) \to (b (0) = X \to ((\|b\| = 2 \land b \in Word Vtx (G)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
99	98	com13	$⊢ (\|b\| = 2 \land b \in Word Vtx (G)) \to (b (0) = X \to (a \in (X ClWWalksNOn (G) (N - 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
100	99	3adant3	$⊢ (\|b\| = 2 \land b \in Word Vtx (G) \land \{b (0), b (1)\} \in Edg (G)) \to (b (0) = X \to (a \in (X ClWWalksNOn (G) (N - 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
101	64 100	sylbi	$⊢ b \in (2 ClWWalksN G) \to (b (0) = X \to (a \in (X ClWWalksNOn (G) (N - 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)))$
102	101	imp	$⊢ (b \in (2 ClWWalksN G) \land b (0) = X) \to (a \in (X ClWWalksNOn (G) (N - 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X))$
103	63 102	sylbi	$⊢ b \in (X ClWWalksNOn (G) 2) \to (a \in (X ClWWalksNOn (G) (N - 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X))$
104	103	impcom	$⊢ (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2)) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b) (N - 2) = X)$
105	104	impcom	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2))) \to (a ++ b) (N - 2) = X$
106	1	2clwwlkel	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (a ++ b \in (X C N) \leftrightarrow (a ++ b \in (X ClWWalksNOn (G) N) \land (a ++ b) (N - 2) = X))$
107	2 106	sylan2	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (a ++ b \in (X C N) \leftrightarrow (a ++ b \in (X ClWWalksNOn (G) N) \land (a ++ b) (N - 2) = X))$
108	107	adantr	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2))) \to (a ++ b \in (X C N) \leftrightarrow (a ++ b \in (X ClWWalksNOn (G) N) \land (a ++ b) (N - 2) = X))$
109	62 105 108	mpbir2and	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2))) \to a ++ b \in (X C N)$
110		eleq1	$⊢ W = a ++ b \to (W \in (X C N) \leftrightarrow a ++ b \in (X C N))$
111	109 110	syl5ibrcom	$⊢ ((X \in V \land N \in ℤ_{\geq 3}) \land (a \in (X ClWWalksNOn (G) (N - 2)) \land b \in (X ClWWalksNOn (G) 2))) \to (W = a ++ b \to W \in (X C N))$
112	111	rexlimdvva	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (\exists a \in (X ClWWalksNOn (G) (N - 2)) \exists b \in (X ClWWalksNOn (G) 2) W = a ++ b \to W \in (X C N))$
113	53 112	impbid	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X C N) \leftrightarrow \exists a \in (X ClWWalksNOn (G) (N - 2)) \exists b \in (X ClWWalksNOn (G) 2) W = a ++ b)$

Metamath Proof Explorer

Theorem 2clwwlk2clwwlk

Proof