Metamath Proof Explorer

Theorem freshmansdream

Description: For a prime number P , if X and Y are members of a commutative ring R of characteristic P , then ( ( X + Y ) ^ P ) = ( ( X ^ P ) + ( Y ^ P ) ) . This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023)

Ref Expression
Hypotheses freshmansdream.s ⊢ 𝐵 = ( Base ‘ 𝑅 )
freshmansdream.a ⊢ + = ( +g ‘ 𝑅 )
freshmansdream.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
freshmansdream.c ⊢ 𝑃 = ( chr ‘ 𝑅 )
freshmansdream.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
freshmansdream.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
freshmansdream.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
freshmansdream.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion freshmansdream ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝑌 ) ) = ( ( 𝑃 ↑ 𝑋 ) + ( 𝑃 ↑ 𝑌 ) ) )

Proof

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