numclwlk1lem1

Description: Lemma 1 for numclwlk1 (Statement 9 in Huneke p. 2 for n=2): "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)". (Contributed by AV, 23-May-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	numclwlk1lem1	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \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		3anass	$⊢ (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X) \leftrightarrow (\|1^{st} (w)\| = 2 \land (2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X))$
5		anidm	$⊢ (2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X) \leftrightarrow 2^{nd} (w) (0) = X$
6	5	anbi2i	$⊢ (\|1^{st} (w)\| = 2 \land (2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)) \leftrightarrow (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)$
7	4 6	bitri	$⊢ (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X) \leftrightarrow (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)$
8	7	rabbii	$⊢ \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\} = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\}$
9	8	fveq2i	$⊢ \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\| = \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\}\|$
10		simpl	$⊢ (V \in Fin \land G RegUSGraph K) \to V \in Fin$
11		simpr	$⊢ (V \in Fin \land G RegUSGraph K) \to G RegUSGraph K$
12		simpl	$⊢ (X \in V \land N = 2) \to X \in V$
13	1	clwlknon2num	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\}\| = K$
14	10 11 12 13	syl2an3an	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\}\| = K$
15	9 14	syl5eq	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\| = K$
16		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
17	16	anim2i	$⊢ (V \in Fin \land G RegUSGraph K) \to (V \in Fin \land G \in USGraph)$
18	17	ancomd	$⊢ (V \in Fin \land G RegUSGraph K) \to (G \in USGraph \land V \in Fin)$
19	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
20	18 19	sylibr	$⊢ (V \in Fin \land G RegUSGraph K) \to G \in FinUSGraph$
21		ne0i	$⊢ X \in V \to V \neq \emptyset$
22	21	adantr	$⊢ (X \in V \land N = 2) \to V \neq \emptyset$
23	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
24	20 11 22 23	syl2an3an	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to K \in ℕ_{0}$
25	24	nn0red	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to K \in ℝ$
26		ax-1rid	$⊢ K \in ℝ \to K \cdot 1 = K$
27	25 26	syl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to K \cdot 1 = K$
28	1	wlkl0	$⊢ X \in V \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\} = \{⟨\emptyset, \{⟨0, X⟩\}⟩\}$
29	28	ad2antrl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\} = \{⟨\emptyset, \{⟨0, X⟩\}⟩\}$
30	29	fveq2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\| = \|\{⟨\emptyset, \{⟨0, X⟩\}⟩\}\|$
31		opex	$⊢ ⟨\emptyset, \{⟨0, X⟩\}⟩ \in V$
32		hashsng	$⊢ ⟨\emptyset, \{⟨0, X⟩\}⟩ \in V \to \|\{⟨\emptyset, \{⟨0, X⟩\}⟩\}\| = 1$
33	31 32	ax-mp	$⊢ \|\{⟨\emptyset, \{⟨0, X⟩\}⟩\}\| = 1$
34	30 33	syl6req	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to 1 = \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|$
35	34	oveq2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to K \cdot 1 = K \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|$
36	15 27 35	3eqtr2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\| = K \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|$
37		eqeq2	$⊢ N = 2 \to (\|1^{st} (w)\| = N \leftrightarrow \|1^{st} (w)\| = 2)$
38		oveq1	$⊢ N = 2 \to N - 2 = 2 - 2$
39		2cn	$⊢ 2 \in ℂ$
40	39	subidi	$⊢ 2 - 2 = 0$
41	38 40	syl6eq	$⊢ N = 2 \to N - 2 = 0$
42	41	fveqeq2d	$⊢ N = 2 \to (2^{nd} (w) (N - 2) = X \leftrightarrow 2^{nd} (w) (0) = X)$
43	37 42	3anbi13d	$⊢ N = 2 \to ((\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X) \leftrightarrow (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X))$
44	43	rabbidv	$⊢ N = 2 \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\} = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}$
45	2 44	syl5eq	$⊢ N = 2 \to C = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}$
46	45	fveq2d	$⊢ N = 2 \to \|C\| = \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\|$
47	41	eqeq2d	$⊢ N = 2 \to (\|1^{st} (w)\| = N - 2 \leftrightarrow \|1^{st} (w)\| = 0)$
48	47	anbi1d	$⊢ N = 2 \to ((\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X) \leftrightarrow (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X))$
49	48	rabbidv	$⊢ N = 2 \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N - 2 \land 2^{nd} (w) (0) = X)\} = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}$
50	3 49	syl5eq	$⊢ N = 2 \to F = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}$
51	50	fveq2d	$⊢ N = 2 \to \|F\| = \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|$
52	51	oveq2d	$⊢ N = 2 \to K \|F\| = K \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|$
53	46 52	eqeq12d	$⊢ N = 2 \to (\|C\| = K \|F\| \leftrightarrow \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\| = K \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|)$
54	53	ad2antll	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to (\|C\| = K \|F\| \leftrightarrow \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (0) = X)\}\| = K \|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\}\|)$
55	36 54	mpbird	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N = 2)) \to \|C\| = K \|F\|$

Metamath Proof Explorer

Theorem numclwlk1lem1

Proof