Metamath Proof Explorer

Theorem mplmonmul

Description: The product of two monomials adds the exponent vectors together. For example, the product of ( x ^ 2 ) ( y ^ 2 ) with ( y ^ 1 ) ( z ^ 3 ) is ( x ^ 2 ) ( y ^ 3 ) ( z ^ 3 ) , where the exponent vectors <. 2 , 2 , 0 >. and <. 0 , 1 , 3 >. are added to give <. 2 , 3 , 3 >. . (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplmon.s 
|- P = ( I mPoly R )
mplmon.b 
|- B = ( Base ` P )
mplmon.z 
|- .0. = ( 0g ` R )
mplmon.o 
|- .1. = ( 1r ` R )
mplmon.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplmon.i 
|- ( ph -> I e. W )
mplmon.r 
|- ( ph -> R e. Ring )
mplmon.x 
|- ( ph -> X e. D )
mplmonmul.t 
|- .x. = ( .r ` P )
mplmonmul.x 
|- ( ph -> Y e. D )
Assertion mplmonmul 
|- ( ph -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) .x. ( y e. D |-> if ( y = Y , .1. , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mplmon.s 
 |-  P = ( I mPoly R )
2 mplmon.b 
 |-  B = ( Base ` P )
3 mplmon.z 
 |-  .0. = ( 0g ` R )
4 mplmon.o 
 |-  .1. = ( 1r ` R )
5 mplmon.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
6 mplmon.i 
 |-  ( ph -> I e. W )
7 mplmon.r 
 |-  ( ph -> R e. Ring )
8 mplmon.x 
 |-  ( ph -> X e. D )
9 mplmonmul.t 
 |-  .x. = ( .r ` P )
10 mplmonmul.x 
 |-  ( ph -> Y e. D )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 1 2 3 4 5 6 7 8 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )
13 1 2 3 4 5 6 7 10 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) e. B )
14 1 2 11 9 5 12 13 mplmul 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) .x. ( y e. D |-> if ( y = Y , .1. , .0. ) ) ) = ( k e. D |-> ( R gsum ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) ) )
15 eqeq1 
 |-  ( y = k -> ( y = ( X oF + Y ) <-> k = ( X oF + Y ) ) )
16 15 ifbid 
 |-  ( y = k -> if ( y = ( X oF + Y ) , .1. , .0. ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
17 16 cbvmptv 
 |-  ( y e. D |-> if ( y = ( X oF + Y ) , .1. , .0. ) ) = ( k e. D |-> if ( k = ( X oF + Y ) , .1. , .0. ) )
18 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X e. { x e. D | x oR <_ k } )
19 18 snssd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> { X } C_ { x e. D | x oR <_ k } )
20 19 resmptd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) = ( j e. { X } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) )
21 20 oveq2d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = ( R gsum ( j e. { X } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) )
22 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> R e. Ring )
23 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
24 22 23 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> R e. Mnd )
25 8 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X e. D )
26 iftrue 
 |-  ( y = X -> if ( y = X , .1. , .0. ) = .1. )
27 eqid 
 |-  ( y e. D |-> if ( y = X , .1. , .0. ) ) = ( y e. D |-> if ( y = X , .1. , .0. ) )
28 4 fvexi 
 |-  .1. e. _V
29 26 27 28 fvmpt 
 |-  ( X e. D -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) = .1. )
30 25 29 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) = .1. )
31 ssrab2 
 |-  { x e. D | x oR <_ k } C_ D
32 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k e. D )
33 eqid 
 |-  { x e. D | x oR <_ k } = { x e. D | x oR <_ k }
