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 
|- B = ( Base ` R )
freshmansdream.a 
|- .+ = ( +g ` R )
freshmansdream.p 
|- .^ = ( .g ` ( mulGrp ` R ) )
freshmansdream.c 
|- P = ( chr ` R )
freshmansdream.r 
|- ( ph -> R e. CRing )
freshmansdream.1 
|- ( ph -> P e. Prime )
freshmansdream.x 
|- ( ph -> X e. B )
freshmansdream.y 
|- ( ph -> Y e. B )
Assertion freshmansdream 
|- ( ph -> ( P .^ ( X .+ Y ) ) = ( ( P .^ X ) .+ ( P .^ Y ) ) )

Proof

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