Metamath Proof Explorer

Theorem mhpmulcl

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024)

Ref Expression
Hypotheses mhpmulcl.h 
|- H = ( I mHomP R )
mhpmulcl.y 
|- Y = ( I mPoly R )
mhpmulcl.t 
|- .x. = ( .r ` Y )
mhpmulcl.i 
|- ( ph -> I e. V )
mhpmulcl.r 
|- ( ph -> R e. Ring )
mhpmulcl.m 
|- ( ph -> M e. NN0 )
mhpmulcl.n 
|- ( ph -> N e. NN0 )
mhpmulcl.p 
|- ( ph -> P e. ( H ` M ) )
mhpmulcl.q 
|- ( ph -> Q e. ( H ` N ) )
Assertion mhpmulcl 
|- ( ph -> ( P .x. Q ) e. ( H ` ( M + N ) ) )

Proof

Step Hyp Ref Expression
1 mhpmulcl.h 
 |-  H = ( I mHomP R )
2 mhpmulcl.y 
 |-  Y = ( I mPoly R )
3 mhpmulcl.t 
 |-  .x. = ( .r ` Y )
4 mhpmulcl.i 
 |-  ( ph -> I e. V )
5 mhpmulcl.r 
 |-  ( ph -> R e. Ring )
6 mhpmulcl.m 
 |-  ( ph -> M e. NN0 )
7 mhpmulcl.n 
 |-  ( ph -> N e. NN0 )
8 mhpmulcl.p 
 |-  ( ph -> P e. ( H ` M ) )
9 mhpmulcl.q 
 |-  ( ph -> Q e. ( H ` N ) )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
13 1 2 10 4 5 6 8 mhpmpl 
 |-  ( ph -> P e. ( Base ` Y ) )
14 1 2 10 4 5 7 9 mhpmpl 
 |-  ( ph -> Q e. ( Base ` Y ) )
15 2 10 11 3 12 13 14 mplmul 
 |-  ( ph -> ( P .x. Q ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) ) ) ) )
16 15 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( P .x. Q ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) ) ) ) )
17 breq2 
 |-  ( d = x -> ( c oR <_ d <-> c oR <_ x ) )
18 17 rabbidv 
 |-  ( d = x -> { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } = { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
19 fvoveq1 
 |-  ( d = x -> ( Q ` ( d oF - e ) ) = ( Q ` ( x oF - e ) ) )
20 19 oveq2d 
 |-  ( d = x -> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) = ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) )
21 18 20 mpteq12dv 
 |-  ( d = x -> ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) ) = ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) )
22 21 oveq2d 
 |-  ( d = x -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) ) ) = ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ d = x ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ d } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) ) ) = ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) )
24 simpr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
25 ovexd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) e. _V )
26 16 23 24 25 fvmptd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( P .x. Q ) ` x ) = ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) )
27 26 neeq1d 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( P .x. Q ) ` x ) =/= ( 0g ` R ) <-> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) =/= ( 0g ` R ) ) )
28 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ph )
29 oveq2 
 |-  ( c = e -> ( ( CCfld |`s NN0 ) gsum c ) = ( ( CCfld |`s NN0 ) gsum e ) )
30 29 eqeq1d 
 |-  ( c = e -> ( ( ( CCfld |`s NN0 ) gsum c ) = M <-> ( ( CCfld |`s NN0 ) gsum e ) = M ) )
31 30 necon3bbid 
 |-  ( c = e -> ( -. ( ( CCfld |`s NN0 ) gsum c ) = M <-> ( ( CCfld |`s NN0 ) gsum e ) =/= M ) )
32 simplr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
33 elrabi 
 |-  ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } -> e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
34 32 33 syl 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
35 simpr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( ( CCfld |`s NN0 ) gsum e ) =/= M )
36 31 34 35 elrabd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | -. ( ( CCfld |`s NN0 ) gsum c ) = M } )
37 notrab 
 |-  ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = M } ) = { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | -. ( ( CCfld |`s NN0 ) gsum c ) = M }
38 36 37 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> e e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = M } ) )
39 eqid 
 |-  ( Base ` R ) = ( Base ` R )
40 2 39 10 12 13 mplelf 
 |-  ( ph -> P : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
41 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
42 1 41 12 4 5 6 8 mhpdeg 
 |-  ( ph -> ( P supp ( 0g ` R ) ) C_ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = M } )
43 ovex 
 |-  ( NN0 ^m I ) e. _V
44 43 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
45 44 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
46 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
47 40 42 45 46 suppssr 
 |-  ( ( ph /\ e e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = M } ) ) -> ( P ` e ) = ( 0g ` R ) )
48 28 38 47 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( P ` e ) = ( 0g ` R ) )
49 48 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( ( 0g ` R ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) )
50 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> R e. Ring )
51 14 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> Q e. ( Base ` Y ) )
52 2 39 10 12 51 mplelf 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> Q : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
53 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
54 eqid 
 |-  { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } = { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x }
55 12 54 psrbagconcl 
 |-  ( ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
56 53 32 55 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( x oF - e ) e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
57 elrabi 
 |-  ( ( x oF - e ) e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } -> ( x oF - e ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
58 56 57 syl 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( x oF - e ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
59 52 58 ffvelrnd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( Q ` ( x oF - e ) ) e. ( Base ` R ) )
60 39 11 41 ringlz 
 |-  ( ( R e. Ring /\ ( Q ` ( x oF - e ) ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( 0g ` R ) )
61 50 59 60 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( ( 0g ` R ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( 0g ` R ) )
62 49 61 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum e ) =/= M ) -> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( 0g ` R ) )
63 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ph )
64 oveq2 
 |-  ( c = ( x oF - e ) -> ( ( CCfld |`s NN0 ) gsum c ) = ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) )
65 64 eqeq1d 
 |-  ( c = ( x oF - e ) -> ( ( ( CCfld |`s NN0 ) gsum c ) = N <-> ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) )
66 65 necon3bbid 
 |-  ( c = ( x oF - e ) -> ( -. ( ( CCfld |`s NN0 ) gsum c ) = N <-> ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) )
67 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
68 simplr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
69 67 68 55 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( x oF - e ) e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
70 69 57 syl 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( x oF - e ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
71 simpr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N )
72 66 70 71 elrabd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( x oF - e ) e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | -. ( ( CCfld |`s NN0 ) gsum c ) = N } )
73 notrab 
 |-  ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = N } ) = { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | -. ( ( CCfld |`s NN0 ) gsum c ) = N }
74 72 73 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( x oF - e ) e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = N } ) )
75 2 39 10 12 14 mplelf 
 |-  ( ph -> Q : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
76 1 41 12 4 5 7 9 mhpdeg 
 |-  ( ph -> ( Q supp ( 0g ` R ) ) C_ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = N } )
77 75 76 45 46 suppssr 
 |-  ( ( ph /\ ( x oF - e ) e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = N } ) ) -> ( Q ` ( x oF - e ) ) = ( 0g ` R ) )
78 63 74 77 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( Q ` ( x oF - e ) ) = ( 0g ` R ) )
79 78 oveq2d 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( ( P ` e ) ( .r ` R ) ( 0g ` R ) ) )
80 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> R e. Ring )
81 13 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> P e. ( Base ` Y ) )
82 2 39 10 12 81 mplelf 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> P : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
83 33 adantl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
84 83 adantr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
85 82 84 ffvelrnd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( P ` e ) e. ( Base ` R ) )
86 39 11 41 ringrz 
 |-  ( ( R e. Ring /\ ( P ` e ) e. ( Base ` R ) ) -> ( ( P ` e ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
87 80 85 86 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( ( P ` e ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
88 79 87 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) -> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( 0g ` R ) )
89 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
90 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
91 90 submbas 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> NN0 = ( Base ` ( CCfld |`s NN0 ) ) )
92 89 91 ax-mp 
 |-  NN0 = ( Base ` ( CCfld |`s NN0 ) )
93 cnfld0 
 |-  0 = ( 0g ` CCfld )
94 90 93 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
95 89 94 ax-mp 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
96 nn0ex 
 |-  NN0 e. _V
97 cnfldadd 
 |-  + = ( +g ` CCfld )
98 90 97 ressplusg 
 |-  ( NN0 e. _V -> + = ( +g ` ( CCfld |`s NN0 ) ) )
99 96 98 ax-mp 
 |-  + = ( +g ` ( CCfld |`s NN0 ) )
100 cnring 
 |-  CCfld e. Ring
101 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
102 100 101 ax-mp 
 |-  CCfld e. CMnd
103 90 submcmn 
 |-  ( ( CCfld e. CMnd /\ NN0 e. ( SubMnd ` CCfld ) ) -> ( CCfld |`s NN0 ) e. CMnd )
104 102 89 103 mp2an 
 |-  ( CCfld |`s NN0 ) e. CMnd
105 104 a1i 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( CCfld |`s NN0 ) e. CMnd )
106 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> I e. V )
107 12 psrbagf 
 |-  ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> e : I --> NN0 )
108 83 107 syl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e : I --> NN0 )
109 simpllr 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
110 12 psrbagf 
 |-  ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> x : I --> NN0 )
111 109 110 syl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> x : I --> NN0 )
112 111 ffnd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> x Fn I )
113 108 ffnd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e Fn I )
114 inidm 
 |-  ( I i^i I ) = I
115 eqidd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( x ` i ) = ( x ` i ) )
116 eqidd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( e ` i ) = ( e ` i ) )
117 112 113 106 106 114 115 116 offval 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) = ( i e. I |-> ( ( x ` i ) - ( e ` i ) ) ) )
118 simpl 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) )
119 simplr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } )
120 breq1 
 |-  ( c = e -> ( c oR <_ x <-> e oR <_ x ) )
121 120 elrab 
 |-  ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } <-> ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ e oR <_ x ) )
122 121 simprbi 
 |-  ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } -> e oR <_ x )
123 119 122 syl 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> e oR <_ x )
124 simpr 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> i e. I )
125 113 112 106 106 114 116 115 ofrval 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ e oR <_ x /\ i e. I ) -> ( e ` i ) <_ ( x ` i ) )
126 118 123 124 125 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( e ` i ) <_ ( x ` i ) )
127 108 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( e ` i ) e. NN0 )
128 111 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( x ` i ) e. NN0 )
129 nn0sub 
 |-  ( ( ( e ` i ) e. NN0 /\ ( x ` i ) e. NN0 ) -> ( ( e ` i ) <_ ( x ` i ) <-> ( ( x ` i ) - ( e ` i ) ) e. NN0 ) )
130 127 128 129 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( ( e ` i ) <_ ( x ` i ) <-> ( ( x ` i ) - ( e ` i ) ) e. NN0 ) )
131 126 130 mpbid 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ i e. I ) -> ( ( x ` i ) - ( e ` i ) ) e. NN0 )
132 117 131 fmpt3d 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) : I --> NN0 )
133 108 ffund 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> Fun e )
134 c0ex 
 |-  0 e. _V
135 106 134 jctir 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( I e. V /\ 0 e. _V ) )
136 frnsuppeq 
 |-  ( ( I e. V /\ 0 e. _V ) -> ( e : I --> NN0 -> ( e supp 0 ) = ( `' e " ( NN0 \ { 0 } ) ) ) )
137 135 108 136 sylc 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e supp 0 ) = ( `' e " ( NN0 \ { 0 } ) ) )
138 dfn2 
 |-  NN = ( NN0 \ { 0 } )
139 138 imaeq2i 
 |-  ( `' e " NN ) = ( `' e " ( NN0 \ { 0 } ) )
140 137 139 eqtr4di 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e supp 0 ) = ( `' e " NN ) )
141 12 psrbag 
 |-  ( I e. V -> ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( e : I --> NN0 /\ ( `' e " NN ) e. Fin ) ) )
142 106 141 syl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( e : I --> NN0 /\ ( `' e " NN ) e. Fin ) ) )
143 83 142 mpbid 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e : I --> NN0 /\ ( `' e " NN ) e. Fin ) )
144 143 simprd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( `' e " NN ) e. Fin )
145 140 144 eqeltrd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e supp 0 ) e. Fin )
146 83 elexd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e e. _V )
147 isfsupp 
 |-  ( ( e e. _V /\ 0 e. _V ) -> ( e finSupp 0 <-> ( Fun e /\ ( e supp 0 ) e. Fin ) ) )
148 146 134 147 sylancl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e finSupp 0 <-> ( Fun e /\ ( e supp 0 ) e. Fin ) ) )
149 133 145 148 mpbir2and 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e finSupp 0 )
150 112 113 106 106 offun 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> Fun ( x oF - e ) )
151 12 psrbagfsupp 
 |-  ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> x finSupp 0 )
152 109 151 syl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> x finSupp 0 )
153 152 149 fsuppunfi 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( x supp 0 ) u. ( e supp 0 ) ) e. Fin )
154 0nn0 
 |-  0 e. NN0
155 154 a1i 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> 0 e. NN0 )
156 0m0e0 
 |-  ( 0 - 0 ) = 0
157 156 a1i 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( 0 - 0 ) = 0 )
158 106 155 111 108 157 suppofssd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( x oF - e ) supp 0 ) C_ ( ( x supp 0 ) u. ( e supp 0 ) ) )
159 153 158 ssfid 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( x oF - e ) supp 0 ) e. Fin )
160 ovexd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) e. _V )
161 isfsupp 
 |-  ( ( ( x oF - e ) e. _V /\ 0 e. _V ) -> ( ( x oF - e ) finSupp 0 <-> ( Fun ( x oF - e ) /\ ( ( x oF - e ) supp 0 ) e. Fin ) ) )
162 160 134 161 sylancl 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( x oF - e ) finSupp 0 <-> ( Fun ( x oF - e ) /\ ( ( x oF - e ) supp 0 ) e. Fin ) ) )
163 150 159 162 mpbir2and 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) finSupp 0 )
164 92 95 99 105 106 108 132 149 163 gsumadd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( CCfld |`s NN0 ) gsum ( e oF + ( x oF - e ) ) ) = ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) )
165 108 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( e ` b ) e. NN0 )
166 165 nn0cnd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( e ` b ) e. CC )
167 111 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( x ` b ) e. NN0 )
168 167 nn0cnd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( x ` b ) e. CC )
169 166 168 pncan3d 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( ( e ` b ) + ( ( x ` b ) - ( e ` b ) ) ) = ( x ` b ) )
170 169 mpteq2dva 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( b e. I |-> ( ( e ` b ) + ( ( x ` b ) - ( e ` b ) ) ) ) = ( b e. I |-> ( x ` b ) ) )
171 fvexd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( e ` b ) e. _V )
172 ovexd 
 |-  ( ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) /\ b e. I ) -> ( ( x ` b ) - ( e ` b ) ) e. _V )
173 108 feqmptd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> e = ( b e. I |-> ( e ` b ) ) )
174 111 feqmptd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> x = ( b e. I |-> ( x ` b ) ) )
175 106 167 165 174 173 offval2 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( x oF - e ) = ( b e. I |-> ( ( x ` b ) - ( e ` b ) ) ) )
176 106 171 172 173 175 offval2 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e oF + ( x oF - e ) ) = ( b e. I |-> ( ( e ` b ) + ( ( x ` b ) - ( e ` b ) ) ) ) )
177 170 176 174 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( e oF + ( x oF - e ) ) = x )
178 177 oveq2d 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( CCfld |`s NN0 ) gsum ( e oF + ( x oF - e ) ) ) = ( ( CCfld |`s NN0 ) gsum x ) )
179 164 178 eqtr3d 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) = ( ( CCfld |`s NN0 ) gsum x ) )
180 simplr 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) )
181 179 180 eqnetrd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) =/= ( M + N ) )
182 oveq12 
 |-  ( ( ( ( CCfld |`s NN0 ) gsum e ) = M /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) -> ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) = ( M + N ) )
