| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | freshmansdream.r | . . 3
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 2 |  | crngring 20243 | . . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 3 |  | freshmansdream.c | . . . . 5
⊢ 𝑃 = (chr‘𝑅) | 
| 4 | 3 | chrcl 21540 | . . . 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 20333 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ ℕ0)
∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑃 ↑ (𝑋 + 𝑌)) = (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) | 
| 15 | 1, 5, 6, 7, 14 | syl22anc 838 | . 2
⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) | 
| 16 | 5 | nn0cnd 12591 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 17 |  | 1cnd 11257 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) | 
| 18 | 16, 17 | npcand 11625 | . . . . . 6
⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃) | 
| 19 | 18 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → (0...((𝑃 − 1) + 1)) = (0...𝑃)) | 
| 20 | 19 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (0...𝑃) = (0...((𝑃 − 1) + 1))) | 
| 21 | 20 | mpteq1d 5236 | . . 3
⊢ (𝜑 → (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))) = (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) | 
| 22 | 21 | oveq2d 7448 | . 2
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...𝑃) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑅 Σg (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) | 
| 23 |  | ringcmn 20280 | . . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) | 
| 24 | 1, 2, 23 | 3syl 18 | . . . 4
⊢ (𝜑 → 𝑅 ∈ CMnd) | 
| 25 |  | freshmansdream.1 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 26 |  | prmnn 16712 | . . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 27 |  | nnm1nn0 12569 | . . . . 5
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) | 
| 28 | 25, 26, 27 | 3syl 18 | . . . 4
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) | 
| 29 |  | ringgrp 20236 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 30 | 1, 2, 29 | 3syl 18 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 31 | 30 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑅 ∈ Grp) | 
| 32 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑃 ∈
ℕ0) | 
| 33 |  | fzssz 13567 | . . . . . . . . 9
⊢
(0...((𝑃 − 1)
+ 1)) ⊆ ℤ | 
| 34 | 33 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (0...((𝑃 − 1) + 1)) ⊆
ℤ) | 
| 35 | 34 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ ℤ) | 
| 36 |  | bccl 14362 | . . . . . . 7
⊢ ((𝑃 ∈ ℕ0
∧ 𝑖 ∈ ℤ)
→ (𝑃C𝑖) ∈
ℕ0) | 
| 37 | 32, 35, 36 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃C𝑖) ∈
ℕ0) | 
| 38 | 37 | nn0zd 12641 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃C𝑖) ∈ ℤ) | 
| 39 | 1, 2 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 40 | 39 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑅 ∈ Ring) | 
| 41 | 12, 8 | mgpbas 20143 | . . . . . . 7
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) | 
| 42 | 12 | ringmgp 20237 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) | 
| 43 | 39, 42 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) | 
| 44 | 43 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) →
(mulGrp‘𝑅) ∈
Mnd) | 
| 45 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ (0...((𝑃 − 1) + 1))) | 
| 46 | 19 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (0...((𝑃 − 1) + 1)) = (0...𝑃)) | 
| 47 | 45, 46 | eleqtrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ (0...𝑃)) | 
| 48 |  | fznn0sub 13597 | . . . . . . . 8
⊢ (𝑖 ∈ (0...𝑃) → (𝑃 − 𝑖) ∈
ℕ0) | 
| 49 | 47, 48 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑃 − 𝑖) ∈
ℕ0) | 
| 50 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑋 ∈ 𝐵) | 
| 51 | 41, 13, 44, 49, 50 | mulgnn0cld 19114 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) | 
| 52 |  | elfznn0 13661 | . . . . . . . 8
⊢ (𝑖 ∈ (0...((𝑃 − 1) + 1)) → 𝑖 ∈ ℕ0) | 
| 53 | 52 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑖 ∈ ℕ0) | 
| 54 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → 𝑌 ∈ 𝐵) | 
| 55 | 41, 13, 44, 53, 54 | mulgnn0cld 19114 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) | 
| 56 | 8, 9 | ringcl 20248 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵 ∧ (𝑖 ↑ 𝑌) ∈ 𝐵) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) | 
| 57 | 40, 51, 55, 56 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) | 
| 58 | 8, 10 | mulgcl 19110 | . . . . 5
⊢ ((𝑅 ∈ Grp ∧ (𝑃C𝑖) ∈ ℤ ∧ (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) | 
| 59 | 31, 38, 57, 58 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...((𝑃 − 1) + 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) | 
| 60 | 8, 11, 24, 28, 59 | gsummptfzsplit 19951 | . . 3
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...((𝑃 − 1) + 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = ((𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {((𝑃 − 1) + 1)} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))))) | 
| 61 | 30 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑅 ∈ Grp) | 
| 62 |  | elfzelz 13565 | . . . . . . . . 9
⊢ (𝑖 ∈ (0...(𝑃 − 1)) → 𝑖 ∈ ℤ) | 
| 63 | 5, 62, 36 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃C𝑖) ∈
ℕ0) | 
| 64 | 63 | nn0zd 12641 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃C𝑖) ∈ ℤ) | 
| 65 | 39 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑅 ∈ Ring) | 
| 66 | 65, 42 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (mulGrp‘𝑅) ∈ Mnd) | 
| 67 |  | fzssp1 13608 | . . . . . . . . . . . 12
⊢
(0...(𝑃 − 1))
⊆ (0...((𝑃 − 1)
+ 1)) | 
| 68 | 67, 19 | sseqtrid 4025 | . . . . . . . . . . 11
⊢ (𝜑 → (0...(𝑃 − 1)) ⊆ (0...𝑃)) | 
| 69 | 68 | sselda 3982 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑖 ∈ (0...𝑃)) | 
| 70 | 69, 48 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑃 − 𝑖) ∈
ℕ0) | 
| 71 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑋 ∈ 𝐵) | 
| 72 | 41, 13, 66, 70, 71 | mulgnn0cld 19114 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) | 
| 73 |  | elfznn0 13661 | . . . . . . . . . 10
⊢ (𝑖 ∈ (0...(𝑃 − 1)) → 𝑖 ∈ ℕ0) | 
| 74 | 73 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑖 ∈ ℕ0) | 
| 75 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → 𝑌 ∈ 𝐵) | 
| 76 | 41, 13, 66, 74, 75 | mulgnn0cld 19114 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) | 
| 77 | 65, 72, 76, 56 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) | 
| 78 | 61, 64, 77, 58 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑃 − 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) ∈ 𝐵) | 
| 79 | 8, 11, 24, 28, 78 | gsummptfzsplitl 19952 | . . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (0...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = ((𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))))) | 
| 80 | 39 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑅 ∈ Ring) | 
| 81 |  | prmdvdsbc 16764 | . . . . . . . . . . 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 12641 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 85 |  | 1nn0 12544 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 | 
| 86 |  | eluzmn 12886 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℕ0) → 𝑃 ∈ (ℤ≥‘(𝑃 − 1))) | 
| 87 | 84, 85, 86 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 1))) | 
| 88 |  | fzss2 13605 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 1)) → (1...(𝑃 − 1)) ⊆ (1...𝑃)) | 
| 89 | 87, 88 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1...(𝑃 − 1)) ⊆ (1...𝑃)) | 
| 90 | 89 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑖 ∈ (1...𝑃)) | 
| 91 |  | fznn0sub 13597 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑃) → (𝑃 − 𝑖) ∈
ℕ0) | 
| 92 | 90, 91 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (𝑃 − 𝑖) ∈
ℕ0) | 
| 93 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑋 ∈ 𝐵) | 
| 94 | 41, 13, 83, 92, 93 | mulgnn0cld 19114 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → ((𝑃 − 𝑖) ↑ 𝑋) ∈ 𝐵) | 
| 95 |  | elfznn 13594 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...(𝑃 − 1)) → 𝑖 ∈ ℕ) | 
| 96 | 95 | nnnn0d 12589 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...(𝑃 − 1)) → 𝑖 ∈ ℕ0) | 
| 97 | 96 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑖 ∈ ℕ0) | 
| 98 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → 𝑌 ∈ 𝐵) | 
| 99 | 41, 13, 83, 97, 98 | mulgnn0cld 19114 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (𝑖 ↑ 𝑌) ∈ 𝐵) | 
| 100 | 80, 94, 99, 56 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) | 
| 101 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 102 | 3, 8, 10, 101 | dvdschrmulg 21544 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∥ (𝑃C𝑖) ∧ (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) ∈ 𝐵) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (0g‘𝑅)) | 
| 103 | 80, 82, 100, 102 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑃 − 1))) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (0g‘𝑅)) | 
| 104 | 103 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))) = (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅))) | 
| 105 | 104 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦
(0g‘𝑅)))) | 
| 106 |  | ringmnd 20241 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 107 | 39, 106 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 108 |  | ovex 7465 | . . . . . . . 8
⊢
(1...(𝑃 − 1))
∈ V | 
| 109 | 101 | gsumz 18850 | . . . . . . . 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 12543 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 113 | 112 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 114 | 41, 13, 43, 5, 6 | mulgnn0cld 19114 | . . . . . . 7
⊢ (𝜑 → (𝑃 ↑ 𝑋) ∈ 𝐵) | 
| 115 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) | 
| 116 | 115 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑃C𝑖) = (𝑃C0)) | 
| 117 | 115 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑃 − 𝑖) = (𝑃 − 0)) | 
| 118 | 117 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃 − 𝑖) ↑ 𝑋) = ((𝑃 − 0) ↑ 𝑋)) | 
| 119 | 115 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑖 ↑ 𝑌) = (0 ↑ 𝑌)) | 
| 120 | 118, 119 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) = (((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) | 
| 121 | 116, 120 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌)))) | 
| 122 |  | bcn0 14350 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ ℕ0
→ (𝑃C0) =
1) | 
| 123 | 5, 122 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃C0) = 1) | 
| 124 | 16 | subid1d 11610 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 0) = 𝑃) | 
| 125 | 124 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 0) ↑ 𝑋) = (𝑃 ↑ 𝑋)) | 
| 126 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 127 | 12, 126 | ringidval 20181 | . . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) | 
| 128 | 41, 127, 13 | mulg0 19093 | . . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝐵 → (0 ↑ 𝑌) = (1r‘𝑅)) | 
| 129 | 7, 128 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 ↑ 𝑌) = (1r‘𝑅)) | 
| 130 | 125, 129 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌)) = ((𝑃 ↑ 𝑋)(.r‘𝑅)(1r‘𝑅))) | 
| 131 | 8, 9, 126 | ringridm 20268 | . . . . . . . . . . . . 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 7450 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) = (1(.g‘𝑅)(𝑃 ↑ 𝑋))) | 
| 135 | 8, 10 | mulg1 19100 | . . . . . . . . . . 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 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C0)(.g‘𝑅)(((𝑃 − 0) ↑ 𝑋)(.r‘𝑅)(0 ↑ 𝑌))) = (𝑃 ↑ 𝑋)) | 
| 139 | 121, 138 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (𝑃 ↑ 𝑋)) | 
| 140 | 8, 107, 113, 114, 139 | gsumsnd 19971 | . . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑃 ↑ 𝑋)) | 
| 141 | 111, 140 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → ((𝑅 Σg (𝑖 ∈ (1...(𝑃 − 1)) ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) + (𝑅 Σg (𝑖 ∈ {0} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)))))) = ((0g‘𝑅) + (𝑃 ↑ 𝑋))) | 
| 142 | 8, 11, 101 | grplid 18986 | . . . . . 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 2840 | . . . . 5
⊢ (𝜑 → ((𝑃 − 1) + 1) ∈
ℕ0) | 
| 146 | 41, 13, 43, 5, 7 | mulgnn0cld 19114 | . . . . 5
⊢ (𝜑 → (𝑃 ↑ 𝑌) ∈ 𝐵) | 
| 147 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → 𝑖 = ((𝑃 − 1) + 1)) | 
| 148 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃 − 1) + 1) = 𝑃) | 
| 149 | 147, 148 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → 𝑖 = 𝑃) | 
| 150 | 149 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑃C𝑖) = (𝑃C𝑃)) | 
| 151 | 149 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑃 − 𝑖) = (𝑃 − 𝑃)) | 
| 152 | 151 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃 − 𝑖) ↑ 𝑋) = ((𝑃 − 𝑃) ↑ 𝑋)) | 
| 153 | 149 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (𝑖 ↑ 𝑌) = (𝑃 ↑ 𝑌)) | 
| 154 | 152, 153 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → (((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌)) = (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) | 
| 155 | 150, 154 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)))) | 
| 156 |  | bcnn 14352 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℕ0
→ (𝑃C𝑃) = 1) | 
| 157 | 5, 156 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑃C𝑃) = 1) | 
| 158 | 16 | subidd 11609 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 𝑃) = 0) | 
| 159 | 158 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 𝑃) ↑ 𝑋) = (0 ↑ 𝑋)) | 
| 160 | 41, 127, 13 | mulg0 19093 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐵 → (0 ↑ 𝑋) = (1r‘𝑅)) | 
| 161 | 6, 160 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (0 ↑ 𝑋) = (1r‘𝑅)) | 
| 162 | 159, 161 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 𝑃) ↑ 𝑋) = (1r‘𝑅)) | 
| 163 | 162 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)) = ((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌))) | 
| 164 | 8, 9, 126 | ringlidm 20267 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑃 ↑ 𝑌) ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) | 
| 165 | 39, 146, 164 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) | 
| 166 | 163, 165 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) | 
| 167 | 157, 166 | oveq12d 7450 | . . . . . . . 8
⊢ (𝜑 → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (1(.g‘𝑅)(𝑃 ↑ 𝑌))) | 
| 168 | 8, 10 | mulg1 19100 | . . . . . . . . 9
⊢ ((𝑃 ↑ 𝑌) ∈ 𝐵 → (1(.g‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) | 
| 169 | 146, 168 | syl 17 | . . . . . . . 8
⊢ (𝜑 →
(1(.g‘𝑅)(𝑃 ↑ 𝑌)) = (𝑃 ↑ 𝑌)) | 
| 170 | 167, 169 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) | 
| 171 | 170 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑃)(.g‘𝑅)(((𝑃 − 𝑃) ↑ 𝑋)(.r‘𝑅)(𝑃 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) | 
| 172 | 155, 171 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 = ((𝑃 − 1) + 1)) → ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))) = (𝑃 ↑ 𝑌)) | 
| 173 | 8, 107, 145, 146, 172 | gsumsnd 19971 | . . . 4
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ {((𝑃 − 1) + 1)} ↦ ((𝑃C𝑖)(.g‘𝑅)(((𝑃 − 𝑖) ↑ 𝑋)(.r‘𝑅)(𝑖 ↑ 𝑌))))) = (𝑃 ↑ 𝑌)) | 
| 174 | 144, 173 | oveq12d 7450 | . . 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
⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) |