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