Metamath Proof Explorer

Theorem psrmonmul

Description: The product of two power series 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 Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrmon.s 
|- S = ( I mPwSer R )
psrmon.b 
|- B = ( Base ` S )
psrmon.z 
|- .0. = ( 0g ` R )
psrmon.o 
|- .1. = ( 1r ` R )
psrmon.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
psrmon.i 
|- ( ph -> I e. W )
psrmon.r 
|- ( ph -> R e. Ring )
psrmon.x 
|- ( ph -> X e. D )
psrmonmul.t 
|- .x. = ( .r ` S )
psrmonmul.y 
|- ( ph -> Y e. D )
Assertion psrmonmul 
|- ( 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 psrmon.s 
 |-  S = ( I mPwSer R )
2 psrmon.b 
 |-  B = ( Base ` S )
3 psrmon.z 
 |-  .0. = ( 0g ` R )
4 psrmon.o 
 |-  .1. = ( 1r ` R )
5 psrmon.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6 psrmon.i 
 |-  ( ph -> I e. W )
7 psrmon.r 
 |-  ( ph -> R e. Ring )
8 psrmon.x 
 |-  ( ph -> X e. D )
9 psrmonmul.t 
 |-  .x. = ( .r ` S )
10 psrmonmul.y 
 |-  ( ph -> Y e. D )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 5 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
13 1 2 3 4 5 6 7 8 psrmon 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )
14 1 2 3 4 5 6 7 10 psrmon 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) e. B )
15 1 2 11 9 12 13 14 psrmulfval 
 |-  ( 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 ) ) ) ) ) ) )
16 eqeq1 
 |-  ( y = k -> ( y = ( X oF + Y ) <-> k = ( X oF + Y ) ) )
17 16 ifbid 
 |-  ( y = k -> if ( y = ( X oF + Y ) , .1. , .0. ) = if ( k = ( X oF + Y ) , .1. , .0. ) )
18 17 cbvmptv 
 |-  ( y e. D |-> if ( y = ( X oF + Y ) , .1. , .0. ) ) = ( k e. D |-> if ( k = ( X oF + Y ) , .1. , .0. ) )
19 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X e. { x e. D | x oR <_ k } )
20 19 snssd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> { X } C_ { x e. D | x oR <_ k } )
21 20 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 ) ) ) ) )
22 21 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 ) ) ) ) ) )
23 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> R e. Ring )
24 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
25 23 24 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> R e. Mnd )
26 8 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X e. D )
27 iftrue 
 |-  ( y = X -> if ( y = X , .1. , .0. ) = .1. )
28 eqid 
 |-  ( y e. D |-> if ( y = X , .1. , .0. ) ) = ( y e. D |-> if ( y = X , .1. , .0. ) )
29 4 fvexi 
 |-  .1. e. _V
30 27 28 29 fvmpt 
 |-  ( X e. D -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) = .1. )
31 26 30 syl 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) = .1. )
32 ssrab2 
 |-  { x e. D | x oR <_ k } C_ D
33 eqid 
 |-  { x e. D | x oR <_ k } = { x e. D | x oR <_ k }
34 12 33 psrbagconcl 
 |-  ( ( k e. D /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
35 34 adantll 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) e. { x e. D | x oR <_ k } )
36 32 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 29 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 31 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 23 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 23 49 ringlidmd 
 |-  ( ( ( 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. ) )
51 12 psrbagf 
 |-  ( k e. D -> k : I --> NN0 )
52 51 ad2antlr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k : I --> NN0 )
53 52 ffvelcdmda 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
54 8 adantr 
 |-  ( ( ph /\ k e. D ) -> X e. D )
55 12 psrbagf 
 |-  ( X e. D -> X : I --> NN0 )
56 54 55 syl 
 |-  ( ( ph /\ k e. D ) -> X : I --> NN0 )
57 56 ffvelcdmda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. NN0 )
58 57 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( X ` z ) e. NN0 )
59 12 psrbagf 
 |-  ( Y e. D -> Y : I --> NN0 )
60 10 59 syl 
 |-  ( ph -> Y : I --> NN0 )
61 60 adantr 
 |-  ( ( ph /\ k e. D ) -> Y : I --> NN0 )
62 61 ffvelcdmda 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
63 62 adantlr 
 |-  ( ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) /\ z e. I ) -> ( Y ` z ) e. NN0 )
64 nn0cn 
 |-  ( ( k ` z ) e. NN0 -> ( k ` z ) e. CC )
65 nn0cn 
 |-  ( ( X ` z ) e. NN0 -> ( X ` z ) e. CC )
