Metamath Proof Explorer

Theorem deg1prod

Description: Degree of a product of polynomials. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses deg1prod.1 
|- D = ( deg1 ` R )
deg1prod.2 
|- P = ( Poly1 ` R )
deg1prod.3 
|- B = ( Base ` P )
deg1prod.4 
|- M = ( mulGrp ` P )
deg1prod.5 
|- .0. = ( 0g ` P )
deg1prod.6 
|- ( ph -> A e. Fin )
deg1prod.7 
|- ( ph -> R e. IDomn )
deg1prod.8 
|- ( ph -> F : A --> ( B \ { .0. } ) )
Assertion deg1prod 
|- ( ph -> ( D ` ( M gsum F ) ) = sum_ k e. A ( D ` ( F ` k ) ) )

Proof

Step Hyp Ref Expression
1 deg1prod.1 
 |-  D = ( deg1 ` R )
2 deg1prod.2 
 |-  P = ( Poly1 ` R )
3 deg1prod.3 
 |-  B = ( Base ` P )
4 deg1prod.4 
 |-  M = ( mulGrp ` P )
5 deg1prod.5 
 |-  .0. = ( 0g ` P )
6 deg1prod.6 
 |-  ( ph -> A e. Fin )
7 deg1prod.7 
 |-  ( ph -> R e. IDomn )
8 deg1prod.8 
 |-  ( ph -> F : A --> ( B \ { .0. } ) )
9 8 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
10 9 oveq2d 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( k e. A |-> ( F ` k ) ) ) )
11 10 fveq2d 
 |-  ( ph -> ( D ` ( M gsum F ) ) = ( D ` ( M gsum ( k e. A |-> ( F ` k ) ) ) ) )
12 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> ( F ` k ) ) = ( k e. (/) |-> ( F ` k ) ) )
13 12 oveq2d 
 |-  ( a = (/) -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. (/) |-> ( F ` k ) ) ) )
14 13 fveq2d 
 |-  ( a = (/) -> ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = ( D ` ( M gsum ( k e. (/) |-> ( F ` k ) ) ) ) )
15 sumeq1 
 |-  ( a = (/) -> sum_ k e. a ( D ` ( F ` k ) ) = sum_ k e. (/) ( D ` ( F ` k ) ) )
16 14 15 eqeq12d 
 |-  ( a = (/) -> ( ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = sum_ k e. a ( D ` ( F ` k ) ) <-> ( D ` ( M gsum ( k e. (/) |-> ( F ` k ) ) ) ) = sum_ k e. (/) ( D ` ( F ` k ) ) ) )
17 mpteq1 
 |-  ( a = b -> ( k e. a |-> ( F ` k ) ) = ( k e. b |-> ( F ` k ) ) )
18 17 oveq2d 
 |-  ( a = b -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. b |-> ( F ` k ) ) ) )
19 18 fveq2d 
 |-  ( a = b -> ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) )
20 sumeq1 
 |-  ( a = b -> sum_ k e. a ( D ` ( F ` k ) ) = sum_ k e. b ( D ` ( F ` k ) ) )
21 19 20 eqeq12d 
 |-  ( a = b -> ( ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = sum_ k e. a ( D ` ( F ` k ) ) <-> ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) )
22 mpteq1 
 |-  ( a = ( b u. { l } ) -> ( k e. a |-> ( F ` k ) ) = ( k e. ( b u. { l } ) |-> ( F ` k ) ) )
23 22 oveq2d 
 |-  ( a = ( b u. { l } ) -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) )
24 23 fveq2d 
 |-  ( a = ( b u. { l } ) -> ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) )
25 sumeq1 
 |-  ( a = ( b u. { l } ) -> sum_ k e. a ( D ` ( F ` k ) ) = sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) )
26 24 25 eqeq12d 
 |-  ( a = ( b u. { l } ) -> ( ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = sum_ k e. a ( D ` ( F ` k ) ) <-> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) ) )
27 mpteq1 
 |-  ( a = A -> ( k e. a |-> ( F ` k ) ) = ( k e. A |-> ( F ` k ) ) )
28 27 oveq2d 
 |-  ( a = A -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. A |-> ( F ` k ) ) ) )
29 28 fveq2d 
 |-  ( a = A -> ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = ( D ` ( M gsum ( k e. A |-> ( F ` k ) ) ) ) )
