clwlknon2num

Description: There are k walks of length 2 on each vertex X in a k-regular simple graph. Variant of clwwlknon2num , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

		Ref	Expression
	Hypothesis	clwlknon2num.v	$⊢ V = Vtx (G)$
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		clwlknon2num.v	$⊢ V = Vtx (G)$
2		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
3		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
4	2 3	syl	$⊢ G RegUSGraph K \to G \in USHGraph$
5	4	3ad2ant2	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to G \in USHGraph$
6	1	eleq2i	$⊢ X \in V \leftrightarrow X \in Vtx (G)$
7	6	biimpi	$⊢ X \in V \to X \in Vtx (G)$
8	7	3ad2ant3	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to X \in Vtx (G)$
9		2nn	$⊢ 2 \in ℕ$
10	9	a1i	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to 2 \in ℕ$
11		clwwlknonclwlknonen	$⊢ (G \in USHGraph \land X \in Vtx (G) \land 2 \in ℕ) \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\} \approx (X ClWWalksNOn (G) 2)$
12	5 8 10 11	syl3anc	$⊢ (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)\} \approx (X ClWWalksNOn (G) 2)$
13	2	anim2i	$⊢ (V \in Fin \land G RegUSGraph K) \to (V \in Fin \land G \in USGraph)$
14	13	ancomd	$⊢ (V \in Fin \land G RegUSGraph K) \to (G \in USGraph \land V \in Fin)$
15	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
16	14 15	sylibr	$⊢ (V \in Fin \land G RegUSGraph K) \to G \in FinUSGraph$
17	16	3adant3	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to G \in FinUSGraph$
18		2nn0	$⊢ 2 \in ℕ_{0}$
19	18	a1i	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to 2 \in ℕ_{0}$
20		wlksnfi	$⊢ (G \in FinUSGraph \land 2 \in ℕ_{0}) \to \{w \in Walks (G) \| \|1^{st} (w)\| = 2\} \in Fin$
21	17 19 20	syl2anc	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to \{w \in Walks (G) \| \|1^{st} (w)\| = 2\} \in Fin$
22		clwlkswks	$⊢ ClWalks (G) \subseteq Walks (G)$
23	22	a1i	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to ClWalks (G) \subseteq Walks (G)$
24		simp2l	$⊢ ((V \in Fin \land G RegUSGraph K \land X \in V) \land (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X) \land w \in ClWalks (G)) \to \|1^{st} (w)\| = 2$
25	23 24	rabssrabd	$⊢ (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)\} \subseteq \{w \in Walks (G) \| \|1^{st} (w)\| = 2\}$
26	21 25	ssfid	$⊢ (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)\} \in Fin$
27	1	clwwlknonfin	$⊢ V \in Fin \to X ClWWalksNOn (G) 2 \in Fin$
28	27	3ad2ant1	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to X ClWWalksNOn (G) 2 \in Fin$
29		hashen	$⊢ (\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\} \in Fin \land X ClWWalksNOn (G) 2 \in Fin) \to (\|\{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\}\| = \|X ClWWalksNOn (G) 2\| \leftrightarrow \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\} \approx (X ClWWalksNOn (G) 2))$
30	26 28 29	syl2anc	$⊢ (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)\}\| = \|X ClWWalksNOn (G) 2\| \leftrightarrow \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 2 \land 2^{nd} (w) (0) = X)\} \approx (X ClWWalksNOn (G) 2))$
31	12 30	mpbird	$⊢ (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)\}\| = \|X ClWWalksNOn (G) 2\|$
32	7	anim2i	$⊢ (G RegUSGraph K \land X \in V) \to (G RegUSGraph K \land X \in Vtx (G))$
33	32	3adant1	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to (G RegUSGraph K \land X \in Vtx (G))$
34		clwwlknon2num	$⊢ (G RegUSGraph K \land X \in Vtx (G)) \to \|X ClWWalksNOn (G) 2\| = K$
35	33 34	syl	$⊢ (V \in Fin \land G RegUSGraph K \land X \in V) \to \|X ClWWalksNOn (G) 2\| = K$
36	31 35	eqtrd	$⊢ (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$

Metamath Proof Explorer

Theorem clwlknon2num

Proof