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 eqtrdi ⊢ X ∈ V → X C 2 = X ClWWalksNOn ⁡ G 2