# Metamath Proof Explorer

## 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 {ℤ}_{\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 {X}{C}2={X}\mathrm{ClWWalksNOn}\left({G}\right)2$

### Proof

Step Hyp Ref Expression
1 2clwwlk.c ${⊢}{C}=\left({v}\in {V},{n}\in {ℤ}_{\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 ℤ$
3 uzid ${⊢}2\in ℤ\to 2\in {ℤ}_{\ge 2}$
4 2 3 ax-mp ${⊢}2\in {ℤ}_{\ge 2}$
5 1 2clwwlk ${⊢}\left({X}\in {V}\wedge 2\in {ℤ}_{\ge 2}\right)\to {X}{C}2=\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 {X}{C}2=\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)↔\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 syl5eq ${⊢}{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 syl6eq ${⊢}{X}\in {V}\to {X}{C}2={X}\mathrm{ClWWalksNOn}\left({G}\right)2$