| 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 ) ) ) |