wspthsnwspthsnon

Description: A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-May-2021) (Revised by AV, 13-Mar-2022)

		Ref	Expression
	Hypothesis	wwlksnwwlksnon.v	$⊢ V = Vtx (G)$
	Assertion	wspthsnwspthsnon	$⊢ W \in (N WSPathsN G) \leftrightarrow \exists a \in V \exists b \in V W \in (a (N WSPathsNOn G) b)$

Proof

Step	Hyp	Ref	Expression
1		wwlksnwwlksnon.v	$⊢ V = Vtx (G)$
2		iswspthn	$⊢ W \in (N WSPathsN G) \leftrightarrow (W \in (N WWalksN G) \land \exists f f SPaths (G) W)$
3	1	wwlksnwwlksnon	$⊢ W \in (N WWalksN G) \leftrightarrow \exists a \in V \exists b \in V W \in (a (N WWalksNOn G) b)$
4	3	anbi1i	$⊢ (W \in (N WWalksN G) \land \exists f f SPaths (G) W) \leftrightarrow (\exists a \in V \exists b \in V W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W)$
5		r19.41vv	$⊢ \exists a \in V \exists b \in V (W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W) \leftrightarrow (\exists a \in V \exists b \in V W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W)$
6	4 5	bitr4i	$⊢ (W \in (N WWalksN G) \land \exists f f SPaths (G) W) \leftrightarrow \exists a \in V \exists b \in V (W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W)$
7		3anass	$⊢ (f SPaths (G) W \land W (0) = a \land W (\|f\|) = b) \leftrightarrow (f SPaths (G) W \land (W (0) = a \land W (\|f\|) = b))$
8	7	a1i	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to ((f SPaths (G) W \land W (0) = a \land W (\|f\|) = b) \leftrightarrow (f SPaths (G) W \land (W (0) = a \land W (\|f\|) = b)))$
9		vex	$⊢ f \in V$
10	1	isspthonpth	$⊢ ((a \in V \land b \in V) \land (f \in V \land W \in (a (N WWalksNOn G) b))) \to (f (a SPathsOn (G) b) W \leftrightarrow (f SPaths (G) W \land W (0) = a \land W (\|f\|) = b))$
11	9 10	mpanr1	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (f (a SPathsOn (G) b) W \leftrightarrow (f SPaths (G) W \land W (0) = a \land W (\|f\|) = b))$
12		spthiswlk	$⊢ f SPaths (G) W \to f Walks (G) W$
13		wlklenvm1	$⊢ f Walks (G) W \to \|f\| = \|W\| - 1$
14		wwlknon	$⊢ W \in (a (N WWalksNOn G) b) \leftrightarrow (W \in (N WWalksN G) \land W (0) = a \land W (N) = b)$
15		simpl2	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to W (0) = a$
16		simpr	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to \|f\| = \|W\| - 1$
17		wwlknbp1	$⊢ W \in (N WWalksN G) \to (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)$
18		oveq1	$⊢ \|W\| = N + 1 \to \|W\| - 1 = N + 1 - 1$
19	18	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| - 1 = N + 1 - 1$
20		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
21		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
22	20 21	syl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
23	22	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N + 1 - 1 = N$
24	19 23	eqtrd	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| - 1 = N$
25	17 24	syl	$⊢ W \in (N WWalksN G) \to \|W\| - 1 = N$
26	25	3ad2ant1	$⊢ (W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \to \|W\| - 1 = N$
27	26	adantr	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to \|W\| - 1 = N$
28	16 27	eqtrd	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to \|f\| = N$
29	28	fveq2d	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to W (\|f\|) = W (N)$
30		simpl3	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to W (N) = b$
31	29 30	eqtrd	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to W (\|f\|) = b$
32	15 31	jca	$⊢ ((W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \land \|f\| = \|W\| - 1) \to (W (0) = a \land W (\|f\|) = b)$
33	32	ex	$⊢ (W \in (N WWalksN G) \land W (0) = a \land W (N) = b) \to (\|f\| = \|W\| - 1 \to (W (0) = a \land W (\|f\|) = b))$
34	14 33	sylbi	$⊢ W \in (a (N WWalksNOn G) b) \to (\|f\| = \|W\| - 1 \to (W (0) = a \land W (\|f\|) = b))$
35	34	adantl	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (\|f\| = \|W\| - 1 \to (W (0) = a \land W (\|f\|) = b))$
36	35	com12	$⊢ \|f\| = \|W\| - 1 \to (((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (W (0) = a \land W (\|f\|) = b))$
37	12 13 36	3syl	$⊢ f SPaths (G) W \to (((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (W (0) = a \land W (\|f\|) = b))$
38	37	com12	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (f SPaths (G) W \to (W (0) = a \land W (\|f\|) = b))$
39	38	pm4.71d	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (f SPaths (G) W \leftrightarrow (f SPaths (G) W \land (W (0) = a \land W (\|f\|) = b)))$
40	8 11 39	3bitr4rd	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (f SPaths (G) W \leftrightarrow f (a SPathsOn (G) b) W)$
41	40	exbidv	$⊢ ((a \in V \land b \in V) \land W \in (a (N WWalksNOn G) b)) \to (\exists f f SPaths (G) W \leftrightarrow \exists f f (a SPathsOn (G) b) W)$
42	41	pm5.32da	$⊢ (a \in V \land b \in V) \to ((W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W) \leftrightarrow (W \in (a (N WWalksNOn G) b) \land \exists f f (a SPathsOn (G) b) W))$
43		wspthnon	$⊢ W \in (a (N WSPathsNOn G) b) \leftrightarrow (W \in (a (N WWalksNOn G) b) \land \exists f f (a SPathsOn (G) b) W)$
44	42 43	bitr4di	$⊢ (a \in V \land b \in V) \to ((W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W) \leftrightarrow W \in (a (N WSPathsNOn G) b))$
45	44	2rexbiia	$⊢ \exists a \in V \exists b \in V (W \in (a (N WWalksNOn G) b) \land \exists f f SPaths (G) W) \leftrightarrow \exists a \in V \exists b \in V W \in (a (N WSPathsNOn G) b)$
46	2 6 45	3bitri	$⊢ W \in (N WSPathsN G) \leftrightarrow \exists a \in V \exists b \in V W \in (a (N WSPathsNOn G) b)$

Metamath Proof Explorer

Theorem wspthsnwspthsnon

Proof