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	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
Assertion	2clwwlk2	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 2 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2clwwlk.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2		2z	⊢ 2 ∈ ℤ
3		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
4	2 3	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 2 )
5	1	2clwwlk	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 2 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐶 2 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∣ ( 𝑤 ‘ ( 2 − 2 ) ) = 𝑋 } )
6	4 5	mpan2	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 2 ) = { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∣ ( 𝑤 ‘ ( 2 − 2 ) ) = 𝑋 } )
7		2cn	⊢ 2 ∈ ℂ
8	7	subidi	⊢ ( 2 − 2 ) = 0
9	8	fveq2i	⊢ ( 𝑤 ‘ ( 2 − 2 ) ) = ( 𝑤 ‘ 0 )
10		isclwwlknon	⊢ ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ↔ ( 𝑤 ∈ ( 2 ClWWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
11	10	simprbi	⊢ ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) → ( 𝑤 ‘ 0 ) = 𝑋 )
12	9 11	syl5eq	⊢ ( 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) → ( 𝑤 ‘ ( 2 − 2 ) ) = 𝑋 )
13	12	rabeqc	⊢ { 𝑤 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∣ ( 𝑤 ‘ ( 2 − 2 ) ) = 𝑋 } = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 )
14	6 13	eqtrdi	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 2 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )