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) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

Ref Expression
Hypotheses mhpmulcl.h 
|- H = ( I mHomP R )
mhpmulcl.y 
|- Y = ( I mPoly R )
mhpmulcl.t 
|- .x. = ( .r ` Y )
mhpmulcl.r 
|- ( ph -> R e. Ring )
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.r 
 |-  ( ph -> R e. Ring )
5 mhpmulcl.p 
 |-  ( ph -> P e. ( H ` M ) )
6 mhpmulcl.q 
 |-  ( ph -> Q e. ( H ` N ) )
7 breq2 
 |-  ( d = x -> ( c oR <_ d <-> c oR <_ x ) )
8 7 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 } )
9 fvoveq1 
 |-  ( d = x -> ( Q ` ( d oF - e ) ) = ( Q ` ( x oF - e ) ) )
10 9 oveq2d 
 |-  ( d = x -> ( ( P ` e ) ( .r ` R ) ( Q ` ( d oF - e ) ) ) = ( ( P ` e ) ( .r ` R ) ( Q ` ( x oF - e ) ) ) )
11 8 10 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 ) ) ) ) )
12 11 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 ) ) ) ) ) )
13 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
16 1 2 13 5 mhpmpl 
 |-  ( ph -> P e. ( Base ` Y ) )
17 1 2 13 6 mhpmpl 
 |-  ( ph -> Q e. ( Base ` Y ) )
18 2 13 14 3 15 16 17 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 ) ) ) ) ) ) )
19 18 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 ) ) ) ) ) ) )
20 simpr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
21 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 )
22 12 19 20 21 fvmptd4 
 |-  ( ( 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 ) ) ) ) ) )
23 22 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 ) ) )
24 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 )
25 oveq2 
 |-  ( c = e -> ( ( CCfld |`s NN0 ) gsum c ) = ( ( CCfld |`s NN0 ) gsum e ) )
26 25 eqeq1d 
 |-  ( c = e -> ( ( ( CCfld |`s NN0 ) gsum c ) = M <-> ( ( CCfld |`s NN0 ) gsum e ) = M ) )
27 26 necon3bbid 
 |-  ( c = e -> ( -. ( ( CCfld |`s NN0 ) gsum c ) = M <-> ( ( CCfld |`s NN0 ) gsum e ) =/= M ) )
28 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 } )
29 28 ad2antlr 
 |-  ( ( ( ( ( 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 } )
30 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 )
31 27 29 30 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 } )
32 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 }
33 31 32 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 } ) )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 2 34 13 15 16 mplelf 
 |-  ( ph -> P : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
36 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
37 1 36 15 5 mhpdeg 
 |-  ( ph -> ( P supp ( 0g ` R ) ) C_ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = M } )
38 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
39 35 37 5 38 suppssrg 
 |-  ( ( 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 ) )
40 24 33 39 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 ) )
41 40 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 ) ) ) )
42 4 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 )
43 17 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 ) )
44 2 34 13 15 43 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 ) )
45 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 }
46 15 45 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 } )
47 46 ad5ant24 
 |-  ( ( ( ( ( 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 } )
48 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 } )
49 47 48 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 } )
50 44 49 ffvelcdmd 
 |-  ( ( ( ( ( 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 ) )
51 34 14 36 42 50 ringlzd 
 |-  ( ( ( ( ( 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 ) )
52 41 51 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 ) )
53 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 )
54 oveq2 
 |-  ( c = ( x oF - e ) -> ( ( CCfld |`s NN0 ) gsum c ) = ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) )
55 54 eqeq1d 
 |-  ( c = ( x oF - e ) -> ( ( ( CCfld |`s NN0 ) gsum c ) = N <-> ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) = N ) )
56 55 necon3bbid 
 |-  ( c = ( x oF - e ) -> ( -. ( ( CCfld |`s NN0 ) gsum c ) = N <-> ( ( CCfld |`s NN0 ) gsum ( x oF - e ) ) =/= N ) )
57 46 ad5ant24 
 |-  ( ( ( ( ( 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 } )
58 57 48 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 } )
59 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 )
60 56 58 59 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 } )
61 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 }
62 60 61 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 } ) )
63 2 34 13 15 17 mplelf 
 |-  ( ph -> Q : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
64 1 36 15 6 mhpdeg 
 |-  ( ph -> ( Q supp ( 0g ` R ) ) C_ { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum c ) = N } )
65 63 64 6 38 suppssrg 
 |-  ( ( 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 ) )
66 53 62 65 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 ) )
67 66 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 ) ) )
68 4 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 )
69 16 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 ) )
70 2 34 13 15 69 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 ) )
71 28 ad2antlr 
 |-  ( ( ( ( ( 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 } )
72 70 71 ffvelcdmd 
 |-  ( ( ( ( ( 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 ) )
73 34 14 36 68 72 ringrzd 
 |-  ( ( ( ( ( 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 ) )
74 67 73 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 ) )
75 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
76 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
77 76 submbas 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> NN0 = ( Base ` ( CCfld |`s NN0 ) ) )
78 75 77 ax-mp 
 |-  NN0 = ( Base ` ( CCfld |`s NN0 ) )
79 cnfld0 
 |-  0 = ( 0g ` CCfld )
80 76 79 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
81 75 80 ax-mp 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
82 nn0ex 
 |-  NN0 e. _V
83 cnfldadd 
 |-  + = ( +g ` CCfld )
84 76 83 ressplusg 
 |-  ( NN0 e. _V -> + = ( +g ` ( CCfld |`s NN0 ) ) )
85 82 84 ax-mp 
 |-  + = ( +g ` ( CCfld |`s NN0 ) )
86 cnring 
 |-  CCfld e. Ring
87 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
88 86 87 ax-mp 
 |-  CCfld e. CMnd
89 76 submcmn 
 |-  ( ( CCfld e. CMnd /\ NN0 e. ( SubMnd ` CCfld ) ) -> ( CCfld |`s NN0 ) e. CMnd )
90 88 75 89 mp2an 
 |-  ( CCfld |`s NN0 ) e. CMnd
91 90 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 )
92 reldmmhp 
 |-  Rel dom mHomP
93 92 1 5 elfvov1 
 |-  ( ph -> I e. _V )
94 93 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 )
95 28 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 } )
96 15 psrbagf 
 |-  ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> e : I --> NN0 )
97 95 96 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 )
98 15 psrbagf 
 |-  ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> x : I --> NN0 )
