numclwwlk2lem1lem

		Ref	Expression
	Assertion	numclwwlk2lem1lem	$⊢ (X \in Vtx (G) \land W \in (N WWalksN G) \land lastS (W) \neq W (0)) \to ((W ++ ⟨“ X ”⟩) (0) = W (0) \land (W ++ ⟨“ X ”⟩) (N) \neq W (0))$

Proof

Step	Hyp	Ref	Expression
1		wwlknbp1	$⊢ W \in (N WWalksN G) \to (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)$
2		simpl2	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to W \in Word Vtx (G)$
3		s1cl	$⊢ X \in Vtx (G) \to ⟨“ X ”⟩ \in Word Vtx (G)$
4	3	ad2antrl	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to ⟨“ X ”⟩ \in Word Vtx (G)$
5		nn0p1gt0	$⊢ N \in ℕ_{0} \to 0 < N + 1$
6	5	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to 0 < N + 1$
7	6	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to 0 < N + 1$
8		breq2	$⊢ \|W\| = N + 1 \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
9	8	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
10	9	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
11	7 10	mpbird	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to 0 < \|W\|$
12		ccatfv0	$⊢ (W \in Word Vtx (G) \land ⟨“ X ”⟩ \in Word Vtx (G) \land 0 < \|W\|) \to (W ++ ⟨“ X ”⟩) (0) = W (0)$
13	2 4 11 12	syl3anc	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to (W ++ ⟨“ X ”⟩) (0) = W (0)$
14		oveq1	$⊢ \|W\| = N + 1 \to \|W\| - 1 = N + 1 - 1$
15	14	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| - 1 = N + 1 - 1$
16		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
17		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
18	16 17	syl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
19	18	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N + 1 - 1 = N$
20	15 19	eqtr2d	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N = \|W\| - 1$
21	20	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to N = \|W\| - 1$
22	21	fveq2d	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (W ++ ⟨“ X ”⟩) (N) = (W ++ ⟨“ X ”⟩) (\|W\| - 1)$
23		simpl2	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to W \in Word Vtx (G)$
24	3	adantl	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to ⟨“ X ”⟩ \in Word Vtx (G)$
25	6	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to 0 < N + 1$
26	9	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
27	25 26	mpbird	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to 0 < \|W\|$
28		hashneq0	$⊢ W \in Word Vtx (G) \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
29	28	bicomd	$⊢ W \in Word Vtx (G) \to (W \neq \emptyset \leftrightarrow 0 < \|W\|)$
30	29	3ad2ant2	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (W \neq \emptyset \leftrightarrow 0 < \|W\|)$
31	30	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (W \neq \emptyset \leftrightarrow 0 < \|W\|)$
32	27 31	mpbird	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to W \neq \emptyset$
33		ccatval1lsw	$⊢ (W \in Word Vtx (G) \land ⟨“ X ”⟩ \in Word Vtx (G) \land W \neq \emptyset) \to (W ++ ⟨“ X ”⟩) (\|W\| - 1) = lastS (W)$
34	23 24 32 33	syl3anc	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (W ++ ⟨“ X ”⟩) (\|W\| - 1) = lastS (W)$
35	22 34	eqtr2d	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to lastS (W) = (W ++ ⟨“ X ”⟩) (N)$
36	35	neeq1d	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (lastS (W) \neq W (0) \leftrightarrow (W ++ ⟨“ X ”⟩) (N) \neq W (0))$
37	36	biimpd	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land X \in Vtx (G)) \to (lastS (W) \neq W (0) \to (W ++ ⟨“ X ”⟩) (N) \neq W (0))$
38	37	impr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to (W ++ ⟨“ X ”⟩) (N) \neq W (0)$
39	13 38	jca	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land (X \in Vtx (G) \land lastS (W) \neq W (0))) \to ((W ++ ⟨“ X ”⟩) (0) = W (0) \land (W ++ ⟨“ X ”⟩) (N) \neq W (0))$
40	39	exp32	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (X \in Vtx (G) \to (lastS (W) \neq W (0) \to ((W ++ ⟨“ X ”⟩) (0) = W (0) \land (W ++ ⟨“ X ”⟩) (N) \neq W (0))))$
41	1 40	syl	$⊢ W \in (N WWalksN G) \to (X \in Vtx (G) \to (lastS (W) \neq W (0) \to ((W ++ ⟨“ X ”⟩) (0) = W (0) \land (W ++ ⟨“ X ”⟩) (N) \neq W (0))))$
42	41	3imp21	$⊢ (X \in Vtx (G) \land W \in (N WWalksN G) \land lastS (W) \neq W (0)) \to ((W ++ ⟨“ X ”⟩) (0) = W (0) \land (W ++ ⟨“ X ”⟩) (N) \neq W (0))$

Metamath Proof Explorer

Theorem numclwwlk2lem1lem

Proof