Step | Hyp | Ref
| Expression |
1 | | numclwwlk6.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | finrusgrfusgr 26461 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph ) |
3 | 2 | 3adant2 1080 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph ) |
4 | | prmnn 15388 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈ ℕ) |
6 | | eqid 2622 |
. . . . 5
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
7 | 1, 6 | numclwwlk4 27244 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℕ) →
(#‘(𝑃 ClWWalksN 𝐺)) = Σ𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃))) |
8 | 3, 5, 7 | syl2an 494 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘(𝑃 ClWWalksN 𝐺)) = Σ𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃))) |
9 | 8 | oveq1d 6665 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑃 ClWWalksN 𝐺)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃)) |
10 | 5 | adantl 482 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ) |
11 | | simp3 1063 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin) |
12 | 11 | adantr 481 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑉 ∈ Fin) |
13 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑉 ∈ Fin) |
14 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
15 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → 𝑃 ∈ ℕ) |
16 | 6, 1 | numclwwlkffin 27214 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℕ) → (𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃) ∈ Fin) |
17 | 13, 14, 15, 16 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃) ∈ Fin) |
18 | | hashcl 13147 |
. . . . . . 7
⊢ ((𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃) ∈ Fin → (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) ∈
ℕ0) |
20 | 19 | nn0zd 11480 |
. . . . 5
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) ∈ ℤ) |
21 | 20 | ralrimiva 2966 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ∀𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) ∈ ℤ) |
22 | 10, 12, 21 | modfsummod 14526 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 ((#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) mod 𝑃)) |
23 | | simpl 473 |
. . . . . 6
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin)) |
24 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) |
25 | 24 | anim1i 592 |
. . . . . . . 8
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) ∧ 𝑥 ∈ 𝑉)) |
26 | 25 | ancomd 467 |
. . . . . . 7
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) |
27 | | 3anass 1042 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) ↔ (𝑥 ∈ 𝑉 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)))) |
28 | 26, 27 | sylibr 224 |
. . . . . 6
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) |
29 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
30 | 29 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑣 ↔ (𝑢‘0) = 𝑣)) |
31 | 30 | cbvrabv 3199 |
. . . . . . . . 9
⊢ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣} = {𝑢 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑢‘0) = 𝑣} |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑛 ∈ ℕ) → {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣} = {𝑢 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑢‘0) = 𝑣}) |
33 | 32 | mpt2eq3ia 6720 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑢 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑢‘0) = 𝑣}) |
34 | 1, 33 | numclwwlk5 27246 |
. . . . . 6
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) = 1) |
35 | 23, 28, 34 | syl2an2r 876 |
. . . . 5
⊢ ((((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) ∧ 𝑥 ∈ 𝑉) → ((#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) = 1) |
36 | 35 | sumeq2dv 14433 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 ((#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) = Σ𝑥 ∈ 𝑉 1) |
37 | 36 | oveq1d 6665 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 ((#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
38 | 22, 37 | eqtrd 2656 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 (#‘(𝑥(𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})𝑃)) mod 𝑃) = (Σ𝑥 ∈ 𝑉 1 mod 𝑃)) |
39 | | 1cnd 10056 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 1 ∈
ℂ) |
40 | | fsumconst 14522 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑥
∈ 𝑉 1 =
((#‘𝑉) ·
1)) |
41 | 11, 39, 40 | syl2an 494 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = ((#‘𝑉) · 1)) |
42 | | hashcl 13147 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
43 | 42 | nn0red 11352 |
. . . . . . 7
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℝ) |
44 | | ax-1rid 10006 |
. . . . . . 7
⊢
((#‘𝑉) ∈
ℝ → ((#‘𝑉)
· 1) = (#‘𝑉)) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝑉 ∈ Fin →
((#‘𝑉) · 1) =
(#‘𝑉)) |
46 | 45 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → ((#‘𝑉) · 1) = (#‘𝑉)) |
47 | 46 | adantr 481 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) · 1) = (#‘𝑉)) |
48 | 41, 47 | eqtrd 2656 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → Σ𝑥 ∈ 𝑉 1 = (#‘𝑉)) |
49 | 48 | oveq1d 6665 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (Σ𝑥 ∈ 𝑉 1 mod 𝑃) = ((#‘𝑉) mod 𝑃)) |
50 | 9, 38, 49 | 3eqtrd 2660 |
1
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘(𝑃 ClWWalksN 𝐺)) mod 𝑃) = ((#‘𝑉) mod 𝑃)) |