99 98 ad3antlr 
 |-  ( ( ( ( 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 )
100 99 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 )
101 97 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 )
102 inidm 
 |-  ( I i^i I ) = I
103 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 ) )
104 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 ) )
105 100 101 94 94 102 103 104 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 ) ) ) )
106 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 } ) )
107 breq1 
 |-  ( c = e -> ( c oR <_ x <-> e oR <_ x ) )
108 107 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 ) )
109 108 simprbi 
 |-  ( e e. { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } -> e oR <_ x )
110 109 ad2antlr 
 |-  ( ( ( ( ( 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 )
111 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 )
112 101 100 94 94 102 104 103 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 ) )
113 106 110 111 112 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 ) )
114 97 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
115 99 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
116 nn0sub 
 |-  ( ( ( e ` i ) e. NN0 /\ ( x ` i ) e. NN0 ) -> ( ( e ` i ) <_ ( x ` i ) <-> ( ( x ` i ) - ( e ` i ) ) e. NN0 ) )
117 114 115 116 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 ) )
118 113 117 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 )
119 105 118 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 )
120 97 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 )
121 c0ex 
 |-  0 e. _V
122 94 121 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 ) )
123 fsuppeq 
 |-  ( ( I e. _V /\ 0 e. _V ) -> ( e : I --> NN0 -> ( e supp 0 ) = ( `' e " ( NN0 \ { 0 } ) ) ) )
124 122 97 123 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 } ) ) )
125 dfn2 
 |-  NN = ( NN0 \ { 0 } )
126 125 imaeq2i 
 |-  ( `' e " NN ) = ( `' e " ( NN0 \ { 0 } ) )
127 124 126 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 ) )
128 15 psrbag 
 |-  ( I e. _V -> ( e e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( e : I --> NN0 /\ ( `' e " NN ) e. Fin ) ) )
129 94 128 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 ) ) )
130 95 129 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 ) )
131 130 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 )
132 127 131 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 )
133 95 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 )
134 isfsupp 
 |-  ( ( e e. _V /\ 0 e. _V ) -> ( e finSupp 0 <-> ( Fun e /\ ( e supp 0 ) e. Fin ) ) )
135 133 121 134 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 ) ) )
136 120 132 135 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 )
137 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 )
138 0nn0 
 |-  0 e. NN0
139 138 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 )
140 100 101 94 94 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 ) )
141 15 psrbagfsupp 
 |-  ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> x finSupp 0 )
142 141 ad3antlr 
 |-  ( ( ( ( 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 )
143 142 136 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 )
144 0m0e0 
 |-  ( 0 - 0 ) = 0
145 144 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 )
146 94 139 99 97 145 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 ) ) )
147 143 146 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 )
148 137 139 140 147 isfsuppd 
 |-  ( ( ( ( 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 )
149 78 81 85 91 94 97 119 136 148 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 ) ) ) )
150 97 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
151 150 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 )
152 99 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
153 152 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 )
154 151 153 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 ) )
155 154 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 ) ) )
156 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 )
157 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 )
158 97 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 ) ) )
159 99 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 ) ) )
160 94 152 150 159 158 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 ) ) ) )
161 94 156 157 158 160 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 ) ) ) ) )
162 155 161 159 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 )
163 162 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 ) )
164 149 163 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 ) )
165 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 ) )
166 164 165 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 ) )
167 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 ) )
168 167 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 ) ) )
169 168 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 ) ) )
170 166 169 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 ) )
171 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 ) )
172 170 171 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 ) )
173 52 74 172 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 ) )
174 173 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 ) ) )
175 174 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 ) ) ) )
176 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
177 4 176 syl 
 |-  ( ph -> R e. Mnd )
178 177 ad2antrr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ ( ( CCfld |`s NN0 ) gsum x ) =/= ( M + N ) ) -> R e. Mnd )
179 ovex 
 |-  ( NN0 ^m I ) e. _V
180 179 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
181 180 rabex 
 |-  { c e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | c oR <_ x } e. _V
182 36 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 ) )
183 178 181 182 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 ) )
184 175 183 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 ) )
185 184 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 ) ) )
186 185 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 ) ) )
187 23 186 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 ) ) )
188 187 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 ) ) )
189 1 5 mhprcl 
 |-  ( ph -> M e. NN0 )
190 1 6 mhprcl 
 |-  ( ph -> N e. NN0 )
191 189 190 nn0addcld 
 |-  ( ph -> ( M + N ) e. NN0 )
192 2 93 4 mplringd 
 |-  ( ph -> Y e. Ring )
193 13 3 192 16 17 ringcld 
 |-  ( ph -> ( P .x. Q ) e. ( Base ` Y ) )
194 1 2 13 36 15 191 193 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 ) ) ) )
195 188 194 mpbird 
 |-  ( ph -> ( P .x. Q ) e. ( H ` ( M + N ) ) )