34 5 33 psrbagconcl 
 |-  ( ( k e. D /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
35 32 18 34 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
36 31 35 sselid 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. D )
37 eqeq1 
 |-  ( y = ( k oF - X ) -> ( y = Y <-> ( k oF - X ) = Y ) )
38 37 ifbid 
 |-  ( y = ( k oF - X ) -> if ( y = Y , .1. , .0. ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
39 eqid 
 |-  ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( y e. D |-> if ( y = Y , .1. , .0. ) )
40 3 fvexi 
 |-  .0. e. _V
41 28 40 ifex 
 |-  if ( ( k oF - X ) = Y , .1. , .0. ) e. _V
42 38 39 41 fvmpt 
 |-  ( ( k oF - X ) e. D -> ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
43 36 42 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
44 30 43 oveq12d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) = ( .1. ( .r ` R ) if ( ( k oF - X ) = Y , .1. , .0. ) ) )
45 eqid 
 |-  ( Base ` R ) = ( Base ` R )
46 45 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
47 45 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
48 46 47 ifcld 
 |-  ( R e. Ring -> if ( ( k oF - X ) = Y , .1. , .0. ) e. ( Base ` R ) )
49 22 48 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> if ( ( k oF - X ) = Y , .1. , .0. ) e. ( Base ` R ) )
50 45 11 4 ringlidm 
 |-  ( ( R e. Ring /\ if ( ( k oF - X ) = Y , .1. , .0. ) e. ( Base ` R ) ) -> ( .1. ( .r ` R ) if ( ( k oF - X ) = Y , .1. , .0. ) ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
51 22 49 50 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( .1. ( .r ` R ) if ( ( k oF - X ) = Y , .1. , .0. ) ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
52 5 psrbagf 
 |-  ( k e. D -> k : I --> NN0 )
53 32 52 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k : I --> NN0 )
54 53 ffvelrnda 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
55 8 adantr 
 |-  ( ( ph /\ k e. D ) -> X e. D )
56 5 psrbagf 
 |-  ( X e. D -> X : I --> NN0 )
57 55 56 syl 
 |-  ( ( ph /\ k e. D ) -> X : I --> NN0 )
58 57 ffvelrnda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. NN0 )
59 58 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( X ` z ) e. NN0 )
60 5 psrbagf 
 |-  ( Y e. D -> Y : I --> NN0 )
61 10 60 syl 
 |-  ( ph -> Y : I --> NN0 )
62 61 adantr 
 |-  ( ( ph /\ k e. D ) -> Y : I --> NN0 )
63 62 ffvelrnda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
64 63 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
65 nn0cn 
 |-  ( ( k ` z ) e. NN0 -> ( k ` z ) e. CC )
66 nn0cn 
 |-  ( ( X ` z ) e. NN0 -> ( X ` z ) e. CC )
67 nn0cn 
 |-  ( ( Y ` z ) e. NN0 -> ( Y ` z ) e. CC )
68 subadd 
 |-  ( ( ( k ` z ) e. CC /\ ( X ` z ) e. CC /\ ( Y ` z ) e. CC ) -> ( ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) <-> ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) ) )
69 65 66 67 68 syl3an 
 |-  ( ( ( k ` z ) e. NN0 /\ ( X ` z ) e. NN0 /\ ( Y ` z ) e. NN0 ) -> ( ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) <-> ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) ) )
70 54 59 64 69 syl3anc 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) <-> ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) ) )
71 eqcom 
 |-  ( ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) <-> ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
72 70 71 bitrdi 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) <-> ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) ) )
73 72 ralbidva 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( A. z e. I ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) <-> A. z e. I ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) ) )
74 mpteqb 
 |-  ( A. z e. I ( ( k ` z ) - ( X ` z ) ) e. _V -> ( ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) <-> A. z e. I ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) ) )
75 ovexd 
 |-  ( z e. I -> ( ( k ` z ) - ( X ` z ) ) e. _V )
76 74 75 mprg 
 |-  ( ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) <-> A. z e. I ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) )
77 mpteqb 
 |-  ( A. z e. I ( k ` z ) e. _V -> ( ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) <-> A. z e. I ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) ) )
78 fvexd 
 |-  ( z e. I -> ( k ` z ) e. _V )
79 77 78 mprg 
 |-  ( ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) <-> A. z e. I ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
80 73 76 79 3bitr4g 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) <-> ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) ) )
81 6 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> I e. W )
82 53 feqmptd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k = ( z e. I |-> ( k ` z ) ) )
83 57 feqmptd 
 |-  ( ( ph /\ k e. D ) -> X = ( z e. I |-> ( X ` z ) ) )
84 83 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X = ( z e. I |-> ( X ` z ) ) )
85 81 54 59 82 84 offval2 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) = ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) )
86 62 feqmptd 
 |-  ( ( ph /\ k e. D ) -> Y = ( z e. I |-> ( Y ` z ) ) )
87 86 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> Y = ( z e. I |-> ( Y ` z ) ) )
88 85 87 eqeq12d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( k oF - X ) = Y <-> ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) ) )
89 6 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
90 89 58 63 83 86 offval2 
 |-  ( ( ph /\ k e. D ) -> ( X oF + Y ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) )