66 nn0cn 
 |-  ( ( Y ` z ) e. NN0 -> ( Y ` z ) e. CC )
67 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 ) ) )
68 64 65 66 67 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 ) ) )
69 53 58 63 68 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 ) ) )
70 eqcom 
 |-  ( ( ( X ` z ) + ( Y ` z ) ) = ( k ` z ) <-> ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
71 69 70 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 ) ) ) )
72 71 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 ) ) ) )
73 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 ) ) )
74 ovexd 
 |-  ( z e. I -> ( ( k ` z ) - ( X ` z ) ) e. _V )
75 73 74 mprg 
 |-  ( ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) = ( z e. I |-> ( Y ` z ) ) <-> A. z e. I ( ( k ` z ) - ( X ` z ) ) = ( Y ` z ) )
76 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 ) ) ) )
77 fvexd 
 |-  ( z e. I -> ( k ` z ) e. _V )
78 76 77 mprg 
 |-  ( ( z e. I |-> ( k ` z ) ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) <-> A. z e. I ( k ` z ) = ( ( X ` z ) + ( Y ` z ) ) )
79 72 75 78 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 ) ) ) ) )
80 6 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> I e. W )
81 52 feqmptd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> k = ( z e. I |-> ( k ` z ) ) )
82 56 feqmptd 
 |-  ( ( ph /\ k e. D ) -> X = ( z e. I |-> ( X ` z ) ) )
83 82 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> X = ( z e. I |-> ( X ` z ) ) )
84 80 53 58 81 83 offval2 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( k oF - X ) = ( z e. I |-> ( ( k ` z ) - ( X ` z ) ) ) )
85 61 feqmptd 
 |-  ( ( ph /\ k e. D ) -> Y = ( z e. I |-> ( Y ` z ) ) )
86 85 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> Y = ( z e. I |-> ( Y ` z ) ) )
87 84 86 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 ) ) ) )
88 6 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
89 88 57 62 82 85 offval2 
 |-  ( ( ph /\ k e. D ) -> ( X oF + Y ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) )
90 89 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( X oF + Y ) = ( z e. I |-> ( ( X ` z ) + ( Y ` z ) ) ) )
91 81 90 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 ) ) ) ) )
92 79 87 91 3bitr4d 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> ( ( k oF - X ) = Y <-> k = ( X oF + Y ) ) )
93 92 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. ) )
94 44 50 93 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. ) )
95 93 49 eqeltrrd 
 |-  ( ( ( ph /\ k e. D ) /\ X e. { x e. D | x oR <_ k } ) -> if ( k = ( X oF + Y ) , .1. , .0. ) e. ( Base ` R ) )
96 94 95 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 ) )
97 fveq2 
 |-  ( j = X -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` X ) )
98 oveq2 
 |-  ( j = X -> ( k oF - j ) = ( k oF - X ) )
99 98 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 ) ) )
100 97 99 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 ) ) ) )
101 45 100 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 ) ) ) )
102 25 26 96 101 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 ) ) ) )
103 22 102 94 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. ) )
104 3 gsum0 
 |-  ( R gsum (/) ) = .0.
105 disjsn 
 |-  ( ( { x e. D | x oR <_ k } i^i { X } ) = (/) <-> -. X e. { x e. D | x oR <_ k } )
106 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> R e. Ring )
107 1 45 12 2 13 psrelbas 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
108 107 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
109 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> j e. { x e. D | x oR <_ k } )
110 32 109 sselid 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> j e. D )
111 108 110 ffvelcdmd 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) e. ( Base ` R ) )
112 1 45 12 2 14 psrelbas 
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) : D --> ( Base ` R ) )
113 112 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) : D --> ( Base ` R ) )
114 12 33 psrbagconcl 
 |-  ( ( k e. D /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
115 114 adantll 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. { x e. D | x oR <_ k } )
116 32 115 sselid 
 |-  ( ( ( ph /\ k e. D ) /\ j e. { x e. D | x oR <_ k } ) -> ( k oF - j ) e. D )
117 113 116 ffvelcdmd 
 |-  ( ( ( 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 ) )
118 45 11 106 111 117 ringcld 
 |-  ( ( ( 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 ) )
119 118 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 ) )
120 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 } )
121 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 } ) = (/) ) )
122 119 120 121 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 } ) = (/) ) )
123 122 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 } ) = (/) )
124 105 123 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 } ) = (/) )
125 124 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 (/) ) )
126 breq1 
 |-  ( x = X -> ( x oR <_ ( X oF + Y ) <-> X oR <_ ( X oF + Y ) ) )
