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 6 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> I e. W )
33 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k e. D )
34 eqid 
 |-  { x e. D | x oR <_ k } = { x e. D | x oR <_ k }
35 5 34 psrbagconcl 
 |-  ( ( I e. W /\ k e. D /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
36 32 33 18 35 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
37 31 36 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. D )
38 eqeq1 
 |-  ( y = ( k oF - X ) -> ( y = Y <-> ( k oF - X ) = Y ) )
39 38 ifbid 
 |-  ( y = ( k oF - X ) -> if ( y = Y , .1. , .0. ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
40 eqid 
 |-  ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( y e. D |-> if ( y = Y , .1. , .0. ) )
41 3 fvexi 
 |-  .0. e. _V
42 28 41 ifex 
 |-  if ( ( k oF - X ) = Y , .1. , .0. ) e. _V
43 39 40 42 fvmpt 
 |-  ( ( k oF - X ) e. D -> ( ( y e. D |-> if ( y = Y , .1. , .0. ) ) ` ( k oF - X ) ) = if ( ( k oF - X ) = Y , .1. , .0. ) )
44 37 43 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. ) )
45 30 44 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. ) ) )
46 eqid 
 |-  ( Base ` R ) = ( Base ` R )
47 46 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
48 46 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
49 47 48 ifcld 
 |-  ( R e. Ring -> if ( ( k oF - X ) = Y , .1. , .0. ) e. ( Base ` R ) )
50 22 49 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> if ( ( k oF - X ) = Y , .1. , .0. ) e. ( Base ` R ) )
51 46 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. ) )
52 22 50 51 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. ) )
53 5 psrbagf 
 |-  ( ( I e. W /\ k e. D ) -> k : I --> NN0 )
54 32 33 53 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k : I --> NN0 )
55 54 ffvelrnda 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
56 6 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
57 8 adantr 
 |-  ( ( ph /\ k e. D ) -> X e. D )
58 5 psrbagf 
 |-  ( ( I e. W /\ X e. D ) -> X : I --> NN0 )
59 56 57 58 syl2anc 
 |-  ( ( ph /\ k e. D ) -> X : I --> NN0 )
60 59 ffvelrnda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. NN0 )
61 60 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( X ` z ) e. NN0 )
62 5 psrbagf 
 |-  ( ( I e. W /\ Y e. D ) -> Y : I --> NN0 )
63 6 10 62 syl2anc 
 |-  ( ph -> Y : I --> NN0 )
64 63 adantr 
 |-  ( ( ph /\ k e. D ) -> Y : I --> NN0 )
65 64 ffvelrnda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
66 65 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
67 nn0cn 
 |-  ( ( k ` z ) e. NN0 -> ( k ` z ) e. CC )
68 nn0cn 
 |-  ( ( X ` z ) e. NN0 -> ( X ` z ) e. CC )
69 nn0cn 
 |-  ( ( Y ` z ) e. NN0 -> ( Y ` z ) e. CC )
70 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 ) ) )
71 67 68 69 70 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 ) ) )
72 55 61 66 71 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 ) ) )
73 eqcom 
 |-  ( ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) <-> ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
74 72 73 syl6bb 
 |-  ( ( ( ( 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 ) ) ) )
75 74 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 ) ) ) )
76 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 ) ) )
77 ovexd 
 |-  ( z e. I -> ( ( k ` z ) - ( X ` z ) ) e. _V )
78 76 77 mprg 
 |-  ( ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) <-> A. z e. I ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) )
79 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 ) ) ) )
80 fvexd 
 |-  ( z e. I -> ( k ` z ) e. _V )
81 79 80 mprg 
 |-  ( ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) <-> A. z e. I ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
82 75 78 81 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 ) ) ) ) )
83 54 feqmptd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k = ( z e. I |-> ( k ` z ) ) )
84 59 feqmptd 
 |-  ( ( ph /\ k e. D ) -> X = ( z e. I |-> ( X ` z ) ) )
85 84 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X = ( z e. I |-> ( X ` z ) ) )
86 32 55 61 83 85 offval2 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) = ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) )
87 64 feqmptd 
 |-  ( ( ph /\ k e. D ) -> Y = ( z e. I |-> ( Y ` z ) ) )
88 87 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> Y = ( z e. I |-> ( Y ` z ) ) )
89 86 88 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 ) ) ) )
90 56 60 65 84 87 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 83 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 82 89 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 45 52 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 50 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 46 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 46 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 sseldi 
 |-  ( ( ( 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 46 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 6 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> I e. W )
116 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> k e. D )
117 5 34 psrbagconcl 
 |-  ( ( I e. W /\ k e. D /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
118 115 116 110 117 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
119 31 118 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. D )
120 114 119 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 ) )
121 46 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 ) )
122 107 112 120 121 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 ) )
123 122 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 ) )
124 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 } )
125 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 } ) = (/) ) )
126 123 124 125 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 } ) = (/) ) )
127 126 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 } ) = (/) )
128 106 127 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 } ) = (/) )
129 128 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 (/) ) )
130 breq1 
 |-  ( x = X -> ( x oR <_ ( X oF + Y ) <-> X oR <_ ( X oF + Y ) ) )
