wwlksnextbi

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 16-Apr-2021) (Proof shortened by AV, 27-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnext.v	$⊢ V = Vtx (G)$
	wwlksnext.e	$⊢ E = Edg (G)$
Assertion	wwlksnextbi	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W \in ((N + 1) WWalksN G) \leftrightarrow T \in (N WWalksN G))$

Proof

Step	Hyp	Ref	Expression
1		wwlksnext.v	$⊢ V = Vtx (G)$
2		wwlksnext.e	$⊢ E = Edg (G)$
3	1 2	wwlknp	$⊢ W \in ((N + 1) WWalksN G) \to (W \in Word V \land \|W\| = N + 1 + 1 \land \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in E)$
4		wwlksnred	$⊢ N \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \to W prefix (N + 1) \in (N WWalksN G))$
5	4	ad2antrr	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W \in ((N + 1) WWalksN G) \to W prefix (N + 1) \in (N WWalksN G))$
6		fveqeq2	$⊢ W = T ++ ⟨“ S ”⟩ \to (\|W\| = N + 1 + 1 \leftrightarrow \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)$
7	6	3ad2ant2	$⊢ (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (\|W\| = N + 1 + 1 \leftrightarrow \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)$
8	7	adantl	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (\|W\| = N + 1 + 1 \leftrightarrow \|T ++ ⟨“ S ”⟩\| = N + 1 + 1)$
9		s1cl	$⊢ S \in V \to ⟨“ S ”⟩ \in Word V$
10	9	adantl	$⊢ (N \in ℕ_{0} \land S \in V) \to ⟨“ S ”⟩ \in Word V$
11	10	anim1ci	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (T \in Word V \land ⟨“ S ”⟩ \in Word V)$
12		ccatlen	$⊢ (T \in Word V \land ⟨“ S ”⟩ \in Word V) \to \|T ++ ⟨“ S ”⟩\| = \|T\| + \|⟨“ S ”⟩\|$
13	11 12	syl	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to \|T ++ ⟨“ S ”⟩\| = \|T\| + \|⟨“ S ”⟩\|$
14	13	eqeq1d	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T ++ ⟨“ S ”⟩\| = N + 1 + 1 \leftrightarrow \|T\| + \|⟨“ S ”⟩\| = N + 1 + 1)$
15		s1len	$⊢ \|⟨“ S ”⟩\| = 1$
16	15	a1i	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to \|⟨“ S ”⟩\| = 1$
17	16	oveq2d	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to \|T\| + \|⟨“ S ”⟩\| = \|T\| + 1$
18	17	eqeq1d	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T\| + \|⟨“ S ”⟩\| = N + 1 + 1 \leftrightarrow \|T\| + 1 = N + 1 + 1)$
19		lencl	$⊢ T \in Word V \to \|T\| \in ℕ_{0}$
20	19	nn0cnd	$⊢ T \in Word V \to \|T\| \in ℂ$
21	20	adantl	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to \|T\| \in ℂ$
22		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
23	22	nn0cnd	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
24	23	ad2antrr	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to N + 1 \in ℂ$
25		1cnd	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to 1 \in ℂ$
26	21 24 25	addcan2d	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T\| + 1 = N + 1 + 1 \leftrightarrow \|T\| = N + 1)$
27	14 18 26	3bitrd	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T ++ ⟨“ S ”⟩\| = N + 1 + 1 \leftrightarrow \|T\| = N + 1)$
28		oveq2	$⊢ N + 1 = \|T\| \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = (T ++ ⟨“ S ”⟩) prefix \|T\|$
29	28	eqcoms	$⊢ \|T\| = N + 1 \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = (T ++ ⟨“ S ”⟩) prefix \|T\|$
30		pfxccat1	$⊢ (T \in Word V \land ⟨“ S ”⟩ \in Word V) \to (T ++ ⟨“ S ”⟩) prefix \|T\| = T$
31	11 30	syl	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (T ++ ⟨“ S ”⟩) prefix \|T\| = T$
32	29 31	sylan9eqr	$⊢ (((N \in ℕ_{0} \land S \in V) \land T \in Word V) \land \|T\| = N + 1) \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T$
33	32	ex	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T\| = N + 1 \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
34	27 33	sylbid	$⊢ ((N \in ℕ_{0} \land S \in V) \land T \in Word V) \to (\|T ++ ⟨“ S ”⟩\| = N + 1 + 1 \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
35	34	3ad2antr1	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (\|T ++ ⟨“ S ”⟩\| = N + 1 + 1 \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
36	8 35	sylbid	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (\|W\| = N + 1 + 1 \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
37	36	imp	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \land \|W\| = N + 1 + 1) \to (T ++ ⟨“ S ”⟩) prefix (N + 1) = T$
38		oveq1	$⊢ W = T ++ ⟨“ S ”⟩ \to W prefix (N + 1) = (T ++ ⟨“ S ”⟩) prefix (N + 1)$
39	38	eqeq1d	$⊢ W = T ++ ⟨“ S ”⟩ \to (W prefix (N + 1) = T \leftrightarrow (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
40	39	3ad2ant2	$⊢ (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (W prefix (N + 1) = T \leftrightarrow (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
41	40	ad2antlr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \land \|W\| = N + 1 + 1) \to (W prefix (N + 1) = T \leftrightarrow (T ++ ⟨“ S ”⟩) prefix (N + 1) = T)$
42	37 41	mpbird	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \land \|W\| = N + 1 + 1) \to W prefix (N + 1) = T$
43	42	eleq1d	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \land \|W\| = N + 1 + 1) \to (W prefix (N + 1) \in (N WWalksN G) \leftrightarrow T \in (N WWalksN G))$
44	43	biimpd	$⊢ (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \land \|W\| = N + 1 + 1) \to (W prefix (N + 1) \in (N WWalksN G) \to T \in (N WWalksN G))$
45	44	ex	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (\|W\| = N + 1 + 1 \to (W prefix (N + 1) \in (N WWalksN G) \to T \in (N WWalksN G)))$
46	45	com23	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W prefix (N + 1) \in (N WWalksN G) \to (\|W\| = N + 1 + 1 \to T \in (N WWalksN G)))$
47	5 46	syld	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W \in ((N + 1) WWalksN G) \to (\|W\| = N + 1 + 1 \to T \in (N WWalksN G)))$
48	47	com13	$⊢ \|W\| = N + 1 + 1 \to (W \in ((N + 1) WWalksN G) \to (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to T \in (N WWalksN G)))$
49	48	3ad2ant2	$⊢ (W \in Word V \land \|W\| = N + 1 + 1 \land \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in E) \to (W \in ((N + 1) WWalksN G) \to (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to T \in (N WWalksN G)))$
50	3 49	mpcom	$⊢ W \in ((N + 1) WWalksN G) \to (((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to T \in (N WWalksN G))$
51	50	com12	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W \in ((N + 1) WWalksN G) \to T \in (N WWalksN G))$
52	1 2	wwlksnext	$⊢ (T \in (N WWalksN G) \land S \in V \land \{lastS (T), S\} \in E) \to T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G)$
53		eleq1	$⊢ W = T ++ ⟨“ S ”⟩ \to (W \in ((N + 1) WWalksN G) \leftrightarrow T ++ ⟨“ S ”⟩ \in ((N + 1) WWalksN G))$
54	52 53	syl5ibrcom	$⊢ (T \in (N WWalksN G) \land S \in V \land \{lastS (T), S\} \in E) \to (W = T ++ ⟨“ S ”⟩ \to W \in ((N + 1) WWalksN G))$
55	54	3exp	$⊢ T \in (N WWalksN G) \to (S \in V \to (\{lastS (T), S\} \in E \to (W = T ++ ⟨“ S ”⟩ \to W \in ((N + 1) WWalksN G))))$
56	55	com23	$⊢ T \in (N WWalksN G) \to (\{lastS (T), S\} \in E \to (S \in V \to (W = T ++ ⟨“ S ”⟩ \to W \in ((N + 1) WWalksN G))))$
57	56	com14	$⊢ W = T ++ ⟨“ S ”⟩ \to (\{lastS (T), S\} \in E \to (S \in V \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G))))$
58	57	imp	$⊢ (W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (S \in V \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G)))$
59	58	3adant1	$⊢ (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (S \in V \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G)))$
60	59	com12	$⊢ S \in V \to ((T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G)))$
61	60	adantl	$⊢ (N \in ℕ_{0} \land S \in V) \to ((T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E) \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G)))$
62	61	imp	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (T \in (N WWalksN G) \to W \in ((N + 1) WWalksN G))$
63	51 62	impbid	$⊢ ((N \in ℕ_{0} \land S \in V) \land (T \in Word V \land W = T ++ ⟨“ S ”⟩ \land \{lastS (T), S\} \in E)) \to (W \in ((N + 1) WWalksN G) \leftrightarrow T \in (N WWalksN G))$

Metamath Proof Explorer

Theorem wwlksnextbi

Proof