numclwlk1lem2

Description: Lemma 2 for numclwlk1 (Statement 9 in Huneke p. 2 for n>2). This theorem corresponds to numclwwlk1 , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

	Ref	Expression
Hypotheses	numclwlk1.v	$⊢ V = Vtx (G)$
	numclwlk1.c	$⊢ C = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\}$
	numclwlk1.f	$⊢ F = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\}$
Assertion	numclwlk1lem2	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|C\| = K \|F\|$

Proof

Step	Hyp	Ref	Expression
1		numclwlk1.v	$⊢ V = Vtx (G)$
2		numclwlk1.c	$⊢ C = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\}$
3		numclwlk1.f	$⊢ F = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\}$
4		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
5		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
6	4 5	syl	$⊢ G RegUSGraph K \to G \in USHGraph$
7	6	ad2antlr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to G \in USHGraph$
8		simpl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to X \in V$
9	8	adantl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X \in V$
10		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
11	10	ad2antll	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to N \in ℤ_{\geq 2}$
12		eqid	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
13	1 2 12	dlwwlknondlwlknonen	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to C \approx \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
14	7 9 11 13	syl3anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to C \approx \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
15	4	anim2i	$⊢ (V \in Fin \land G RegUSGraph K) \to (V \in Fin \land G \in USGraph)$
16	15	ancomd	$⊢ (V \in Fin \land G RegUSGraph K) \to (G \in USGraph \land V \in Fin)$
17	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
18	16 17	sylibr	$⊢ (V \in Fin \land G RegUSGraph K) \to G \in FinUSGraph$
19		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
20	19	nnnn0d	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ_{0}$
21	20	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N \in ℕ_{0}$
22		wlksnfi	$⊢ (G \in FinUSGraph \land N \in ℕ_{0}) \to \{w \in Walks (G) \| \|1^{st} (w)\| = N\} \in Fin$
23	18 21 22	syl2an	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in Walks (G) \| \|1^{st} (w)\| = N\} \in Fin$
24		clwlkswks	$⊢ ClWalks (G) \subseteq Walks (G)$
25	24	a1i	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to ClWalks (G) \subseteq Walks (G)$
26		simp21	$⊢ (((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \land (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X) \land w \in ClWalks (G)) \to \|1^{st} (w)\| = N$
27	25 26	rabssrabd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\} \subseteq \{w \in Walks (G) \| \|1^{st} (w)\| = N\}$
28	23 27	ssfid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\} \in Fin$
29	2 28	eqeltrid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to C \in Fin$
30	1	clwwlknonfin	$⊢ V \in Fin \to X ClWWalksNOn (G) N \in Fin$
31	30	ad2antrr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X ClWWalksNOn (G) N \in Fin$
32		ssrab2	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \subseteq X ClWWalksNOn (G) N$
33	32	a1i	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \subseteq X ClWWalksNOn (G) N$
34	31 33	ssfid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in Fin$
35		hashen	$⊢ (C \in Fin \land \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in Fin) \to (\|C\| = \|\{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}\| \leftrightarrow C \approx \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\})$
36	29 34 35	syl2anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to (\|C\| = \|\{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}\| \leftrightarrow C \approx \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\})$
37	14 36	mpbird	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|C\| = \|\{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}\|$
38		eqidd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
39		oveq12	$⊢ (v = X \land n = N) \to v ClWWalksNOn (G) n = X ClWWalksNOn (G) N$
40		fvoveq1	$⊢ n = N \to w (n - 2) = w (N - 2)$
41	40	adantl	$⊢ (v = X \land n = N) \to w (n - 2) = w (N - 2)$
42		simpl	$⊢ (v = X \land n = N) \to v = X$
43	41 42	eqeq12d	$⊢ (v = X \land n = N) \to (w (n - 2) = v \leftrightarrow w (N - 2) = X)$
44	39 43	rabeqbidv	$⊢ (v = X \land n = N) \to \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\} = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
45	44	adantl	$⊢ (((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \land (v = X \land n = N)) \to \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\} = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
46		ovex	$⊢ X ClWWalksNOn (G) N \in V$
47	46	rabex	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in V$
48	47	a1i	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in V$
49	38 45 9 11 48	ovmpod	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
50	49	fveq2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = \|\{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}\|$
51		eqid	$⊢ (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
52		eqid	$⊢ X ClWWalksNOn (G) (N - 2) = X ClWWalksNOn (G) (N - 2)$
53	1 51 52	numclwwlk1	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = K \|X ClWWalksNOn (G) (N - 2)\|$
54	8 1	eleqtrdi	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to X \in Vtx (G)$
55	54	adantl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X \in Vtx (G)$
56		uz3m2nn	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ$
57	56	ad2antll	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 2 \in ℕ$
58		clwwlknonclwlknonen	$⊢ (G \in USHGraph \land X \in Vtx (G) \land N - 2 \in ℕ) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\} \approx (X ClWWalksNOn (G) (N - 2))$
59	7 55 57 58	syl3anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\} \approx (X ClWWalksNOn (G) (N - 2))$
60	3 59	eqbrtrid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to F \approx (X ClWWalksNOn (G) (N - 2))$
61		uznn0sub	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in ℕ_{0}$
62	10 61	syl	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ_{0}$
63	62	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N - 2 \in ℕ_{0}$
64		wlksnfi	$⊢ (G \in FinUSGraph \land N - 2 \in ℕ_{0}) \to \{w \in Walks (G) \| \|1^{st} (w)\| = N - 2\} \in Fin$
65	18 63 64	syl2an	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in Walks (G) \| \|1^{st} (w)\| = N - 2\} \in Fin$
66		simp2l	$⊢ (((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \land (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X) \land w \in ClWalks (G)) \to \|1^{st} (w)\| = N - 2$
67	25 66	rabssrabd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\} \subseteq \{w \in Walks (G) \| \|1^{st} (w)\| = N - 2\}$
68	65 67	ssfid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\} \in Fin$
69	3 68	eqeltrid	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to F \in Fin$
70	1	clwwlknonfin	$⊢ V \in Fin \to X ClWWalksNOn (G) (N - 2) \in Fin$
71	70	ad2antrr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X ClWWalksNOn (G) (N - 2) \in Fin$
72		hashen	$⊢ (F \in Fin \land X ClWWalksNOn (G) (N - 2) \in Fin) \to (\|F\| = \|X ClWWalksNOn (G) (N - 2)\| \leftrightarrow F \approx (X ClWWalksNOn (G) (N - 2)))$
73	69 71 72	syl2anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to (\|F\| = \|X ClWWalksNOn (G) (N - 2)\| \leftrightarrow F \approx (X ClWWalksNOn (G) (N - 2)))$
74	60 73	mpbird	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F\| = \|X ClWWalksNOn (G) (N - 2)\|$
75	74	eqcomd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) (N - 2)\| = \|F\|$
76	75	oveq2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to K \|X ClWWalksNOn (G) (N - 2)\| = K \|F\|$
77	53 76	eqtrd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = K \|F\|$
78	37 50 77	3eqtr2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|C\| = K \|F\|$

Metamath Proof Explorer

Theorem numclwlk1lem2

Proof