127 57 nn0red 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) e. RR )
128 nn0addge1 
 |-  ( ( ( X ` z ) e. RR /\ ( Y ` z ) e. NN0 ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
129 127 62 128 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
130 129 ralrimiva 
 |-  ( ( ph /\ k e. D ) -> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) )
131 ovexd 
 |-  ( ( ( ph /\ k e. D ) /\ z e. I ) -> ( ( X ` z ) + ( Y ` z ) ) e. _V )
132 88 57 131 82 89 ofrfval2 
 |-  ( ( ph /\ k e. D ) -> ( X oR <_ ( X oF + Y ) <-> A. z e. I ( X ` z ) <_ ( ( X ` z ) + ( Y ` z ) ) ) )
133 130 132 mpbird 
 |-  ( ( ph /\ k e. D ) -> X oR <_ ( X oF + Y ) )
134 126 54 133 elrabd 
 |-  ( ( ph /\ k e. D ) -> X e. { x e. D | x oR <_ ( X oF + Y ) } )
135 breq2 
 |-  ( k = ( X oF + Y ) -> ( x oR <_ k <-> x oR <_ ( X oF + Y ) ) )
136 135 rabbidv 
 |-  ( k = ( X oF + Y ) -> { x e. D | x oR <_ k } = { x e. D | x oR <_ ( X oF + Y ) } )
137 136 eleq2d 
 |-  ( k = ( X oF + Y ) -> ( X e. { x e. D | x oR <_ k } <-> X e. { x e. D | x oR <_ ( X oF + Y ) } ) )
138 134 137 syl5ibrcom 
 |-  ( ( ph /\ k e. D ) -> ( k = ( X oF + Y ) -> X e. { x e. D | x oR <_ k } ) )
139 138 con3dimp 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> -. k = ( X oF + Y ) )
140 139 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ -. X e. { x e. D | x oR <_ k } ) -> if ( k = ( X oF + Y ) , .1. , .0. ) = .0. )
141 104 125 140 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. ) )
142 103 141 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. ) )
143 7 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
144 143 ringcmnd 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
145 12 psrbaglefi 
 |-  ( k e. D -> { x e. D | x oR <_ k } e. Fin )
146 145 adantl 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. Fin )
147 ssdif 
 |-  ( { x e. D | x oR <_ k } C_ D -> ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } ) )
148 32 147 ax-mp 
 |-  ( { x e. D | x oR <_ k } \ { X } ) C_ ( D \ { X } )
149 148 sseli 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. ( D \ { X } ) )
150 107 adantr 
 |-  ( ( ph /\ k e. D ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
151 eldifsni 
 |-  ( y e. ( D \ { X } ) -> y =/= X )
152 151 adantl 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> y =/= X )
153 152 neneqd 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> -. y = X )
154 153 iffalsed 
 |-  ( ( ( ph /\ k e. D ) /\ y e. ( D \ { X } ) ) -> if ( y = X , .1. , .0. ) = .0. )
155 ovex 
 |-  ( NN0 ^m I ) e. _V
156 5 155 rabex2 
 |-  D e. _V
157 156 a1i 
 |-  ( ( ph /\ k e. D ) -> D e. _V )
158 154 157 suppss2 
 |-  ( ( ph /\ k e. D ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) supp .0. ) C_ { X } )
159 40 a1i 
 |-  ( ( ph /\ k e. D ) -> .0. e. _V )
160 150 158 157 159 suppssr 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( D \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
161 149 160 sylan2 
 |-  ( ( ( ph /\ k e. D ) /\ j e. ( { x e. D | x oR <_ k } \ { X } ) ) -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) ` j ) = .0. )
162 161 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 ) ) ) )
163 eldifi 
 |-  ( j e. ( { x e. D | x oR <_ k } \ { X } ) -> j e. { x e. D | x oR <_ k } )
164 45 11 3 106 117 ringlzd 
 |-  ( ( ( 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. )
165 163 164 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. )
166 162 165 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. )
167 156 rabex 
 |-  { x e. D | x oR <_ k } e. _V
168 167 a1i 
 |-  ( ( ph /\ k e. D ) -> { x e. D | x oR <_ k } e. _V )
169 166 168 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 } )
170 156 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
171 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 ) ) ) )
172 170 171 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 )
173 172 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 ) )
174 snfi 
 |-  { X } e. Fin
175 174 a1i 
 |-  ( ( ph /\ k e. D ) -> { X } e. Fin )
176 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. )
177 173 175 169 176 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. )
178 45 3 144 146 119 169 177 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 ) ) ) ) ) )
179 142 178 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 ) ) ) ) ) )
180 179 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 ) ) ) ) ) ) )
181 18 180 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 ) ) ) ) ) ) )
182 15 181 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. ) ) )