Theorem 2clwwlk2

Description: The set ( X C 2 ) of double loops of length 2 on a vertex X is equal to the set of closed walks with length 2 on X . Considered as "double loops", the first of the two closed walks/loops is degenerated, i.e., has length 0. (Contributed by AV, 18-Feb-2022) (Revised by AV, 20-Apr-2022)

	Ref	Expression
Hypothesis	2clwwlk.c	$$⊢C=\left(v\in V,n\in {\mathbb{Z}}_{\ge 2}⟼\left\{w\in \left(v\mathrm{ClWWalksNOn}\left(G\right)n\right)|w\left(n-2\right)=v\right\}\right)$$
Assertion	2clwwlk2	$$⊢X\in V\to XC2=X\mathrm{ClWWalksNOn}\left(G\right)2$$

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	$$⊢C=\left(v\in V,n\in {\mathbb{Z}}_{\ge 2}⟼\left\{w\in \left(v\mathrm{ClWWalksNOn}\left(G\right)n\right)|w\left(n-2\right)=v\right\}\right)$$
2		2z	$$⊢2\in \mathbb{Z}$$
3		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
4	2 3	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
5	1	2clwwlk	$$⊢\left(X\in V\wedge 2\in {\mathbb{Z}}_{\ge 2}\right)\to XC2=\left\{w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)|w\left(2-2\right)=X\right\}$$
6	4 5	mpan2	$$⊢X\in V\to XC2=\left\{w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)|w\left(2-2\right)=X\right\}$$
7		2cn	$$⊢2\in ℂ$$
8	7	subidi	$$⊢2-2=0$$
9	8	fveq2i	$$⊢w\left(2-2\right)=w\left(0\right)$$
10		isclwwlknon	$$⊢w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)\leftrightarrow \left(w\in \left(2\mathrm{ClWWalksN}G\right)\wedge w\left(0\right)=X\right)$$
11	10	simprbi	$$⊢w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)\to w\left(0\right)=X$$
12	9 11	eqtrid	$$⊢w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)\to w\left(2-2\right)=X$$
13	12	rabeqc	$$⊢\left\{w\in \left(X\mathrm{ClWWalksNOn}\left(G\right)2\right)|w\left(2-2\right)=X\right\}=X\mathrm{ClWWalksNOn}\left(G\right)2$$
14	6 13	eqtrdi	$$⊢X\in V\to XC2=X\mathrm{ClWWalksNOn}\left(G\right)2$$