131 60 nn0red 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. RR )
132 nn0addge1 
 |-  ( ( ( X ` z ) e. RR /\ ( Y ` z ) e. NN0 ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
133 131 65 132 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
134 133 ralrimiva 
 |-  ( ( ph /\ k e. D ) -> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
135 ovexd 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( ( X ` z ) + ( Y ` z ) ) e. _V )
136 56 60 135 84 90 ofrfval2 
 |-  ( ( ph /\ k e. D ) -> ( X oR <_ ( X oF + Y ) <-> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) ) )
137 134 136 mpbird 
 |-  ( ( ph /\ k e. D ) -> X oR <_ ( X oF + Y ) )
138 130 57 137 elrabd 
 |-  ( ( ph /\ k e. D ) -> X e. { x e. D | x oR <_ ( X oF + Y ) } )
139 breq2 
 |-  ( k = ( X oF + Y ) -> ( x oR <_ k <-> x oR <_ ( X oF + Y ) ) )
140 139 rabbidv 
 |-  ( k = ( X oF + Y ) -> { x e. D | x oR <_ k } = { x e. D | x oR <_ ( X oF + Y ) } )
141 140 eleq2d 
 |-  ( k = ( X oF + Y ) -> ( X e. { x e. D | x oR <_ k } <-> X e. { x e. D | x oR <_ ( X oF + Y ) } ) )
142 138 141 syl5ibrcom 
 |-  ( ( ph /\ k e. D ) -> ( k = ( X oF + Y ) -> X e. { x e. D | x oR <_ k } ) )
143 142 con3dimp 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> -. k = ( X oF + Y ) )
144 143 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> if ( k = ( X oF + Y ) , .1. , .0. ) = .0. )
145 105 129 144 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. ) )
146 104 145 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. ) )
147 7 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
148 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
149 147 148 syl 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
150 5 psrbaglefi 
 |-  ( ( I e. W /\ k e. D ) -> { x e. D | x oR <_ k } e. Fin )
151 6 150 sylan 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. Fin )
152 ssdif 
 |-  ( { x e. D | x oR <_ k } C_ D -> ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } ) )
153 31 152 ax-mp 
 |-  ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } )
154 153 sseli 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. ( D \ { X } ) )
155 108 adantr 
 |-  ( ( ph /\ k e. D ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
156 eldifsni 
 |-  ( y e. ( D \ { X } ) -> y =/= X )
157 156 adantl 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> y =/= X )
158 157 neneqd 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> -. y = X )
159 158 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> if ( y = X , .1. , .0. ) = .0. )
160 ovex 
 |-  ( NN0 ^m I ) e. _V
161 5 160 rabex2 
 |-  D e. _V
162 161 a1i 
 |-  ( ( ph /\ k e. D ) -> D e. _V )
163 159 162 suppss2 
 |-  ( ( ph /\ k e. D ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) supp .0. ) C_ { X } )
164 41 a1i 
 |-  ( ( ph /\ k e. D ) -> .0. e. _V )
165 155 163 162 164 suppssr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( D \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
166 154 165 sylan2 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
167 166 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 ) ) ) )
168 eldifi 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. { x e. D | x oR <_ k } )
169 46 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. )
170 107 120 169 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. )
171 168 170 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. )
172 167 171 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. )
173 161 rabex 
 |-  { x e. D | x oR <_ k } e. _V
174 173 a1i 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. _V )
175 172 174 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 } )
176 161 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
177 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 ) ) ) )
178 176 177 41 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 )
179 178 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 ) )
180 snfi 
 |-  { X } e. Fin
181 180 a1i 
 |-  ( ( ph /\ k e. D ) -> { X } e. Fin )
182 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. )
183 179 181 175 182 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. )
184 46 3 149 151 123 175 183 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 ) ) ) ) ) )
185 146 184 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 ) ) ) ) ) )
186 185 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 ) ) ) ) ) ) )
187 17 186 syl5eq 
 |-  ( 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 ) ) ) ) ) ) )
188 14 187 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. ) ) )