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 = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
Assertion 2clwwlk2 X V X C 2 = X ClWWalksNOn G 2

Proof

Step Hyp Ref Expression
1 2clwwlk.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
2 2z 2
3 uzid 2 2 2
4 2 3 ax-mp 2 2
5 1 2clwwlk X V 2 2 X C 2 = w X ClWWalksNOn G 2 | w 2 2 = X
6 4 5 mpan2 X V X C 2 = w X ClWWalksNOn G 2 | w 2 2 = X
7 2cn 2
8 7 subidi 2 2 = 0
9 8 fveq2i w 2 2 = w 0
10 isclwwlknon w X ClWWalksNOn G 2 w 2 ClWWalksN G w 0 = X
11 10 simprbi w X ClWWalksNOn G 2 w 0 = X
12 9 11 syl5eq w X ClWWalksNOn G 2 w 2 2 = X
13 12 rabeqc w X ClWWalksNOn G 2 | w 2 2 = X = X ClWWalksNOn G 2
14 6 13 syl6eq X V X C 2 = X ClWWalksNOn G 2