Theorem clwwlkn

Description: The set of closed walks of a fixed length N as words over the set of vertices in a graph G . (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

	Ref	Expression
Assertion	clwwlkn	$$⊢N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢g=G\to \mathrm{ClWWalks}\left(g\right)=\mathrm{ClWWalks}\left(G\right)$$
2	1	adantl	$$⊢\left(n=N\wedge g=G\right)\to \mathrm{ClWWalks}\left(g\right)=\mathrm{ClWWalks}\left(G\right)$$
3		eqeq2	$$⊢n=N\to \left(\left|w\right|=n\leftrightarrow \left|w\right|=N\right)$$
4	3	adantr	$$⊢\left(n=N\wedge g=G\right)\to \left(\left|w\right|=n\leftrightarrow \left|w\right|=N\right)$$
5	2 4	rabeqbidv	$$⊢\left(n=N\wedge g=G\right)\to \left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$
6		df-clwwlkn	$$⊢\mathrm{ClWWalksN}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left\{w\in \mathrm{ClWWalks}\left(g\right)|\left|w\right|=n\right\}\right)$$
7		fvex	$$⊢\mathrm{ClWWalks}\left(G\right)\in \mathrm{V}$$
8	7	rabex	$$⊢\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}\in \mathrm{V}$$
9	5 6 8	ovmpoa	$$⊢\left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$
10	6	mpondm0	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to N\mathrm{ClWWalksN}G=\varnothing$$
11		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
12	11	clwwlkbp	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to \left(G\in \mathrm{V}\wedge w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)\wedge w\ne \varnothing \right)$$
13	12	simp2d	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)$$
14		lencl	$$⊢w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)\to \left|w\right|\in {\mathbb{N}}_0$$
15	13 14	syl	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to \left|w\right|\in {\mathbb{N}}_0$$
16		eleq1	$$⊢\left|w\right|=N\to \left(\left|w\right|\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{N}}_0\right)$$
17	15 16	syl5ibcom	$$⊢w\in \mathrm{ClWWalks}\left(G\right)\to \left(\left|w\right|=N\to N\in {\mathbb{N}}_0\right)$$
18	17	con3rr3	$$⊢\neg N\in {\mathbb{N}}_0\to \left(w\in \mathrm{ClWWalks}\left(G\right)\to \neg \left|w\right|=N\right)$$
19	18	ralrimiv	$$⊢\neg N\in {\mathbb{N}}_0\to \forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=N$$
20		ral0	$$⊢\forall w\in \varnothing \neg \left|w\right|=N$$
21		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{ClWWalks}\left(G\right)=\varnothing$$
22	21	raleqdv	$$⊢\neg G\in \mathrm{V}\to \left(\forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=N\leftrightarrow \forall w\in \varnothing \neg \left|w\right|=N\right)$$
23	20 22	mpbiri	$$⊢\neg G\in \mathrm{V}\to \forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=N$$
24	19 23	jaoi	$$⊢\left(\neg N\in {\mathbb{N}}_0\vee \neg G\in \mathrm{V}\right)\to \forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=N$$
25		ianor	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\leftrightarrow \left(\neg N\in {\mathbb{N}}_0\vee \neg G\in \mathrm{V}\right)$$
26		rabeq0	$$⊢\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}=\varnothing \leftrightarrow \forall w\in \mathrm{ClWWalks}\left(G\right)\neg \left|w\right|=N$$
27	24 25 26	3imtr4i	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to \left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}=\varnothing$$
28	10 27	eqtr4d	$$⊢\neg \left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$
29	9 28	pm2.61i	$$⊢N\mathrm{ClWWalksN}G=\left\{w\in \mathrm{ClWWalks}\left(G\right)|\left|w\right|=N\right\}$$