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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	numclwlk1.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
	numclwlk1.f	⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
Assertion	numclwlk1lem1	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		numclwlk1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		numclwlk1.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
3		numclwlk1.f	⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
4		3anass	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) )
5		anidm	⊢ ( ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 )
6	5	anbi2i	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) )
7	4 6	bitri	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) )
8	7	rabbii	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
9	8	fveq2i	⊢ ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } )
10		simpl	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝑉 ∈ Fin )
11		simpr	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 RegUSGraph 𝐾 )
12		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) → 𝑋 ∈ 𝑉 )
13	1	clwlknon2num	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = 𝐾 )
14	10 11 12 13	syl2an3an	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = 𝐾 )
15	9 14	syl5eq	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = 𝐾 )
16		rusgrusgr	⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph )
17	16	anim2i	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph ) )
18	17	ancomd	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
19	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
20	18 19	sylibr	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph )
21		ne0i	⊢ ( 𝑋 ∈ 𝑉 → 𝑉 ≠ ∅ )
22	21	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) → 𝑉 ≠ ∅ )
23	1	frusgrnn0	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ₀ )
24	20 11 22 23	syl2an3an	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → 𝐾 ∈ ℕ₀ )
25	24	nn0red	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → 𝐾 ∈ ℝ )
26		ax-1rid	⊢ ( 𝐾 ∈ ℝ → ( 𝐾 · 1 ) = 𝐾 )
27	25 26	syl	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( 𝐾 · 1 ) = 𝐾 )
28	1	wlkl0	⊢ ( 𝑋 ∈ 𝑉 → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } )
29	28	ad2antrl	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } )
30	29	fveq2d	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( ♯ ‘ { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } ) )
31		opex	⊢ ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ∈ V
32		hashsng	⊢ ( ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ∈ V → ( ♯ ‘ { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } ) = 1 )
33	31 32	ax-mp	⊢ ( ♯ ‘ { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } ) = 1
34	30 33	eqtr2di	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → 1 = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) )
35	34	oveq2d	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( 𝐾 · 1 ) = ( 𝐾 · ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) ) )
36	15 27 35	3eqtr2d	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( 𝐾 · ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) ) )
37		eqeq2	⊢ ( 𝑁 = 2 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ) )
38		oveq1	⊢ ( 𝑁 = 2 → ( 𝑁 − 2 ) = ( 2 − 2 ) )
39		2cn	⊢ 2 ∈ ℂ
40	39	subidi	⊢ ( 2 − 2 ) = 0
41	38 40	eqtrdi	⊢ ( 𝑁 = 2 → ( 𝑁 − 2 ) = 0 )
42	41	fveqeq2d	⊢ ( 𝑁 = 2 → ( ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) )
43	37 42	3anbi13d	⊢ ( 𝑁 = 2 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) )
44	43	rabbidv	⊢ ( 𝑁 = 2 → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } )
45	2 44	syl5eq	⊢ ( 𝑁 = 2 → 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } )
46	45	fveq2d	⊢ ( 𝑁 = 2 → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) )
47	41	eqeq2d	⊢ ( 𝑁 = 2 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ) )
48	47	anbi1d	⊢ ( 𝑁 = 2 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) )
49	48	rabbidv	⊢ ( 𝑁 = 2 → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } )
50	3 49	syl5eq	⊢ ( 𝑁 = 2 → 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } )
51	50	fveq2d	⊢ ( 𝑁 = 2 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) )
52	51	oveq2d	⊢ ( 𝑁 = 2 → ( 𝐾 · ( ♯ ‘ 𝐹 ) ) = ( 𝐾 · ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) ) )
53	46 52	eqeq12d	⊢ ( 𝑁 = 2 → ( ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( 𝐾 · ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) ) ) )
54	53	ad2antll	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 2 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) = ( 𝐾 · ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } ) ) ) )
55	36 54	mpbird	⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )

Metamath Proof Explorer

Theorem numclwlk1lem1

Proof