91 90 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( X oF + Y ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) )
92 82 91 eqeq12d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k = ( X oF + Y ) <-> ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) ) )
93 80 88 92 3bitr4d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( k oF - X ) = Y <-> k = ( X oF + Y ) ) )
94 93 ifbid 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> if ( ( k oF - X ) = Y , .1. , .0. ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
95 44 51 94 3eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
96 94 49 eqeltrrd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> if ( k = ( X oF + Y ) , .1. , .0. ) e. ( Base ` R ) )
97 95 96 eqeltrd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) e. ( Base ` R ) )
98 fveq2 
 |-  ( j = X -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) )
99 oveq2 
 |-  ( j = X -> ( k oF - j ) = ( k oF - X ) )
100 99 fveq2d 
 |-  ( j = X -> ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) = ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) )
101 98 100 oveq12d 
 |-  ( j = X -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) )
102 45 101 gsumsn 
 |-  ( ( R e. Mnd /\ X e. D /\ ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) e. ( Base ` R ) ) -> ( R gsum ( j e. { X } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) = ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) )
103 24 25 97 102 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( R gsum ( j e. { X } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) = ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) ) )
104 21 103 95 3eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
105 3 gsum0 
 |-  ( R gsum (/) ) = .0.
106 disjsn 
 |-  ( ( { x e. D | x oR <_ k } i^i { X } ) = (/) <-> -. X e. { x e. D | x oR <_ k } )
107 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> R e. Ring )
108 1 45 2 5 12 mplelf 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
109 108 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
110 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> j e. { x e. D | x oR <_ k } )
111 31 110 sselid 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> j e. D )
112 109 111 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) e. ( Base ` R ) )
113 1 45 2 5 13 mplelf 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) : D --> ( Base ` R ) )
114 113 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) : D --> ( Base ` R ) )
115 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> k e. D )
116 5 33 psrbagconcl 
 |-  ( ( k e. D /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
117 115 110 116 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
118 31 117 sselid 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. D )
119 114 118 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) e. ( Base ` R ) )
120 45 11 ringcl 
 |-  ( ( R e. Ring /\ ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) e. ( Base ` R ) /\ ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) e. ( Base ` R ) ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) e. ( Base ` R ) )
121 107 112 119 120 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) e. ( Base ` R ) )
122 121 fmpttd 
 |-  ( ( ph /\ k e. D ) -> ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) : { x e. D | x oR <_ k } --> ( Base ` R ) )
