Step | Hyp | Ref
| Expression |
1 | | freshmansdream.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
2 | | crngring 19976 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
3 | | freshmansdream.c |
. . . . 5
⊢ 𝑃 = (chr‘𝑅) |
4 | 3 | chrcl 20929 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑃 ∈
ℕ0) |
5 | 1, 2, 4 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
6 | | freshmansdream.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
7 | | freshmansdream.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
8 | | freshmansdream.s |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
9 | | eqid 2736 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
10 | | eqid 2736 |
. . . 4
⊢
(.g‘𝑅) = (.g‘𝑅) |
11 | | freshmansdream.a |
. . . 4
⊢ + =
(+g‘𝑅) |
12 | | eqid 2736 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
13 | | freshmansdream.p |
. . . 4
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
14 | 8, 9, 10, 11, 12, 13 | crngbinom 20047 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ ℕ0)
∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑃 ↑ (𝑋 + 𝑌)) = (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) |
15 | 1, 5, 6, 7, 14 | syl22anc 837 |
. 2
⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) |
16 | 5 | nn0cnd 12475 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) |
17 | | 1cnd 11150 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
18 | 16, 17 | npcand 11516 |
. . . . . 6
⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃) |
19 | 18 | oveq2d 7373 |
. . . . 5
⊢ (𝜑 → (0...((𝑃 − 1) + 1)) = (0...𝑃)) |
20 | 19 | eqcomd 2742 |
. . . 4
⊢ (𝜑 → (0...𝑃) = (0...((𝑃 − 1) + 1))) |
21 | 20 | mpteq1d 5200 |
. . 3
⊢ (𝜑 → (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))) = (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) |
22 | 21 | oveq2d 7373 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑅 Σg (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) |
23 | | ringcmn 20003 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
24 | 1, 2, 23 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CMnd) |
25 | | freshmansdream.1 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) |
26 | | prmnn 16550 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
27 | | nnm1nn0 12454 |
. . . . 5
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
28 | 25, 26, 27 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
29 | | ringgrp 19969 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
30 | 1, 2, 29 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
31 | 30 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑅 ∈ Grp) |
32 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑃 ∈
ℕ0) |
33 | | fzssz 13443 |
. . . . . . . . 9
⊢
(0...((𝑃 − 1)
+ 1)) ⊆ ℤ |
34 | 33 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0...((𝑃 − 1) + 1)) ⊆
ℤ) |
35 | 34 | sselda 3944 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ ℤ) |
36 | | bccl 14222 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ0
∧ 𝑖 ∈ ℤ)
→ (𝑃C𝑖) ∈
ℕ0) |
37 | 32, 35, 36 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃C𝑖) ∈
ℕ0) |
38 | 37 | nn0zd 12525 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃C𝑖) ∈ ℤ) |
39 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
40 | 39 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑅 ∈ Ring) |
41 | 12, 8 | mgpbas 19902 |
. . . . . . 7
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
42 | 12 | ringmgp 19970 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
43 | 39, 42 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
44 | 43 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) →
(mulGrp‘𝑅) ∈
Mnd) |
45 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ (0...((𝑃 − 1) + 1))) |
46 | 19 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (0...((𝑃 − 1) + 1)) = (0...𝑃)) |
47 | 45, 46 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ (0...𝑃)) |
48 | | fznn0sub 13473 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝑃) → (𝑃 − 𝑖) ∈
ℕ0) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃 − 𝑖) ∈
ℕ0) |
50 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑋 ∈ 𝐵) |
51 | 41, 13, 44, 49, 50 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) |
52 | | elfznn0 13534 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...((𝑃 − 1) + 1)) → 𝑖 ∈ ℕ0) |
53 | 52 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ ℕ0) |
54 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑌 ∈ 𝐵) |
55 | 41, 13, 44, 53, 54 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) |
56 | 8, 9 | ringcl 19981 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵 ∧ (𝑖 ↑ 𝑌) ∈ 𝐵) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) |
57 | 40, 51, 55, 56 | syl3anc 1371 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) |
58 | 8, 10 | mulgcl 18893 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ (𝑃C𝑖) ∈ ℤ ∧ (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) |
59 | 31, 38, 57, 58 | syl3anc 1371 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) |
60 | 8, 11, 24, 28, 59 | gsummptfzsplit 19709 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = ((𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {((𝑃 − 1) + 1)} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))))) |
61 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑅 ∈ Grp) |
62 | | elfzelz 13441 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0...(𝑃 − 1)) → 𝑖 ∈ ℤ) |
63 | 5, 62, 36 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃C𝑖) ∈
ℕ0) |
64 | 63 | nn0zd 12525 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃C𝑖) ∈ ℤ) |
65 | 39 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑅 ∈ Ring) |
66 | 65, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (mulGrp‘𝑅) ∈ Mnd) |
67 | | fzssp1 13484 |
. . . . . . . . . . . 12
⊢
(0...(𝑃 − 1))
⊆ (0...((𝑃 − 1)
+ 1)) |
68 | 67, 19 | sseqtrid 3996 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...(𝑃 − 1)) ⊆ (0...𝑃)) |
69 | 68 | sselda 3944 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑖 ∈ (0...𝑃)) |
70 | 69, 48 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃 − 𝑖) ∈
ℕ0) |
71 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑋 ∈ 𝐵) |
72 | 41, 13, 66, 70, 71 | mulgnn0cld 18897 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) |
73 | | elfznn0 13534 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (0...(𝑃 − 1)) → 𝑖 ∈ ℕ0) |
74 | 73 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑖 ∈ ℕ0) |
75 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑌 ∈ 𝐵) |
76 | 41, 13, 66, 74, 75 | mulgnn0cld 18897 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) |
77 | 65, 72, 76, 56 | syl3anc 1371 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) |
78 | 61, 64, 77, 58 | syl3anc 1371 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) |
79 | 8, 11, 24, 28, 78 | gsummptfzsplitl 19710 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = ((𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))))) |
80 | 39 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑅 ∈ Ring) |
81 | | prmdvdsbc 31712 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑖)) |
82 | 25, 81 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑖)) |
83 | 80, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (mulGrp‘𝑅) ∈ Mnd) |
84 | 5 | nn0zd 12525 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
85 | | 1nn0 12429 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
86 | | eluzmn 12770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℕ0) → 𝑃 ∈ (ℤ≥‘(𝑃 − 1))) |
87 | 84, 85, 86 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 1))) |
88 | | fzss2 13481 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 1)) → (1...(𝑃 − 1)) ⊆ (1...𝑃)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...(𝑃 − 1)) ⊆ (1...𝑃)) |
90 | 89 | sselda 3944 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑖 ∈ (1...𝑃)) |
91 | | fznn0sub 13473 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑃) → (𝑃 − 𝑖) ∈
ℕ0) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (𝑃 − 𝑖) ∈
ℕ0) |
93 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑋 ∈ 𝐵) |
94 | 41, 13, 83, 92, 93 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) |
95 | | elfznn 13470 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...(𝑃 − 1)) → 𝑖 ∈ ℕ) |
96 | 95 | nnnn0d 12473 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...(𝑃 − 1)) → 𝑖 ∈ ℕ0) |
97 | 96 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑖 ∈ ℕ0) |
98 | 7 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑌 ∈ 𝐵) |
99 | 41, 13, 83, 97, 98 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) |
100 | 80, 94, 99, 56 | syl3anc 1371 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) |
101 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
102 | 3, 8, 10, 101 | dvdschrmulg 32066 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∥ (𝑃C𝑖) ∧ (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (0g‘𝑅)) |
103 | 80, 82, 100, 102 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (0g‘𝑅)) |
104 | 103 | mpteq2dva 5205 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))) = (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅))) |
105 | 104 | oveq2d 7373 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅)))) |
106 | | ringmnd 19974 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
107 | 39, 106 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) |
108 | | ovex 7390 |
. . . . . . . 8
⊢
(1...(𝑃 − 1))
∈ V |
109 | 101 | gsumz 18646 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (1...(𝑃 − 1)) ∈ V) →
(𝑅
Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
110 | 107, 108,
109 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
111 | 105, 110 | eqtrd 2776 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (0g‘𝑅)) |
112 | | 0nn0 12428 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
113 | 112 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) |
114 | 41, 13, 43, 5, 6 | mulgnn0cld 18897 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ↑ 𝑋) ∈ 𝐵) |
115 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) |
116 | 115 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑃C𝑖) = (𝑃C0)) |
117 | 115 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑃 − 𝑖) = (𝑃 − 0)) |
118 | 117 | oveq1d 7372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃 − 𝑖) ↑ 𝑋) = ((𝑃 − 0) ↑ 𝑋)) |
119 | 115 | oveq1d 7372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑖 ↑ 𝑌) = (0 ↑ 𝑌)) |
120 | 118, 119 | oveq12d 7375 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) = (((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) |
121 | 116, 120 | oveq12d 7375 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌)))) |
122 | | bcn0 14210 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℕ0
→ (𝑃C0) =
1) |
123 | 5, 122 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃C0) = 1) |
124 | 16 | subid1d 11501 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 0) = 𝑃) |
125 | 124 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 0) ↑ 𝑋) = (𝑃 ↑ 𝑋)) |
126 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑅) = (1r‘𝑅) |
127 | 12, 126 | ringidval 19915 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) |
128 | 41, 127, 13 | mulg0 18879 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝐵 → (0 ↑ 𝑌) = (1r‘𝑅)) |
129 | 7, 128 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 ↑ 𝑌) = (1r‘𝑅)) |
130 | 125, 129 | oveq12d 7375 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌)) = ((𝑃 ↑ 𝑋)(.r‘𝑅)(1r‘𝑅))) |
131 | 8, 9, 126 | ringridm 19993 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝑃 ↑ 𝑋) ∈ 𝐵) → ((𝑃 ↑ 𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝑃 ↑ 𝑋)) |
132 | 39, 114, 131 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 ↑ 𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝑃 ↑ 𝑋)) |
133 | 130, 132 | eqtrd 2776 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌)) = (𝑃 ↑ 𝑋)) |
134 | 123, 133 | oveq12d 7375 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) = (1(.g‘𝑅)(𝑃 ↑ 𝑋))) |
135 | 8, 10 | mulg1 18883 |
. . . . . . . . . . 11
⊢ ((𝑃 ↑ 𝑋) ∈ 𝐵 → (1(.g‘𝑅)(𝑃 ↑ 𝑋)) = (𝑃 ↑ 𝑋)) |
136 | 114, 135 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(1(.g‘𝑅)(𝑃 ↑ 𝑋)) = (𝑃 ↑ 𝑋)) |
137 | 134, 136 | eqtrd 2776 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) = (𝑃 ↑ 𝑋)) |
138 | 137 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) = (𝑃 ↑ 𝑋)) |
139 | 121, 138 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (𝑃 ↑ 𝑋)) |
140 | 8, 107, 113, 114, 139 | gsumsnd 19729 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑃 ↑ 𝑋)) |
141 | 111, 140 | oveq12d 7375 |
. . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) = ((0g‘𝑅) + (𝑃 ↑ 𝑋))) |
142 | 8, 11, 101 | grplid 18780 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ (𝑃 ↑ 𝑋) ∈ 𝐵) → ((0g‘𝑅) + (𝑃 ↑ 𝑋)) = (𝑃 ↑ 𝑋)) |
143 | 30, 114, 142 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑅)
+ (𝑃 ↑ 𝑋)) = (𝑃 ↑ 𝑋)) |
144 | 79, 141, 143 | 3eqtrd 2780 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑃 ↑ 𝑋)) |
145 | 18, 5 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → ((𝑃 − 1) + 1) ∈
ℕ0) |
146 | 41, 13, 43, 5, 7 | mulgnn0cld 18897 |
. . . . 5
⊢ (𝜑 → (𝑃 ↑ 𝑌) ∈ 𝐵) |
147 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → 𝑖 = ((𝑃 − 1) + 1)) |
148 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃 − 1) + 1) = 𝑃) |
149 | 147, 148 | eqtrd 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → 𝑖 = 𝑃) |
150 | 149 | oveq2d 7373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑃C𝑖) = (𝑃C𝑃)) |
151 | 149 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑃 − 𝑖) = (𝑃 − 𝑃)) |
152 | 151 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃 − 𝑖) ↑ 𝑋) = ((𝑃 − 𝑃) ↑ 𝑋)) |
153 | 149 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑖 ↑ 𝑌) = (𝑃 ↑ 𝑌)) |
154 | 152, 153 | oveq12d 7375 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) = (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) |
155 | 150, 154 | oveq12d 7375 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)))) |
156 | | bcnn 14212 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ0
→ (𝑃C𝑃) = 1) |
157 | 5, 156 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃C𝑃) = 1) |
158 | 16 | subidd 11500 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 𝑃) = 0) |
159 | 158 | oveq1d 7372 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 𝑃) ↑ 𝑋) = (0 ↑ 𝑋)) |
160 | 41, 127, 13 | mulg0 18879 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐵 → (0 ↑ 𝑋) = (1r‘𝑅)) |
161 | 6, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ↑ 𝑋) = (1r‘𝑅)) |
162 | 159, 161 | eqtrd 2776 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 𝑃) ↑ 𝑋) = (1r‘𝑅)) |
163 | 162 | oveq1d 7372 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)) = ((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌))) |
164 | 8, 9, 126 | ringlidm 19992 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑃 ↑ 𝑌) ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) |
165 | 39, 146, 164 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) |
166 | 163, 165 | eqtrd 2776 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) |
167 | 157, 166 | oveq12d 7375 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (1(.g‘𝑅)(𝑃 ↑ 𝑌))) |
168 | 8, 10 | mulg1 18883 |
. . . . . . . . 9
⊢ ((𝑃 ↑ 𝑌) ∈ 𝐵 → (1(.g‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) |
169 | 146, 168 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(1(.g‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) |
170 | 167, 169 | eqtrd 2776 |
. . . . . . 7
⊢ (𝜑 → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) |
171 | 170 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) |
172 | 155, 171 | eqtrd 2776 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) |
173 | 8, 107, 145, 146, 172 | gsumsnd 19729 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ {((𝑃 − 1) + 1)} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑃 ↑ 𝑌)) |
174 | 144, 173 | oveq12d 7375 |
. . 3
⊢ (𝜑 → ((𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {((𝑃 − 1) + 1)} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) |
175 | 60, 174 | eqtrd 2776 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) |
176 | 15, 22, 175 | 3eqtrd 2780 |
1
⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) |