clwwlknonex2e

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk on vertex X . (Contributed by AV, 17-Apr-2022)

	Ref	Expression
Hypotheses	clwwlknonex2.v	$⊢ V = Vtx (G)$
	clwwlknonex2.e	$⊢ E = Edg (G)$
Assertion	clwwlknonex2e	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X ClWWalksNOn (G) N)$

Proof

Step	Hyp	Ref	Expression
1		clwwlknonex2.v	$⊢ V = Vtx (G)$
2		clwwlknonex2.e	$⊢ E = Edg (G)$
3	1 2	clwwlknonex2	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G)$
4		isclwwlknon	$⊢ W \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow (W \in ((N - 2) ClWWalksN G) \land W (0) = X)$
5		isclwwlkn	$⊢ W \in ((N - 2) ClWWalksN G) \leftrightarrow (W \in ClWWalks (G) \land \|W\| = N - 2)$
6	1	clwwlkbp	$⊢ W \in ClWWalks (G) \to (G \in V \land W \in Word V \land W \neq \emptyset)$
7	6	simp2d	$⊢ W \in ClWWalks (G) \to W \in Word V$
8		clwwlkgt0	$⊢ W \in ClWWalks (G) \to 0 < \|W\|$
9	7 8	jca	$⊢ W \in ClWWalks (G) \to (W \in Word V \land 0 < \|W\|)$
10	9	adantr	$⊢ (W \in ClWWalks (G) \land \|W\| = N - 2) \to (W \in Word V \land 0 < \|W\|)$
11	5 10	sylbi	$⊢ W \in ((N - 2) ClWWalksN G) \to (W \in Word V \land 0 < \|W\|)$
12	11	ad2antrl	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land (W \in ((N - 2) ClWWalksN G) \land W (0) = X)) \to (W \in Word V \land 0 < \|W\|)$
13		ccat2s1fst	$⊢ (W \in Word V \land 0 < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = W (0)$
14	12 13	syl	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land (W \in ((N - 2) ClWWalksN G) \land W (0) = X)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = W (0)$
15		simprr	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land (W \in ((N - 2) ClWWalksN G) \land W (0) = X)) \to W (0) = X$
16	14 15	eqtrd	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land (W \in ((N - 2) ClWWalksN G) \land W (0) = X)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X$
17	16	ex	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to ((W \in ((N - 2) ClWWalksN G) \land W (0) = X) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X)$
18	4 17	syl5bi	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to (W \in (X ClWWalksNOn (G) (N - 2)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X)$
19	18	a1d	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to (\{X, Y\} \in E \to (W \in (X ClWWalksNOn (G) (N - 2)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X))$
20	19	3imp	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X$
21		isclwwlknon	$⊢ (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X ClWWalksNOn (G) N) \leftrightarrow ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = X)$
22	3 20 21	sylanbrc	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X ClWWalksNOn (G) N)$

Metamath Proof Explorer

Theorem clwwlknonex2e

Proof