rusgrnumwwlks

Description: Induction step for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 27-May-2022)

	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	rusgrnumwwlks	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (P L N = K^{N} \to P L (N + 1) = K^{N + 1})$

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		simpr2	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to P \in V$
4		simpr3	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to N \in ℕ_{0}$
5	1 2	rusgrnumwwlklem	$⊢ (P \in V \land N \in ℕ_{0}) \to P L N = \|\{w \in (N WWalksN G) \| w (0) = P\}\|$
6	5	eqeq1d	$⊢ (P \in V \land N \in ℕ_{0}) \to (P L N = K^{N} \leftrightarrow \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N})$
7	3 4 6	syl2anc	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (P L N = K^{N} \leftrightarrow \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N})$
8		eqid	$⊢ Edg (G) = Edg (G)$
9	8	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 Edg (G)))$
10	9	ex	$⊢ N \in ℕ_{0} \to (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 Edg (G))))$
11	10	3ad2ant3	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to (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 Edg (G))))$
12	11	adantl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (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 Edg (G))))$
13	12	imp	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land 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 Edg (G)))$
14	13	rabbidva	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \{w \in ((N + 1) WWalksN G) \| w (0) = P\} = \{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
15	14	adantr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \{w \in ((N + 1) WWalksN G) \| w (0) = P\} = \{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
16	15	fveq2d	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\| = \|\{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
17		simp2	$⊢ (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)) \to y (0) = P$
18	17	pm4.71ri	$⊢ (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)) \leftrightarrow (y (0) = P \land (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)))$
19	18	a1i	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land w \in ((N + 1) WWalksN G)) \land y \in (N WWalksN G)) \to ((w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)) \leftrightarrow (y (0) = P \land (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))))$
20	19	rexbidva	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land 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 Edg (G)) \leftrightarrow \exists y \in (N WWalksN G) (y (0) = P \land (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))))$
21		fveq1	$⊢ x = y \to x (0) = y (0)$
22	21	eqeq1d	$⊢ x = y \to (x (0) = P \leftrightarrow y (0) = P)$
23	22	rexrab	$⊢ \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)) \leftrightarrow \exists y \in (N WWalksN G) (y (0) = P \land (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)))$
24	20 23	bitr4di	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land 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 Edg (G)) \leftrightarrow \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G)))$
25	24	rabbidva	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\} = \{w \in ((N + 1) WWalksN G) \| \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
26	25	adantr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\} = \{w \in ((N + 1) WWalksN G) \| \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
27	26	fveq2d	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \|\{w \in ((N + 1) WWalksN G) \| \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
28		simplr1	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to V \in Fin$
29	1	eleq1i	$⊢ V \in Fin \leftrightarrow Vtx (G) \in Fin$
30	29	biimpi	$⊢ V \in Fin \to Vtx (G) \in Fin$
31		eqid	$⊢ (N + 1) WWalksN G = (N + 1) WWalksN G$
32		eqid	$⊢ \{x \in (N WWalksN G) \| x (0) = P\} = \{x \in (N WWalksN G) \| x (0) = P\}$
33	31 8 32	hashwwlksnext	$⊢ Vtx (G) \in Fin \to \|\{w \in ((N + 1) WWalksN G) \| \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{x \in (N WWalksN G) \| x (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
34	28 30 33	3syl	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in ((N + 1) WWalksN G) \| \exists y \in \{x \in (N WWalksN G) \| x (0) = P\} (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{x \in (N WWalksN G) \| x (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
35		fveq1	$⊢ x = w \to x (0) = w (0)$
36	35	eqeq1d	$⊢ x = w \to (x (0) = P \leftrightarrow w (0) = P)$
37	36	cbvrabv	$⊢ \{x \in (N WWalksN G) \| x (0) = P\} = \{w \in (N WWalksN G) \| w (0) = P\}$
38	37	sumeq1i	$⊢ \sum_{y \in \{x \in (N WWalksN G) \| x (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
39	38	a1i	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \sum_{y \in \{x \in (N WWalksN G) \| x (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
40	27 34 39	3eqtrd	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in ((N + 1) WWalksN G) \| \exists y \in (N WWalksN G) (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
41		rusgrnumwwlkslem	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\} = \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
42	41	eqcomd	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\} = \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\}$
43	42	fveq2d	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
44	43	adantl	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land y \in \{w \in (N WWalksN G) \| w (0) = P\}) \to \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\}\|$
45		elrabi	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to y \in (N WWalksN G)$
46	45	adantl	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land y \in \{w \in (N WWalksN G) \| w (0) = P\}) \to y \in (N WWalksN G)$
47	1 8	wwlksnexthasheq	$⊢ y \in (N WWalksN G) \to \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\|$
48	46 47	syl	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land y \in \{w \in (N WWalksN G) \| w (0) = P\}) \to \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\|$
49	1	rusgrpropadjvtx	$⊢ G RegUSGraph K \to (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K)$
50		fveq1	$⊢ w = y \to w (0) = y (0)$
51	50	eqeq1d	$⊢ w = y \to (w (0) = P \leftrightarrow y (0) = P)$
52	51	elrab	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \leftrightarrow (y \in (N WWalksN G) \land y (0) = P)$
53	1 8	wwlknp	$⊢ y \in (N WWalksN G) \to (y \in Word V \land \|y\| = N + 1 \land \forall i \in (0 ..^N) \{y (i), y (i + 1)\} \in Edg (G))$
54	53	adantr	$⊢ (y \in (N WWalksN G) \land y (0) = P) \to (y \in Word V \land \|y\| = N + 1 \land \forall i \in (0 ..^N) \{y (i), y (i + 1)\} \in Edg (G))$
55		simpll	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to y \in Word V$
56		nn0p1gt0	$⊢ N \in ℕ_{0} \to 0 < N + 1$
57	56	3ad2ant3	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to 0 < N + 1$
58	57	adantl	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to 0 < N + 1$
59		breq2	$⊢ \|y\| = N + 1 \to (0 < \|y\| \leftrightarrow 0 < N + 1)$
60	59	ad2antlr	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (0 < \|y\| \leftrightarrow 0 < N + 1)$
61	58 60	mpbird	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to 0 < \|y\|$
62		hashle00	$⊢ y \in Word V \to (\|y\| \leq 0 \leftrightarrow y = \emptyset)$
63		lencl	$⊢ y \in Word V \to \|y\| \in ℕ_{0}$
64	63	nn0red	$⊢ y \in Word V \to \|y\| \in ℝ$
65		0re	$⊢ 0 \in ℝ$
66		lenlt	$⊢ (\|y\| \in ℝ \land 0 \in ℝ) \to (\|y\| \leq 0 \leftrightarrow \neg 0 < \|y\|)$
67	66	bicomd	$⊢ (\|y\| \in ℝ \land 0 \in ℝ) \to (\neg 0 < \|y\| \leftrightarrow \|y\| \leq 0)$
68	64 65 67	sylancl	$⊢ y \in Word V \to (\neg 0 < \|y\| \leftrightarrow \|y\| \leq 0)$
69		nne	$⊢ \neg y \neq \emptyset \leftrightarrow y = \emptyset$
70	69	a1i	$⊢ y \in Word V \to (\neg y \neq \emptyset \leftrightarrow y = \emptyset)$
71	62 68 70	3bitr4rd	$⊢ y \in Word V \to (\neg y \neq \emptyset \leftrightarrow \neg 0 < \|y\|)$
72	71	ad2antrr	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (\neg y \neq \emptyset \leftrightarrow \neg 0 < \|y\|)$
73	72	con4bid	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (y \neq \emptyset \leftrightarrow 0 < \|y\|)$
74	61 73	mpbird	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to y \neq \emptyset$
75	55 74	jca	$⊢ ((y \in Word V \land \|y\| = N + 1) \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (y \in Word V \land y \neq \emptyset)$
76	75	ex	$⊢ (y \in Word V \land \|y\| = N + 1) \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (y \in Word V \land y \neq \emptyset))$
77	76	3adant3	$⊢ (y \in Word V \land \|y\| = N + 1 \land \forall i \in (0 ..^N) \{y (i), y (i + 1)\} \in Edg (G)) \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (y \in Word V \land y \neq \emptyset))$
78	54 77	syl	$⊢ (y \in (N WWalksN G) \land y (0) = P) \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (y \in Word V \land y \neq \emptyset))$
79	52 78	sylbi	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (y \in Word V \land y \neq \emptyset))$
80	79	imp	$⊢ (y \in \{w \in (N WWalksN G) \| w (0) = P\} \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (y \in Word V \land y \neq \emptyset)$
81		lswcl	$⊢ (y \in Word V \land y \neq \emptyset) \to lastS (y) \in V$
82	80 81	syl	$⊢ (y \in \{w \in (N WWalksN G) \| w (0) = P\} \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to lastS (y) \in V$
83	82	ad2antrr	$⊢ (((y \in \{w \in (N WWalksN G) \| w (0) = P\} \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K) \to lastS (y) \in V$
84		preq1	$⊢ p = lastS (y) \to \{p, n\} = \{lastS (y), n\}$
85	84	eleq1d	$⊢ p = lastS (y) \to (\{p, n\} \in Edg (G) \leftrightarrow \{lastS (y), n\} \in Edg (G))$
86	85	rabbidv	$⊢ p = lastS (y) \to \{n \in V \| \{p, n\} \in Edg (G)\} = \{n \in V \| \{lastS (y), n\} \in Edg (G)\}$
87	86	fveqeq2d	$⊢ p = lastS (y) \to (\|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K \leftrightarrow \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K)$
88	87	rspcva	$⊢ (lastS (y) \in V \land \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K) \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K$
89	83 88	sylancom	$⊢ (((y \in \{w \in (N WWalksN G) \| w (0) = P\} \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K) \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K$
90	89	exp41	$⊢ y \in \{w \in (N WWalksN G) \| w (0) = P\} \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (\|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to (\forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K)))$
91	90	com14	$⊢ \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (\|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to (y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K)))$
92	91	3ad2ant3	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall p \in V \|\{n \in V \| \{p, n\} \in Edg (G)\}\| = K) \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (\|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to (y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K)))$
93	49 92	syl	$⊢ G RegUSGraph K \to ((V \in Fin \land P \in V \land N \in ℕ_{0}) \to (\|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to (y \in \{w \in (N WWalksN G) \| w (0) = P\} \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K)))$
94	93	imp41	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land y \in \{w \in (N WWalksN G) \| w (0) = P\}) \to \|\{n \in V \| \{lastS (y), n\} \in Edg (G)\}\| = K$
95	44 48 94	3eqtrd	$⊢ (((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \land y \in \{w \in (N WWalksN G) \| w (0) = P\}) \to \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = K$
96	95	sumeq2dv	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} K$
97		oveq1	$⊢ \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to \|\{w \in (N WWalksN G) \| w (0) = P\}\| K = K^{N} K$
98	97	adantl	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in (N WWalksN G) \| w (0) = P\}\| K = K^{N} K$
99		wwlksnfi	$⊢ Vtx (G) \in Fin \to N WWalksN G \in Fin$
100	29 99	sylbi	$⊢ V \in Fin \to N WWalksN G \in Fin$
101	100	3ad2ant1	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to N WWalksN G \in Fin$
102	101	ad2antlr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to N WWalksN G \in Fin$
103		rabfi	$⊢ N WWalksN G \in Fin \to \{w \in (N WWalksN G) \| w (0) = P\} \in Fin$
104	102 103	syl	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \{w \in (N WWalksN G) \| w (0) = P\} \in Fin$
105		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
106		simp1	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to V \in Fin$
107	105 106	anim12i	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (G \in USGraph \land V \in Fin)$
108	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
109	107 108	sylibr	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to G \in FinUSGraph$
110		simpl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to G RegUSGraph K$
111		ne0i	$⊢ P \in V \to V \neq \emptyset$
112	111	3ad2ant2	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to V \neq \emptyset$
113	112	adantl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to V \neq \emptyset$
114	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
115	109 110 113 114	syl3anc	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to K \in ℕ_{0}$
116	115	nn0cnd	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to K \in ℂ$
117	116	adantr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to K \in ℂ$
118		fsumconst	$⊢ (\{w \in (N WWalksN G) \| w (0) = P\} \in Fin \land K \in ℂ) \to \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} K = \|\{w \in (N WWalksN G) \| w (0) = P\}\| K$
119	104 117 118	syl2anc	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} K = \|\{w \in (N WWalksN G) \| w (0) = P\}\| K$
120	116 4	expp1d	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to K^{N + 1} = K^{N} K$
121	120	adantr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to K^{N + 1} = K^{N} K$
122	98 119 121	3eqtr4d	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} K = K^{N + 1}$
123	96 122	eqtrd	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \sum_{y \in \{w \in (N WWalksN G) \| w (0) = P\}} \|\{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = y \land y (0) = P \land \{lastS (y), lastS (w)\} \in Edg (G))\}\| = K^{N + 1}$
124	16 40 123	3eqtrd	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\| = K^{N + 1}$
125		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
126	125	3ad2ant3	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to N + 1 \in ℕ_{0}$
127	126	adantl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to N + 1 \in ℕ_{0}$
128	1 2	rusgrnumwwlklem	$⊢ (P \in V \land N + 1 \in ℕ_{0}) \to P L (N + 1) = \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\|$
129	128	eqeq1d	$⊢ (P \in V \land N + 1 \in ℕ_{0}) \to (P L (N + 1) = K^{N + 1} \leftrightarrow \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\| = K^{N + 1})$
130	3 127 129	syl2anc	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (P L (N + 1) = K^{N + 1} \leftrightarrow \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\| = K^{N + 1})$
131	130	adantr	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to (P L (N + 1) = K^{N + 1} \leftrightarrow \|\{w \in ((N + 1) WWalksN G) \| w (0) = P\}\| = K^{N + 1})$
132	124 131	mpbird	$⊢ ((G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \land \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}) \to P L (N + 1) = K^{N + 1}$
133	132	ex	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (\|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N} \to P L (N + 1) = K^{N + 1})$
134	7 133	sylbid	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (P L N = K^{N} \to P L (N + 1) = K^{N + 1})$

Metamath Proof Explorer

Theorem rusgrnumwwlks

Proof