30 sumeq1 
 |-  ( a = A -> sum_ k e. a ( D ` ( F ` k ) ) = sum_ k e. A ( D ` ( F ` k ) ) )
31 29 30 eqeq12d 
 |-  ( a = A -> ( ( D ` ( M gsum ( k e. a |-> ( F ` k ) ) ) ) = sum_ k e. a ( D ` ( F ` k ) ) <-> ( D ` ( M gsum ( k e. A |-> ( F ` k ) ) ) ) = sum_ k e. A ( D ` ( F ` k ) ) ) )
32 mpt0 
 |-  ( k e. (/) |-> ( F ` k ) ) = (/)
33 32 oveq2i 
 |-  ( M gsum ( k e. (/) |-> ( F ` k ) ) ) = ( M gsum (/) )
34 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
35 4 34 ringidval 
 |-  ( 1r ` P ) = ( 0g ` M )
36 35 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` P )
37 33 36 eqtri 
 |-  ( M gsum ( k e. (/) |-> ( F ` k ) ) ) = ( 1r ` P )
38 37 a1i 
 |-  ( ph -> ( M gsum ( k e. (/) |-> ( F ` k ) ) ) = ( 1r ` P ) )
39 38 fveq2d 
 |-  ( ph -> ( D ` ( M gsum ( k e. (/) |-> ( F ` k ) ) ) ) = ( D ` ( 1r ` P ) ) )
40 7 idomdomd 
 |-  ( ph -> R e. Domn )
41 domnring 
 |-  ( R e. Domn -> R e. Ring )
42 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
43 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
44 2 42 43 34 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
45 40 41 44 3syl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
46 45 fveq2d 
 |-  ( ph -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( D ` ( 1r ` P ) ) )
47 7 idomringd 
 |-  ( ph -> R e. Ring )
48 eqid 
 |-  ( Base ` R ) = ( Base ` R )
49 48 43 47 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
50 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
51 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
52 43 51 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
53 40 50 52 3syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
54 1 2 48 42 51 deg1scl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = 0 )
55 47 49 53 54 syl3anc 
 |-  ( ph -> ( D ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = 0 )
56 39 46 55 3eqtr2d 
 |-  ( ph -> ( D ` ( M gsum ( k e. (/) |-> ( F ` k ) ) ) ) = 0 )
57 sum0 
 |-  sum_ k e. (/) ( D ` ( F ` k ) ) = 0
58 56 57 eqtr4di 
 |-  ( ph -> ( D ` ( M gsum ( k e. (/) |-> ( F ` k ) ) ) ) = sum_ k e. (/) ( D ` ( F ` k ) ) )
59 eqid 
 |-  ( .r ` P ) = ( .r ` P )
60 40 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> R e. Domn )
61 4 3 mgpbas 
 |-  B = ( Base ` M )
62 2 ply1idom 
 |-  ( R e. IDomn -> P e. IDomn )
63 7 62 syl 
 |-  ( ph -> P e. IDomn )
64 63 idomcringd 
 |-  ( ph -> P e. CRing )
65 4 crngmgp 
 |-  ( P e. CRing -> M e. CMnd )
66 64 65 syl 
 |-  ( ph -> M e. CMnd )
67 66 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> M e. CMnd )
68 6 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> A e. Fin )
69 simplr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> b C_ A )
70 68 69 ssfid 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> b e. Fin )
71 8 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> F : A --> ( B \ { .0. } ) )
72 69 sselda 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> k e. A )
73 71 72 ffvelcdmd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> ( F ` k ) e. ( B \ { .0. } ) )
74 73 eldifad 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> ( F ` k ) e. B )
75 74 ralrimiva 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> A. k e. b ( F ` k ) e. B )
76 61 67 70 75 gsummptcl 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( M gsum ( k e. b |-> ( F ` k ) ) ) e. B )
77 nfv 
 |-  F/ k ( ph /\ b C_ A )
78 eqid 
 |-  ( k e. b |-> ( F ` k ) ) = ( k e. b |-> ( F ` k ) )
79 5 fvexi 
 |-  .0. e. _V
80 79 a1i 
 |-  ( ( ph /\ b C_ A ) -> .0. e. _V )
81 8 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> F : A --> ( B \ { .0. } ) )
82 simpr 
 |-  ( ( ph /\ b C_ A ) -> b C_ A )
83 82 sselda 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> k e. A )
84 81 83 ffvelcdmd 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> ( F ` k ) e. ( B \ { .0. } ) )
85 eldifsni 
 |-  ( ( F ` k ) e. ( B \ { .0. } ) -> ( F ` k ) =/= .0. )
86 84 85 syl 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> ( F ` k ) =/= .0. )
87 86 necomd 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> .0. =/= ( F ` k ) )
88 77 78 80 87 nelrnmpt 
 |-  ( ( ph /\ b C_ A ) -> -. .0. e. ran ( k e. b |-> ( F ` k ) ) )
