Theorem 2clwwlk 30828

Description: Value of operation 𝐶, mapping a vertex v and an integer n greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v" according to definition 6 in [Huneke] p. 2. Such closed walks are "double loops" consisting of a closed (n-2)-walk v = v(0) ... v(n-2) = v and a closed 2-walk v = v(n-2) v(n-1) v(n) = v, see 2clwwlk2clwwlk 30831. (𝑋𝐶𝑁) is called the "set of double loops of length 𝑁 on vertex 𝑋 " in the following. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 20-Apr-2022.)

Hypothesis

Ref	Expression
2clwwlk.c	⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})

Assertion

Ref	Expression
2clwwlk	⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})

Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑛,𝑉,𝑣   𝑛,𝑋,𝑣,𝑤

Allowed substitution hints:   𝐶(𝑤, 𝑣, 𝑛)   𝑉(𝑤)

Proof of Theorem 2clwwlk

Step	Hyp	Ref	Expression
1		oveq12 7423	. . 3 ⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → (𝑣(ClWWalksNOn‘𝐺)𝑛) = (𝑋(ClWWalksNOn‘𝐺)𝑁))
2		fvoveq1 7437	. . . . 5 ⊢ (𝑛 = 𝑁 → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2)))
3	2	adantl 487	. . . 4 ⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2)))
4		simpl 488	. . . 4 ⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑋)
5	3, 4	eqeq12d 2776	. . 3 ⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → ((𝑤‘(𝑛 − 2)) = 𝑣 ↔ (𝑤‘(𝑁 − 2)) = 𝑋))
6	1, 5	rabeqbidv 3429	. 2 ⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
7		2clwwlk.c	. 2 ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
8		ovex 7447	. . 3 ⊢ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ V
9	8	rabex 5303	. 2 ⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ V
10	6, 7, 9	ovmpoa 7569	1 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3412  ‘cfv 6533  (class class class)co 7414   ∈ cmpo 7416   − cmin 11466  2c2 12320  ℤ_≥cuz 12888  ClWWalksNOncclwwlknon 30558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419

This theorem is used by:  2clwwlk2  30829  2clwwlkel  30830  extwwlkfab  30833  numclwwlk3lem2lem  30864  numclwwlk3lem2  30865