MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  numclwlk1lem2 Structured version   Visualization version   GIF version

Theorem numclwlk1lem2 28307
Description: Lemma 2 for numclwlk1 28308 (Statement 9 in [Huneke] p. 2 for n>2). This theorem corresponds to numclwwlk1 28298, using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022.)
Hypotheses
Ref Expression
numclwlk1.v 𝑉 = (Vtx‘𝐺)
numclwlk1.c 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
numclwlk1.f 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)}
Assertion
Ref Expression
numclwlk1lem2 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘𝐶) = (𝐾 · (♯‘𝐹)))
Distinct variable groups:   𝑤,𝐺   𝑤,𝐾   𝑤,𝑁   𝑤,𝑉   𝑤,𝑋   𝑤,𝐶   𝑤,𝐹

Proof of Theorem numclwlk1lem2
Dummy variables 𝑛 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rusgrusgr 27506 . . . . . 6 (𝐺 RegUSGraph 𝐾𝐺 ∈ USGraph)
2 usgruspgr 27123 . . . . . 6 (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph)
31, 2syl 17 . . . . 5 (𝐺 RegUSGraph 𝐾𝐺 ∈ USPGraph)
43ad2antlr 727 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝐺 ∈ USPGraph)
5 simpl 486 . . . . 5 ((𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑋𝑉)
65adantl 485 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑋𝑉)
7 uzuzle23 12371 . . . . 5 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (ℤ‘2))
87ad2antll 729 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑁 ∈ (ℤ‘2))
9 numclwlk1.v . . . . 5 𝑉 = (Vtx‘𝐺)
10 numclwlk1.c . . . . 5 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)}
11 eqid 2738 . . . . 5 {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}
129, 10, 11dlwwlknondlwlknonen 28303 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘2)) → 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
134, 6, 8, 12syl3anc 1372 . . 3 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
141anim2i 620 . . . . . . . . 9 ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph))
1514ancomd 465 . . . . . . . 8 ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
169isfusgr 27260 . . . . . . . 8 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
1715, 16sylibr 237 . . . . . . 7 ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph)
18 eluzge3nn 12372 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ)
1918nnnn0d 12036 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ0)
2019adantl 485 . . . . . . 7 ((𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ ℕ0)
21 wlksnfi 27845 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = 𝑁} ∈ Fin)
2217, 20, 21syl2an 599 . . . . . 6 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = 𝑁} ∈ Fin)
23 clwlkswks 27717 . . . . . . . 8 (ClWalks‘𝐺) ⊆ (Walks‘𝐺)
2423a1i 11 . . . . . . 7 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (ClWalks‘𝐺) ⊆ (Walks‘𝐺))
25 simp21 1207 . . . . . . 7 ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st𝑤)) = 𝑁)
2624, 25rabssrabd 3972 . . . . . 6 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = 𝑁})
2722, 26ssfid 8819 . . . . 5 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = 𝑁 ∧ ((2nd𝑤)‘0) = 𝑋 ∧ ((2nd𝑤)‘(𝑁 − 2)) = 𝑋)} ∈ Fin)
2810, 27eqeltrid 2837 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝐶 ∈ Fin)
299clwwlknonfin 28031 . . . . . 6 (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin)
3029ad2antrr 726 . . . . 5 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin)
31 ssrab2 3969 . . . . . 6 {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ⊆ (𝑋(ClWWalksNOn‘𝐺)𝑁)
3231a1i 11 . . . . 5 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ⊆ (𝑋(ClWWalksNOn‘𝐺)𝑁))
3330, 32ssfid 8819 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin)
34 hashen 13799 . . . 4 ((𝐶 ∈ Fin ∧ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin) → ((♯‘𝐶) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) ↔ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}))
3528, 33, 34syl2anc 587 . . 3 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → ((♯‘𝐶) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) ↔ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}))
3613, 35mpbird 260 . 2 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘𝐶) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}))
37 eqidd 2739 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}))
38 oveq12 7179 . . . . . 6 ((𝑣 = 𝑋𝑛 = 𝑁) → (𝑣(ClWWalksNOn‘𝐺)𝑛) = (𝑋(ClWWalksNOn‘𝐺)𝑁))
39 fvoveq1 7193 . . . . . . . 8 (𝑛 = 𝑁 → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2)))
4039adantl 485 . . . . . . 7 ((𝑣 = 𝑋𝑛 = 𝑁) → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2)))
41 simpl 486 . . . . . . 7 ((𝑣 = 𝑋𝑛 = 𝑁) → 𝑣 = 𝑋)
4240, 41eqeq12d 2754 . . . . . 6 ((𝑣 = 𝑋𝑛 = 𝑁) → ((𝑤‘(𝑛 − 2)) = 𝑣 ↔ (𝑤‘(𝑁 − 2)) = 𝑋))
4338, 42rabeqbidv 3387 . . . . 5 ((𝑣 = 𝑋𝑛 = 𝑁) → {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
4443adantl 485 . . . 4 ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ (𝑣 = 𝑋𝑛 = 𝑁)) → {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
45 ovex 7203 . . . . . 6 (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ V
4645rabex 5200 . . . . 5 {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ V
4746a1i 11 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ V)
4837, 44, 6, 8, 47ovmpod 7317 . . 3 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋(𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
4948fveq2d 6678 . 2 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘(𝑋(𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}))
50 eqid 2738 . . . 4 (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
51 eqid 2738 . . . 4 (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))
529, 50, 51numclwwlk1 28298 . . 3 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘(𝑋(𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))))
53 numclwlk1.f . . . . . . 7 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)}
545, 9eleqtrdi 2843 . . . . . . . . 9 ((𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑋 ∈ (Vtx‘𝐺))
5554adantl 485 . . . . . . . 8 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝑋 ∈ (Vtx‘𝐺))
56 uz3m2nn 12373 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ)
5756ad2antll 729 . . . . . . . 8 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑁 − 2) ∈ ℕ)
58 clwwlknonclwlknonen 28300 . . . . . . . 8 ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
594, 55, 57, 58syl3anc 1372 . . . . . . 7 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
6053, 59eqbrtrid 5065 . . . . . 6 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
61 uznn0sub 12359 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) → (𝑁 − 2) ∈ ℕ0)
627, 61syl 17 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ0)
6362adantl 485 . . . . . . . . . 10 ((𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℕ0)
64 wlksnfi 27845 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ (𝑁 − 2) ∈ ℕ0) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = (𝑁 − 2)} ∈ Fin)
6517, 63, 64syl2an 599 . . . . . . . . 9 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = (𝑁 − 2)} ∈ Fin)
66 simp2l 1200 . . . . . . . . . 10 ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) ∧ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st𝑤)) = (𝑁 − 2))
6724, 66rabssrabd 3972 . . . . . . . . 9 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st𝑤)) = (𝑁 − 2)})
6865, 67ssfid 8819 . . . . . . . 8 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st𝑤)) = (𝑁 − 2) ∧ ((2nd𝑤)‘0) = 𝑋)} ∈ Fin)
6953, 68eqeltrid 2837 . . . . . . 7 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → 𝐹 ∈ Fin)
709clwwlknonfin 28031 . . . . . . . 8 (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin)
7170ad2antrr 726 . . . . . . 7 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin)
72 hashen 13799 . . . . . . 7 ((𝐹 ∈ Fin ∧ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) → ((♯‘𝐹) = (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ↔ 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))
7369, 71, 72syl2anc 587 . . . . . 6 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → ((♯‘𝐹) = (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ↔ 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))
7460, 73mpbird 260 . . . . 5 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘𝐹) = (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))
7574eqcomd 2744 . . . 4 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) = (♯‘𝐹))
7675oveq2d 7186 . . 3 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) = (𝐾 · (♯‘𝐹)))
7752, 76eqtrd 2773 . 2 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘(𝑋(𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘𝐹)))
7836, 49, 773eqtr2d 2779 1 (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋𝑉𝑁 ∈ (ℤ‘3))) → (♯‘𝐶) = (𝐾 · (♯‘𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2114  {crab 3057  Vcvv 3398  wss 3843   class class class wbr 5030  cfv 6339  (class class class)co 7170  cmpo 7172  1st c1st 7712  2nd c2nd 7713  cen 8552  Fincfn 8555  0cc0 10615   · cmul 10620  cmin 10948  cn 11716  2c2 11771  3c3 11772  0cn0 11976  cuz 12324  chash 13782  Vtxcvtx 26941  USPGraphcuspgr 27093  USGraphcusgr 27094  FinUSGraphcfusgr 27258   RegUSGraph crusgr 27498  Walkscwlks 27538  ClWalkscclwlks 27711  ClWWalksNOncclwwlknon 28024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ifp 1063  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-oadd 8135  df-er 8320  df-map 8439  df-pm 8440  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-dju 9403  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-nn 11717  df-2 11779  df-3 11780  df-n0 11977  df-xnn0 12049  df-z 12063  df-uz 12325  df-rp 12473  df-xadd 12591  df-fz 12982  df-fzo 13125  df-seq 13461  df-exp 13522  df-hash 13783  df-word 13956  df-lsw 14004  df-concat 14012  df-s1 14039  df-substr 14092  df-pfx 14122  df-s2 14299  df-vtx 26943  df-iedg 26944  df-edg 26993  df-uhgr 27003  df-ushgr 27004  df-upgr 27027  df-umgr 27028  df-uspgr 27095  df-usgr 27096  df-fusgr 27259  df-nbgr 27275  df-vtxdg 27408  df-rgr 27499  df-rusgr 27500  df-wlks 27541  df-clwlks 27712  df-wwlks 27768  df-wwlksn 27769  df-clwwlk 27919  df-clwwlkn 27962  df-clwwlknon 28025
This theorem is referenced by:  numclwlk1  28308
  Copyright terms: Public domain W3C validator