clwwlknclwwlkdifnum - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > clwwlknclwwlkdifnum		Structured version Visualization version GIF version

Theorem clwwlknclwwlkdifnum 41163

Description: In a k-regular graph, the size of the set of walks of length n starting with a fixed vertex and ending not at this vertex is the difference between k to the power of n and the size of the set of walks of length n starting with this vertex and ending at this vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.)

**Hypotheses**
Ref	Expression
clwwlknclwwlkdif.a	⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}
clwwlknclwwlkdif.b	⊢ 𝐵 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}
clwwlknclwwlkdifnum.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
clwwlknclwwlkdifnum	⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘𝐴) = ((𝐾↑𝑁) − (#‘𝐵)))

Distinct variable groups: 𝑤,𝐺 𝑤,𝐾 𝑤,𝑁 𝑤,𝑉 𝑤,𝑋 Allowed substitution hints: 𝐴(𝑤) 𝐵(𝑤)

**Proof of Theorem clwwlknclwwlkdifnum**
Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	. . . 4 ⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}
2		clwwlknclwwlkdif.b	. . . 4 ⊢ 𝐵 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}
3	1, 2	clwwlknclwwlkdifs 41162	. . 3 ⊢ 𝐴 = ({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)
4	3	fveq2i 6090	. 2 ⊢ (#‘𝐴) = (#‘({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵))
5		clwwlknclwwlkdifnum.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
6	5	eleq1i 2678	. . . . . . . 8 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
7	6	biimpi 204	. . . . . . 7 ⊢ (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
8	7	adantl 480	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → (Vtx‘𝐺) ∈ Fin)
9	8	adantr 479	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (Vtx‘𝐺) ∈ Fin)
10		wwlksnfi 41093	. . . . 5 ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalkSN 𝐺) ∈ Fin)
11		rabfi 8047	. . . . 5 ⊢ ((𝑁 WWalkSN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∈ Fin)
12	9, 10, 11	3syl 18	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∈ Fin)
13		simpr 475	. . . . . . 7 ⊢ ((( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → (𝑤‘0) = 𝑋)
14	13	a1i 11	. . . . . 6 ⊢ (𝑤 ∈ (𝑁 WWalkSN 𝐺) → ((( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → (𝑤‘0) = 𝑋))
15	14	ss2rabi 3646	. . . . 5 ⊢ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} ⊆ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}
16	2, 15	eqsstri 3597	. . . 4 ⊢ 𝐵 ⊆ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}
17		hashssdif 13015	. . . 4 ⊢ (({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∈ Fin ∧ 𝐵 ⊆ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) → (#‘({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)) = ((#‘{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) − (#‘𝐵)))
18	12, 16, 17	sylancl 692	. . 3 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)) = ((#‘{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) − (#‘𝐵)))
19		simpl 471	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 RegUSGraph 𝐾)
20	19	adantr 479	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝐺 RegUSGraph 𝐾)
21		simpr 475	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin)
22	21	adantr 479	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑉 ∈ Fin)
23		simpl 471	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝑉)
24	23	adantl 480	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑋 ∈ 𝑉)
25		nnnn0 11148	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
26	25	adantl 480	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
27	26	adantl 480	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
28	5	rusgrnumwwlkg 41160	. . . . 5 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (#‘{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) = (𝐾↑𝑁))
29	20, 22, 24, 27, 28	syl13anc 1319	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) = (𝐾↑𝑁))
30	29	oveq1d 6541	. . 3 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((#‘{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) − (#‘𝐵)) = ((𝐾↑𝑁) − (#‘𝐵)))
31	18, 30	eqtrd 2643	. 2 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)) = ((𝐾↑𝑁) − (#‘𝐵)))
32	4, 31	syl5eq 2655	1 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘𝐴) = ((𝐾↑𝑁) − (#‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 = wceq 1474 ∈ wcel 1976 ≠ wne 2779 {crab 2899 ∖ cdif 3536 ⊆ wss 3539 class class class wbr 4577 ‘cfv 5789 (class class class)co 6526 Fincfn 7818 0cc0 9792 − cmin 10117 ℕcn 10869 ℕ₀cn0 11141 ↑cexp 12679 #chash 12936 lastS clsw 13095 Vtxcvtx 40210 RegUSGraph crusgr 40737 WWalkSN cwwlksn 41010

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4711 ax-pow 4763 ax-pr 4827 ax-un 6824 ax-inf2 8398 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-pre-sup 9870

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-disj 4548 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4938 df-id 4942 df-po 4948 df-so 4949 df-fr 4986 df-se 4987 df-we 4988 df-xp 5033 df-rel 5034 df-cnv 5035 df-co 5036 df-dm 5037 df-rn 5038 df-res 5039 df-ima 5040 df-pred 5582 df-ord 5628 df-on 5629 df-lim 5630 df-suc 5631 df-iota 5753 df-fun 5791 df-fn 5792 df-f 5793 df-f1 5794 df-fo 5795 df-f1o 5796 df-fv 5797 df-isom 5798 df-riota 6488 df-ov 6529 df-oprab 6530 df-mpt2 6531 df-om 6935 df-1st 7036 df-2nd 7037 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-2o 7425 df-oadd 7428 df-er 7606 df-map 7723 df-pm 7724 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-sup 8208 df-oi 8275 df-card 8625 df-cda 8850 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-div 10536 df-nn 10870 df-2 10928 df-3 10929 df-n0 11142 df-z 11213 df-uz 11522 df-rp 11667 df-xadd 11781 df-fz 12155 df-fzo 12292 df-seq 12621 df-exp 12680 df-hash 12937 df-word 13102 df-lsw 13103 df-concat 13104 df-s1 13105 df-substr 13106 df-cj 13635 df-re 13636 df-im 13637 df-sqrt 13771 df-abs 13772 df-clim 14015 df-sum 14213 df-xnn0 40179 df-vtx 40212 df-iedg 40213 df-uhgr 40261 df-ushgr 40262 df-upgr 40289 df-umgr 40290 df-edga 40333 df-uspgr 40361 df-usgr 40362 df-fusgr 40517 df-nbgr 40535 df-vtxdg 40663 df-rgr 40738 df-rusgr 40739 df-wwlks 41014 df-wwlksn 41015

This theorem is referenced by: av-numclwwlkqhash 41511

W3C validator