89 63 adantr 
 |-  ( ( ph /\ b C_ A ) -> P e. IDomn )
90 6 adantr 
 |-  ( ( ph /\ b C_ A ) -> A e. Fin )
91 90 82 ssfid 
 |-  ( ( ph /\ b C_ A ) -> b e. Fin )
92 84 eldifad 
 |-  ( ( ( ph /\ b C_ A ) /\ k e. b ) -> ( F ` k ) e. B )
93 92 fmpttd 
 |-  ( ( ph /\ b C_ A ) -> ( k e. b |-> ( F ` k ) ) : b --> B )
94 4 3 5 89 91 93 domnprodeq0 
 |-  ( ( ph /\ b C_ A ) -> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) )
95 94 necon3abid 
 |-  ( ( ph /\ b C_ A ) -> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) =/= .0. <-> -. .0. e. ran ( k e. b |-> ( F ` k ) ) ) )
96 88 95 mpbird 
 |-  ( ( ph /\ b C_ A ) -> ( M gsum ( k e. b |-> ( F ` k ) ) ) =/= .0. )
97 96 adantr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( M gsum ( k e. b |-> ( F ` k ) ) ) =/= .0. )
98 8 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> F : A --> ( B \ { .0. } ) )
99 simpr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> l e. ( A \ b ) )
100 99 eldifad 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> l e. A )
101 98 100 ffvelcdmd 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( F ` l ) e. ( B \ { .0. } ) )
102 101 eldifad 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( F ` l ) e. B )
103 eldifsni 
 |-  ( ( F ` l ) e. ( B \ { .0. } ) -> ( F ` l ) =/= .0. )
104 101 103 syl 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( F ` l ) =/= .0. )
105 1 2 3 59 5 60 76 97 102 104 deg1mul 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( D ` ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) ) = ( ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) + ( D ` ( F ` l ) ) ) )
106 105 adantr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) ) = ( ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) + ( D ` ( F ` l ) ) ) )
107 simpr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) )
108 107 oveq1d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) + ( D ` ( F ` l ) ) ) = ( sum_ k e. b ( D ` ( F ` k ) ) + ( D ` ( F ` l ) ) ) )
109 106 108 eqtr2d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( sum_ k e. b ( D ` ( F ` k ) ) + ( D ` ( F ` l ) ) ) = ( D ` ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) ) )
110 nfv 
 |-  F/ k ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) )
111 nfcv 
 |-  F/_ k D
112 nfcv 
 |-  F/_ k M
113 nfcv 
 |-  F/_ k gsum
114 nfmpt1 
 |-  F/_ k ( k e. b |-> ( F ` k ) )
115 112 113 114 nfov 
 |-  F/_ k ( M gsum ( k e. b |-> ( F ` k ) ) )
116 111 115 nffv 
 |-  F/_ k ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) )