123 ffn 
 |-  ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) : { x e. D | x oR <_ k } --> ( Base ` R ) -> ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) Fn { x e. D | x oR <_ k } )
124 fnresdisj 
 |-  ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) Fn { x e. D | x oR <_ k } -> ( ( { x e. D | x oR <_ k } i^i { X } ) = (/) <-> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) = (/) ) )
125 122 123 124 3syl 
 |-  ( ( ph /\ k e. D ) -> ( ( { x e. D | x oR <_ k } i^i { X } ) = (/) <-> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) = (/) ) )
126 125 biimpa 
 |-  ( ( ( ph /\ k e. D ) /\ ( { x e. D | x oR <_ k } i^i { X } ) = (/) ) -> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) = (/) )
127 106 126 sylan2br 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) = (/) )
128 127 oveq2d 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = ( R gsum (/) ) )
129 breq1 
 |-  ( x = X -> ( x oR <_ ( X oF + Y ) <-> X oR <_ ( X oF + Y ) ) )
130 58 nn0red 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. RR )
131 nn0addge1 
 |-  ( ( ( X ` z ) e. RR /\ ( Y ` z ) e. NN0 ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
132 130 63 131 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
133 132 ralrimiva 
 |-  ( ( ph /\ k e. D ) -> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
134 ovexd 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( ( X ` z ) + ( Y ` z ) ) e. _V )
135 89 58 134 83 90 ofrfval2 
 |-  ( ( ph /\ k e. D ) -> ( X oR <_ ( X oF + Y ) <-> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) ) )
136 133 135 mpbird 
 |-  ( ( ph /\ k e. D ) -> X oR <_ ( X oF + Y ) )
137 129 55 136 elrabd 
 |-  ( ( ph /\ k e. D ) -> X e. { x e. D | x oR <_ ( X oF + Y ) } )
138 breq2 
 |-  ( k = ( X oF + Y ) -> ( x oR <_ k <-> x oR <_ ( X oF + Y ) ) )
139 138 rabbidv 
 |-  ( k = ( X oF + Y ) -> { x e. D | x oR <_ k } = { x e. D | x oR <_ ( X oF + Y ) } )
140 139 eleq2d 
 |-  ( k = ( X oF + Y ) -> ( X e. { x e. D | x oR <_ k } <-> X e. { x e. D | x oR <_ ( X oF + Y ) } ) )
141 137 140 syl5ibrcom 
 |-  ( ( ph /\ k e. D ) -> ( k = ( X oF + Y ) -> X e. { x e. D | x oR <_ k } ) )
142 141 con3dimp 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> -. k = ( X oF + Y ) )
143 142 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> if ( k = ( X oF + Y ) , .1. , .0. ) = .0. )
144 105 128 143 3eqtr4a 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
145 104 144 pm2.61dan 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
146 7 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
147 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
148 146 147 syl 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
149 5 psrbaglefi 
 |-  ( k e. D -> { x e. D | x oR <_ k } e. Fin )
150 149 adantl 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. Fin )
151 ssdif 
 |-  ( { x e. D | x oR <_ k } C_ D -> ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } ) )
152 31 151 ax-mp 
 |-  ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } )
153 152 sseli 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. ( D \ { X } ) )
154 108 adantr 
 |-  ( ( ph /\ k e. D ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
155 eldifsni 
 |-  ( y e. ( D \ { X } ) -> y =/= X )
156 155 adantl 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> y =/= X )
157 156 neneqd 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> -. y = X )
158 157 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> if ( y = X , .1. , .0. ) = .0. )
159 ovex 
 |-  ( NN0 ^m I ) e. _V
160 5 159 rabex2 
 |-  D e. _V
161 160 a1i 
 |-  ( ( ph /\ k e. D ) -> D e. _V )
162 158 161 suppss2 
 |-  ( ( ph /\ k e. D ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) supp .0. ) C_ { X } )
163 40 a1i 
 |-  ( ( ph /\ k e. D ) -> .0. e. _V )
164 154 162 161 163 suppssr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( D \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
165 153 164 sylan2 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
166 165 oveq1d 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = ( .0. ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) )
167 eldifi 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. { x e. D | x oR <_ k } )
168 45 11 3 ringlz 
 |-  ( ( R e. Ring /\ ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = .0. )
169 107 119 168 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( .0. ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = .0. )
170 167 169 sylan2 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( .0. ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = .0. )
171 166 170 eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) = .0. )
172 160 rabex 
 |-  { x e. D | x oR <_ k } e. _V
173 172 a1i 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. _V )
174 171 173 suppss2 
 |-  ( ( ph /\ k e. D ) -> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) supp .0. ) C_ { X } )
175 160 mptrabex 
 |-  ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) e. _V
176 funmpt 
 |-  Fun ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) )
177 175 176 40 3pm3.2i 
 |-  ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) e. _V /\ Fun ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) /\ .0. e. _V )
178 177 a1i 
 |-  ( ( ph /\ k e. D ) -> ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) e. _V /\ Fun ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) /\ .0. e. _V ) )
179 snfi 
 |-  { X } e. Fin
180 179 a1i 
 |-  ( ( ph /\ k e. D ) -> { X } e. Fin )
181 suppssfifsupp 
 |-  ( ( ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) e. _V /\ Fun ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) /\ .0. e. _V ) /\ ( { X } e. Fin /\ ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) supp .0. ) C_ { X } ) ) -> ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) finSupp .0. )
182 178 180 174 181 syl12anc 
 |-  ( ( ph /\ k e. D ) -> ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) finSupp .0. )
183 45 3 148 150 122 174 182 gsumres 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) |` { X } ) ) = ( R gsum ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) )
184 145 183 eqtr3d 
 |-  ( ( ph /\ k e. D ) -> if ( k = ( X oF + Y ) , .1. , .0. ) = ( R gsum ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) )
185 184 mpteq2dva 
 |-  ( ph -> ( k e. D |-> if ( k = ( X oF + Y ) , .1. , .0. ) ) = ( k e. D |-> ( R gsum ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) ) )
186 17 185 eqtrid 
 |-  ( ph -> ( y e. D |-> if ( y = ( X oF + Y ) , .1. , .0. ) ) = ( k e. D |-> ( R gsum ( j e. { x e. D | x oR <_ k } |-> ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) ( .r ` R ) ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - j ) ) ) ) ) ) )
187 14 186 eqtr4d 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) .x. ( y e. D |-> if ( y = Y , .1. , .0. ) ) ) = ( y e. D |-> if ( y = ( X oF + Y ) , .1. , .0. ) ) )