wwlksnredwwlkn0

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 26-Oct-2022)

		Ref	Expression
	Hypothesis	wwlksnredwwlkn.e	$⊢ E = Edg (G)$
	Assertion	wwlksnredwwlkn0	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W (0) = P \leftrightarrow \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E))$

Proof

Step	Hyp	Ref	Expression
1		wwlksnredwwlkn.e	$⊢ E = Edg (G)$
2	1	wwlksnredwwlkn	$⊢ N \in ℕ_{0} \to (W \in ((N + 1) WWalksN G) \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E))$
3	2	imp	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E)$
4		simpl	$⊢ (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to W prefix (N + 1) = y$
5	4	adantl	$⊢ (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \land (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E)) \to W prefix (N + 1) = y$
6		fveq1	$⊢ y = W prefix (N + 1) \to y (0) = (W prefix (N + 1)) (0)$
7	6	eqcoms	$⊢ W prefix (N + 1) = y \to y (0) = (W prefix (N + 1)) (0)$
8	7	adantr	$⊢ (W prefix (N + 1) = y \land ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G))) \to y (0) = (W prefix (N + 1)) (0)$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9 1	wwlknp	$⊢ W \in ((N + 1) WWalksN G) \to (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in E)$
11		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
12		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
13		nn0re	$⊢ N + 1 \in ℕ_{0} \to N + 1 \in ℝ$
14		lep1	$⊢ N + 1 \in ℝ \to N + 1 \leq N + 1 + 1$
15	12 13 14	3syl	$⊢ N \in ℕ_{0} \to N + 1 \leq N + 1 + 1$
16		peano2nn0	$⊢ N + 1 \in ℕ_{0} \to N + 1 + 1 \in ℕ_{0}$
17	16	nn0zd	$⊢ N + 1 \in ℕ_{0} \to N + 1 + 1 \in ℤ$
18		fznn	$⊢ N + 1 + 1 \in ℤ \to (N + 1 \in (1 \dots N + 1 + 1) \leftrightarrow (N + 1 \in ℕ \land N + 1 \leq N + 1 + 1))$
19	12 17 18	3syl	$⊢ N \in ℕ_{0} \to (N + 1 \in (1 \dots N + 1 + 1) \leftrightarrow (N + 1 \in ℕ \land N + 1 \leq N + 1 + 1))$
20	11 15 19	mpbir2and	$⊢ N \in ℕ_{0} \to N + 1 \in (1 \dots N + 1 + 1)$
21		oveq2	$⊢ \|W\| = N + 1 + 1 \to (1 \dots \|W\|) = (1 \dots N + 1 + 1)$
22	21	eleq2d	$⊢ \|W\| = N + 1 + 1 \to (N + 1 \in (1 \dots \|W\|) \leftrightarrow N + 1 \in (1 \dots N + 1 + 1))$
23	20 22	syl5ibr	$⊢ \|W\| = N + 1 + 1 \to (N \in ℕ_{0} \to N + 1 \in (1 \dots \|W\|))$
24	23	adantl	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to N + 1 \in (1 \dots \|W\|))$
25		simpl	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1) \to W \in Word Vtx (G)$
26	24 25	jctild	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1) \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|)))$
27	26	3adant3	$⊢ (W \in Word Vtx (G) \land \|W\| = N + 1 + 1 \land \forall i \in (0 ..^N + 1) \{W (i), W (i + 1)\} \in E) \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|)))$
28	10 27	syl	$⊢ W \in ((N + 1) WWalksN G) \to (N \in ℕ_{0} \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|)))$
29	28	impcom	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|))$
30	29	adantl	$⊢ (W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|))$
31	30	adantr	$⊢ ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|))$
32	31	adantl	$⊢ (W prefix (N + 1) = y \land ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G))) \to (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|))$
33		pfxfv0	$⊢ (W \in Word Vtx (G) \land N + 1 \in (1 \dots \|W\|)) \to (W prefix (N + 1)) (0) = W (0)$
34	32 33	syl	$⊢ (W prefix (N + 1) = y \land ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G))) \to (W prefix (N + 1)) (0) = W (0)$
35		simprll	$⊢ (W prefix (N + 1) = y \land ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G))) \to W (0) = P$
36	8 34 35	3eqtrd	$⊢ (W prefix (N + 1) = y \land ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G))) \to y (0) = P$
37	36	ex	$⊢ W prefix (N + 1) = y \to (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \to y (0) = P)$
38	37	adantr	$⊢ (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \to y (0) = P)$
39	38	impcom	$⊢ (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \land (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E)) \to y (0) = P$
40		simpr	$⊢ (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to \{lastS (y), lastS (W)\} \in E$
41	40	adantl	$⊢ (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \land (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E)) \to \{lastS (y), lastS (W)\} \in E$
42	5 39 41	3jca	$⊢ (((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \land (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E)) \to (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E)$
43	42	ex	$⊢ ((W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \land y \in (N WWalksN G)) \to ((W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E))$
44	43	reximdva	$⊢ (W (0) = P \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to (\exists y \in (N WWalksN G) (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E))$
45	44	ex	$⊢ W (0) = P \to ((N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (\exists y \in (N WWalksN G) (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E)))$
46	45	com13	$⊢ \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land \{lastS (y), lastS (W)\} \in E) \to ((N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W (0) = P \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E)))$
47	3 46	mpcom	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W (0) = P \to \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E))$
48	29 33	syl	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W prefix (N + 1)) (0) = W (0)$
49	48	eqcomd	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to W (0) = (W prefix (N + 1)) (0)$
50	49	adantl	$⊢ ((W prefix (N + 1) = y \land y (0) = P) \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to W (0) = (W prefix (N + 1)) (0)$
51		fveq1	$⊢ W prefix (N + 1) = y \to (W prefix (N + 1)) (0) = y (0)$
52	51	adantr	$⊢ (W prefix (N + 1) = y \land y (0) = P) \to (W prefix (N + 1)) (0) = y (0)$
53	52	adantr	$⊢ ((W prefix (N + 1) = y \land y (0) = P) \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to (W prefix (N + 1)) (0) = y (0)$
54		simpr	$⊢ (W prefix (N + 1) = y \land y (0) = P) \to y (0) = P$
55	54	adantr	$⊢ ((W prefix (N + 1) = y \land y (0) = P) \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to y (0) = P$
56	50 53 55	3eqtrd	$⊢ ((W prefix (N + 1) = y \land y (0) = P) \land (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G))) \to W (0) = P$
57	56	ex	$⊢ (W prefix (N + 1) = y \land y (0) = P) \to ((N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to W (0) = P)$
58	57	3adant3	$⊢ (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E) \to ((N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to W (0) = P)$
59	58	com12	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to ((W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E) \to W (0) = P)$
60	59	rexlimdvw	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (\exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E) \to W (0) = P)$
61	47 60	impbid	$⊢ (N \in ℕ_{0} \land W \in ((N + 1) WWalksN G)) \to (W (0) = P \leftrightarrow \exists y \in (N WWalksN G) (W prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (W)\} \in E))$

Metamath Proof Explorer

Theorem wwlksnredwwlkn0

Proof