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