rusgr0edg

Description: Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	$⊢ V = Vtx (G)$
	rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
Assertion	rusgr0edg	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to P L N = 0$

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	$⊢ V = Vtx (G)$
2		rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
3		simp2	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to P \in V$
4		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
5	4	3ad2ant3	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to N \in ℕ_{0}$
6	1 2	rusgrnumwwlklem	$⊢ (P \in V \land N \in ℕ_{0}) \to P L N = \|\{w \in (N WWalksN G) \| w (0) = P\}\|$
7	3 5 6	syl2anc	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to P L N = \|\{w \in (N WWalksN G) \| w (0) = P\}\|$
8		rusgrusgr	$⊢ G RegUSGraph 0 \to G \in USGraph$
9		usgr0edg0rusgr	$⊢ G \in USGraph \to (G RegUSGraph 0 \leftrightarrow Edg (G) = \emptyset)$
10	9	biimpcd	$⊢ G RegUSGraph 0 \to (G \in USGraph \to Edg (G) = \emptyset)$
11	8 10	mpd	$⊢ G RegUSGraph 0 \to Edg (G) = \emptyset$
12		0enwwlksnge1	$⊢ (Edg (G) = \emptyset \land N \in ℕ) \to N WWalksN G = \emptyset$
13	11 12	sylan	$⊢ (G RegUSGraph 0 \land N \in ℕ) \to N WWalksN G = \emptyset$
14		eleq2	$⊢ N WWalksN G = \emptyset \to (w \in (N WWalksN G) \leftrightarrow w \in \emptyset)$
15		noel	$⊢ \neg w \in \emptyset$
16	15	pm2.21i	$⊢ w \in \emptyset \to \neg w (0) = P$
17	14 16	syl6bi	$⊢ N WWalksN G = \emptyset \to (w \in (N WWalksN G) \to \neg w (0) = P)$
18	13 17	syl	$⊢ (G RegUSGraph 0 \land N \in ℕ) \to (w \in (N WWalksN G) \to \neg w (0) = P)$
19	18	3adant2	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to (w \in (N WWalksN G) \to \neg w (0) = P)$
20	19	ralrimiv	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to \forall w \in (N WWalksN G) \neg w (0) = P$
21		rabeq0	$⊢ \{w \in (N WWalksN G) \| w (0) = P\} = \emptyset \leftrightarrow \forall w \in (N WWalksN G) \neg w (0) = P$
22	20 21	sylibr	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to \{w \in (N WWalksN G) \| w (0) = P\} = \emptyset$
23	22	fveq2d	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to \|\{w \in (N WWalksN G) \| w (0) = P\}\| = \|\emptyset\|$
24		hash0	$⊢ \|\emptyset\| = 0$
25	23 24	eqtrdi	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to \|\{w \in (N WWalksN G) \| w (0) = P\}\| = 0$
26	7 25	eqtrd	$⊢ (G RegUSGraph 0 \land P \in V \land N \in ℕ) \to P L N = 0$

Metamath Proof Explorer

Theorem rusgr0edg

Proof