183 182 a1i 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( ( ( CCfld |`s NN0 ) gsum e ) = M /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) -> ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) = ( M + N ) ) )
184 183 necon3ad 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( ( ( CCfld |`s NN0 ) gsum e ) + ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) ) =/= ( M + N ) -> -. ( ( ( CCfld |`s NN0 ) gsum e ) = M /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) ) )
185 181 184 mpd 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> -. ( ( ( CCfld |`s NN0 ) gsum e ) = M /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) )
186 neorian 
 |-  ( ( ( ( CCfld |`s NN0 ) gsum e ) =/= M \/ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) <-> -. ( ( ( CCfld |`s NN0 ) gsum e ) = M /\ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) )
187 185 186 sylibr 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( ( CCfld |`s NN0 ) gsum e ) =/= M \/ ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) )
188 62 88 187 mpjaodan 
 |-  ( ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) /\ e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } ) -> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) = ( 0g ` R ) )
189 188 mpteq2dva 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) = ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( 0g ` R ) ) )
190 189 oveq2d 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) = ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( 0g ` R ) ) ) )
191 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
192 5 191 syl 
 |-  ( ph -> R e. Mnd )
193 192 ad2antrr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> R e. Mnd )
194 44 rabex 
 |-  { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } e. _V
195 41 gsumz 
 |-  ( ( R e. Mnd /\ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } e. _V ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
196 193 194 195 sylancl 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
197 190 196 eqtrd 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) = ( 0g ` R ) )
198 197 ex 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) -> ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) = ( 0g ` R ) ) )
199 198 necon1d 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( R gsum ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } |-> ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) ) ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum x ) = ( M + N ) ) )
200 27 199 sylbid 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( P .x. Q ) ` x ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum x ) = ( M + N ) ) )
201 200 ralrimiva 
 |-  ( ph -> A. x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( P .x. Q ) ` x ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum x ) = ( M + N ) ) )
202 6 7 nn0addcld 
 |-  ( ph -> ( M + N ) e. NN0 )
203 2 mplring 
 |-  ( ( I e. V /\ R e. Ring ) -> Y e. Ring )
204 4 5 203 syl2anc 
 |-  ( ph -> Y e. Ring )
205 10 3 ringcl 
 |-  ( ( Y e. Ring /\ P e. ( Base ` Y ) /\ Q e. ( Base ` Y ) ) -> ( P .x. Q ) e. ( Base ` Y ) )
206 204 13 14 205 syl3anc 
 |-  ( ph -> ( P .x. Q ) e. ( Base ` Y ) )
207 1 2 10 41 12 4 5 202 206 ismhp3 
 |-  ( ph -> ( ( P .x. Q ) e. ( H ` ( M + N ) ) <-> A. x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( P .x. Q ) ` x ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum x ) = ( M + N ) ) ) )
208 201 207 mpbird 
 |-  ( ph -> ( P .x. Q ) e. ( H ` ( M + N ) ) )