117 nfcv 
 |-  F/_ k b
118 117 nfsum1 
 |-  F/_ k sum_ k e. b ( D ` ( F ` k ) )
119 116 118 nfeq 
 |-  F/ k ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) )
120 110 119 nfan 
 |-  F/ k ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) )
121 nfcv 
 |-  F/_ k ( D ` ( F ` l ) )
122 6 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> A e. Fin )
123 simpllr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> b C_ A )
124 122 123 ssfid 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> b e. Fin )
125 simplr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> l e. ( A \ b ) )
126 125 eldifbd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> -. l e. b )
127 47 ad4antr 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> R e. Ring )
128 8 ad4antr 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> F : A --> ( B \ { .0. } ) )
129 123 sselda 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> k e. A )
130 128 129 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> ( F ` k ) e. ( B \ { .0. } ) )
131 130 eldifad 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> ( F ` k ) e. B )
132 130 85 syl 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> ( F ` k ) =/= .0. )
133 1 2 5 3 deg1nn0cl 
 |-  ( ( R e. Ring /\ ( F ` k ) e. B /\ ( F ` k ) =/= .0. ) -> ( D ` ( F ` k ) ) e. NN0 )
134 127 131 132 133 syl3anc 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> ( D ` ( F ` k ) ) e. NN0 )
135 134 nn0cnd 
 |-  ( ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) /\ k e. b ) -> ( D ` ( F ` k ) ) e. CC )
136 2fveq3 
 |-  ( k = l -> ( D ` ( F ` k ) ) = ( D ` ( F ` l ) ) )
137 47 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> R e. Ring )
138 8 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> F : A --> ( B \ { .0. } ) )
139 125 eldifad 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> l e. A )
140 138 139 ffvelcdmd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( F ` l ) e. ( B \ { .0. } ) )
141 140 eldifad 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( F ` l ) e. B )
142 140 103 syl 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( F ` l ) =/= .0. )
143 1 2 5 3 deg1nn0cl 
 |-  ( ( R e. Ring /\ ( F ` l ) e. B /\ ( F ` l ) =/= .0. ) -> ( D ` ( F ` l ) ) e. NN0 )
144 137 141 142 143 syl3anc 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( F ` l ) ) e. NN0 )
145 144 nn0cnd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( F ` l ) ) e. CC )
146 120 121 124 125 126 135 136 145 fsumsplitsn 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) = ( sum_ k e. b ( D ` ( F ` k ) ) + ( D ` ( F ` l ) ) ) )
147 4 59 mgpplusg 
 |-  ( .r ` P ) = ( +g ` M )
148 99 eldifbd 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> -. l e. b )
149 fveq2 
 |-  ( k = l -> ( F ` k ) = ( F ` l ) )
150 61 147 67 70 74 99 148 102 149 gsumunsn 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) )
151 150 fveq2d 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = ( D ` ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) ) )
152 151 adantr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = ( D ` ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` P ) ( F ` l ) ) ) )
153 109 146 152 3eqtr4rd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) ) -> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) )
154 153 ex 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) -> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) ) )
155 154 anasss 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( ( D ` ( M gsum ( k e. b |-> ( F ` k ) ) ) ) = sum_ k e. b ( D ` ( F ` k ) ) -> ( D ` ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) = sum_ k e. ( b u. { l } ) ( D ` ( F ` k ) ) ) )
156 16 21 26 31 58 155 6 findcard2d 
 |-  ( ph -> ( D ` ( M gsum ( k e. A |-> ( F ` k ) ) ) ) = sum_ k e. A ( D ` ( F ` k ) ) )
157 11 156 eqtrd 
 |-  ( ph -> ( D ` ( M gsum F ) ) = sum_ k e. A ( D ` ( F ` k ) ) )