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 e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
Assertion	2clwwlk2	|- ( X e. V -> ( X C 2 ) = ( X ( ClWWalksNOn ` G ) 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
2		2z	|- 2 e. ZZ
3		uzid	|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
4	2 3	ax-mp	|- 2 e. ( ZZ>= ` 2 )
5	1	2clwwlk	|- ( ( X e. V /\ 2 e. ( ZZ>= ` 2 ) ) -> ( X C 2 ) = { w e. ( X ( ClWWalksNOn ` G ) 2 ) | ( w ` ( 2 - 2 ) ) = X } )
6	4 5	mpan2	|- ( X e. V -> ( X C 2 ) = { w e. ( X ( ClWWalksNOn ` G ) 2 ) | ( w ` ( 2 - 2 ) ) = X } )
7		2cn	|- 2 e. CC
8	7	subidi	|- ( 2 - 2 ) = 0
9	8	fveq2i	|- ( w ` ( 2 - 2 ) ) = ( w ` 0 )
10		isclwwlknon	|- ( w e. ( X ( ClWWalksNOn ` G ) 2 ) <-> ( w e. ( 2 ClWWalksN G ) /\ ( w ` 0 ) = X ) )
11	10	simprbi	|- ( w e. ( X ( ClWWalksNOn ` G ) 2 ) -> ( w ` 0 ) = X )
12	9 11	syl5eq	|- ( w e. ( X ( ClWWalksNOn ` G ) 2 ) -> ( w ` ( 2 - 2 ) ) = X )
13	12	rabeqc	|- { w e. ( X ( ClWWalksNOn ` G ) 2 ) | ( w ` ( 2 - 2 ) ) = X } = ( X ( ClWWalksNOn ` G ) 2 )
14	6 13	eqtrdi	|- ( X e. V -> ( X C 2 ) = ( X ( ClWWalksNOn ` G ) 2 ) )