Metamath Proof Explorer

Theorem mplsubrglem

Description: Lemma for mplsubrg . (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by AV, 18-Jul-2019)

Ref Expression
Hypotheses mplsubg.s 
|- S = ( I mPwSer R )
mplsubg.p 
|- P = ( I mPoly R )
mplsubg.u 
|- U = ( Base ` P )
mplsubg.i 
|- ( ph -> I e. W )
mpllss.r 
|- ( ph -> R e. Ring )
mplsubrglem.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplsubrglem.z 
|- .0. = ( 0g ` R )
mplsubrglem.p 
|- A = ( oF + " ( ( X supp .0. ) X. ( Y supp .0. ) ) )
mplsubrglem.t 
|- .x. = ( .r ` R )
mplsubrglem.x 
|- ( ph -> X e. U )
mplsubrglem.y 
|- ( ph -> Y e. U )
Assertion mplsubrglem 
|- ( ph -> ( X ( .r ` S ) Y ) e. U )

Proof

Step Hyp Ref Expression
1 mplsubg.s 
 |-  S = ( I mPwSer R )
2 mplsubg.p 
 |-  P = ( I mPoly R )
3 mplsubg.u 
 |-  U = ( Base ` P )
4 mplsubg.i 
 |-  ( ph -> I e. W )
5 mpllss.r 
 |-  ( ph -> R e. Ring )
6 mplsubrglem.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
7 mplsubrglem.z 
 |-  .0. = ( 0g ` R )
8 mplsubrglem.p 
 |-  A = ( oF + " ( ( X supp .0. ) X. ( Y supp .0. ) ) )
9 mplsubrglem.t 
 |-  .x. = ( .r ` R )
10 mplsubrglem.x 
 |-  ( ph -> X e. U )
11 mplsubrglem.y 
 |-  ( ph -> Y e. U )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 eqid 
 |-  ( .r ` S ) = ( .r ` S )
14 2 1 3 12 mplbasss 
 |-  U C_ ( Base ` S )
15 14 10 sselid 
 |-  ( ph -> X e. ( Base ` S ) )
16 14 11 sselid 
 |-  ( ph -> Y e. ( Base ` S ) )
17 1 12 13 5 15 16 psrmulcl 
 |-  ( ph -> ( X ( .r ` S ) Y ) e. ( Base ` S ) )
18 ovexd 
 |-  ( ph -> ( X ( .r ` S ) Y ) e. _V )
19 1 12 psrelbasfun 
 |-  ( ( X ( .r ` S ) Y ) e. ( Base ` S ) -> Fun ( X ( .r ` S ) Y ) )
20 17 19 syl 
 |-  ( ph -> Fun ( X ( .r ` S ) Y ) )
21 7 fvexi 
 |-  .0. e. _V
22 21 a1i 
 |-  ( ph -> .0. e. _V )
23 df-ima 
 |-  ( oF + " ( ( X supp .0. ) X. ( Y supp .0. ) ) ) = ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) )
24 8 23 eqtri 
 |-  A = ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) )
25 2 1 12 7 3 mplelbas 
 |-  ( X e. U <-> ( X e. ( Base ` S ) /\ X finSupp .0. ) )
26 25 simprbi 
 |-  ( X e. U -> X finSupp .0. )
27 10 26 syl 
 |-  ( ph -> X finSupp .0. )
28 2 1 12 7 3 mplelbas 
 |-  ( Y e. U <-> ( Y e. ( Base ` S ) /\ Y finSupp .0. ) )
29 28 simprbi 
 |-  ( Y e. U -> Y finSupp .0. )
30 11 29 syl 
 |-  ( ph -> Y finSupp .0. )
31 fsuppxpfi 
 |-  ( ( X finSupp .0. /\ Y finSupp .0. ) -> ( ( X supp .0. ) X. ( Y supp .0. ) ) e. Fin )
32 27 30 31 syl2anc 
 |-  ( ph -> ( ( X supp .0. ) X. ( Y supp .0. ) ) e. Fin )
33 ofmres 
 |-  ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) = ( f e. ( X supp .0. ) , g e. ( Y supp .0. ) |-> ( f oF + g ) )
34 ovex 
 |-  ( f oF + g ) e. _V
35 33 34 fnmpoi 
 |-  ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) Fn ( ( X supp .0. ) X. ( Y supp .0. ) )
36 dffn4 
 |-  ( ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) Fn ( ( X supp .0. ) X. ( Y supp .0. ) ) <-> ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) : ( ( X supp .0. ) X. ( Y supp .0. ) ) -onto-> ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) )
37 35 36 mpbi 
 |-  ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) : ( ( X supp .0. ) X. ( Y supp .0. ) ) -onto-> ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) )
38 fofi 
 |-  ( ( ( ( X supp .0. ) X. ( Y supp .0. ) ) e. Fin /\ ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) : ( ( X supp .0. ) X. ( Y supp .0. ) ) -onto-> ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) ) -> ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) e. Fin )
39 32 37 38 sylancl 
 |-  ( ph -> ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) e. Fin )
40 24 39 eqeltrid 
 |-  ( ph -> A e. Fin )
41 eqid 
 |-  ( Base ` R ) = ( Base ` R )
42 1 41 6 12 17 psrelbas 
 |-  ( ph -> ( X ( .r ` S ) Y ) : D --> ( Base ` R ) )
43 15 adantr 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> X e. ( Base ` S ) )
44 16 adantr 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> Y e. ( Base ` S ) )
45 eldifi 
 |-  ( k e. ( D \ A ) -> k e. D )
46 45 adantl 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> k e. D )
47 1 12 9 13 6 43 44 46 psrmulval 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> ( ( X ( .r ` S ) Y ) ` k ) = ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) ) ) )
48 5 ad2antrr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
49 2 41 3 6 11 mplelf 
 |-  ( ph -> Y : D --> ( Base ` R ) )
50 49 ad2antrr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
51 ssrab2 
 |-  { y e. D | y oR <_ k } C_ D
52 46 adantr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
53 simpr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
54 eqid 
 |-  { y e. D | y oR <_ k } = { y e. D | y oR <_ k }
55 6 54 psrbagconcl 
 |-  ( ( k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
56 52 53 55 syl2anc 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
57 51 56 sselid 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
58 50 57 ffvelcdmd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
59 41 9 7 ringlz 
 |-  ( ( R e. Ring /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) -> ( .0. .x. ( Y ` ( k oF - x ) ) ) = .0. )
60 48 58 59 syl2anc 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( .0. .x. ( Y ` ( k oF - x ) ) ) = .0. )
61 oveq1 
 |-  ( ( X ` x ) = .0. -> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = ( .0. .x. ( Y ` ( k oF - x ) ) ) )
62 61 eqeq1d 
 |-  ( ( X ` x ) = .0. -> ( ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = .0. <-> ( .0. .x. ( Y ` ( k oF - x ) ) ) = .0. ) )
63 60 62 syl5ibrcom 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) = .0. -> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = .0. ) )
64 2 41 3 6 10 mplelf 
 |-  ( ph -> X : D --> ( Base ` R ) )
65 64 ad2antrr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
66 51 53 sselid 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
67 65 66 ffvelcdmd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
68 41 9 7 ringrz 
 |-  ( ( R e. Ring /\ ( X ` x ) e. ( Base ` R ) ) -> ( ( X ` x ) .x. .0. ) = .0. )
69 48 67 68 syl2anc 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) .x. .0. ) = .0. )
70 oveq2 
 |-  ( ( Y ` ( k oF - x ) ) = .0. -> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = ( ( X ` x ) .x. .0. ) )
71 70 eqeq1d 
 |-  ( ( Y ` ( k oF - x ) ) = .0. -> ( ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = .0. <-> ( ( X ` x ) .x. .0. ) = .0. ) )
72 69 71 syl5ibrcom 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y ` ( k oF - x ) ) = .0. -> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = .0. ) )
73 6 psrbagf 
 |-  ( x e. D -> x : I --> NN0 )
74 66 73 syl 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> x : I --> NN0 )
75 74 ffvelcdmda 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ n e. I ) -> ( x ` n ) e. NN0 )
76 6 psrbagf 
 |-  ( k e. D -> k : I --> NN0 )
77 52 76 syl 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> k : I --> NN0 )
78 77 ffvelcdmda 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ n e. I ) -> ( k ` n ) e. NN0 )
79 nn0cn 
 |-  ( ( x ` n ) e. NN0 -> ( x ` n ) e. CC )
80 nn0cn 
 |-  ( ( k ` n ) e. NN0 -> ( k ` n ) e. CC )
81 pncan3 
 |-  ( ( ( x ` n ) e. CC /\ ( k ` n ) e. CC ) -> ( ( x ` n ) + ( ( k ` n ) - ( x ` n ) ) ) = ( k ` n ) )
82 79 80 81 syl2an 
 |-  ( ( ( x ` n ) e. NN0 /\ ( k ` n ) e. NN0 ) -> ( ( x ` n ) + ( ( k ` n ) - ( x ` n ) ) ) = ( k ` n ) )
83 75 78 82 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ n e. I ) -> ( ( x ` n ) + ( ( k ` n ) - ( x ` n ) ) ) = ( k ` n ) )
84 83 mpteq2dva 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( n e. I |-> ( ( x ` n ) + ( ( k ` n ) - ( x ` n ) ) ) ) = ( n e. I |-> ( k ` n ) ) )
85 4 ad2antrr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> I e. W )
86 ovexd 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ n e. I ) -> ( ( k ` n ) - ( x ` n ) ) e. _V )
87 74 feqmptd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> x = ( n e. I |-> ( x ` n ) ) )
88 77 feqmptd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> k = ( n e. I |-> ( k ` n ) ) )
89 85 78 75 88 87 offval2 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) = ( n e. I |-> ( ( k ` n ) - ( x ` n ) ) ) )
90 85 75 86 87 89 offval2 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( x oF + ( k oF - x ) ) = ( n e. I |-> ( ( x ` n ) + ( ( k ` n ) - ( x ` n ) ) ) ) )
91 84 90 88 3eqtr4d 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( x oF + ( k oF - x ) ) = k )
92 simplr 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> k e. ( D \ A ) )
93 91 92 eqeltrd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( x oF + ( k oF - x ) ) e. ( D \ A ) )
94 93 eldifbd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> -. ( x oF + ( k oF - x ) ) e. A )
95 ovres 
 |-  ( ( x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) -> ( x ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) ( k oF - x ) ) = ( x oF + ( k oF - x ) ) )
96 fnovrn 
 |-  ( ( ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) Fn ( ( X supp .0. ) X. ( Y supp .0. ) ) /\ x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) -> ( x ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) ( k oF - x ) ) e. ran ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) )
97 96 24 eleqtrrdi 
 |-  ( ( ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) Fn ( ( X supp .0. ) X. ( Y supp .0. ) ) /\ x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) -> ( x ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) ( k oF - x ) ) e. A )
98 35 97 mp3an1 
 |-  ( ( x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) -> ( x ( oF + |` ( ( X supp .0. ) X. ( Y supp .0. ) ) ) ( k oF - x ) ) e. A )
99 95 98 eqeltrrd 
 |-  ( ( x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) -> ( x oF + ( k oF - x ) ) e. A )
100 94 99 nsyl 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> -. ( x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) )
101 ianor 
 |-  ( -. ( x e. ( X supp .0. ) /\ ( k oF - x ) e. ( Y supp .0. ) ) <-> ( -. x e. ( X supp .0. ) \/ -. ( k oF - x ) e. ( Y supp .0. ) ) )
102 100 101 sylib 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( -. x e. ( X supp .0. ) \/ -. ( k oF - x ) e. ( Y supp .0. ) ) )
103 eldif 
 |-  ( x e. ( D \ ( X supp .0. ) ) <-> ( x e. D /\ -. x e. ( X supp .0. ) ) )
104 103 baib 
 |-  ( x e. D -> ( x e. ( D \ ( X supp .0. ) ) <-> -. x e. ( X supp .0. ) ) )
105 66 104 syl 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( x e. ( D \ ( X supp .0. ) ) <-> -. x e. ( X supp .0. ) ) )
106 ssidd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( X supp .0. ) C_ ( X supp .0. ) )
107 ovex 
 |-  ( NN0 ^m I ) e. _V
108 6 107 rabex2 
 |-  D e. _V
109 108 a1i 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> D e. _V )
110 21 a1i 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> .0. e. _V )
111 65 106 109 110 suppssr 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ x e. ( D \ ( X supp .0. ) ) ) -> ( X ` x ) = .0. )
112 111 ex 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( x e. ( D \ ( X supp .0. ) ) -> ( X ` x ) = .0. ) )
113 105 112 sylbird 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( -. x e. ( X supp .0. ) -> ( X ` x ) = .0. ) )
114 eldif 
 |-  ( ( k oF - x ) e. ( D \ ( Y supp .0. ) ) <-> ( ( k oF - x ) e. D /\ -. ( k oF - x ) e. ( Y supp .0. ) ) )
115 114 baib 
 |-  ( ( k oF - x ) e. D -> ( ( k oF - x ) e. ( D \ ( Y supp .0. ) ) <-> -. ( k oF - x ) e. ( Y supp .0. ) ) )
116 57 115 syl 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( k oF - x ) e. ( D \ ( Y supp .0. ) ) <-> -. ( k oF - x ) e. ( Y supp .0. ) ) )
117 ssidd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y supp .0. ) C_ ( Y supp .0. ) )
118 50 117 109 110 suppssr 
 |-  ( ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. ( D \ ( Y supp .0. ) ) ) -> ( Y ` ( k oF - x ) ) = .0. )
119 118 ex 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( k oF - x ) e. ( D \ ( Y supp .0. ) ) -> ( Y ` ( k oF - x ) ) = .0. ) )
120 116 119 sylbird 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( -. ( k oF - x ) e. ( Y supp .0. ) -> ( Y ` ( k oF - x ) ) = .0. ) )
121 113 120 orim12d 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( -. x e. ( X supp .0. ) \/ -. ( k oF - x ) e. ( Y supp .0. ) ) -> ( ( X ` x ) = .0. \/ ( Y ` ( k oF - x ) ) = .0. ) ) )
122 102 121 mpd 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) = .0. \/ ( Y ` ( k oF - x ) ) = .0. ) )
123 63 72 122 mpjaod 
 |-  ( ( ( ph /\ k e. ( D \ A ) ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) = .0. )
124 123 mpteq2dva 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> .0. ) )
125 124 oveq2d 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) .x. ( Y ` ( k oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ k } |-> .0. ) ) )
126 5 adantr 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> R e. Ring )
127 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
128 126 127 syl 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> R e. Mnd )
129 6 psrbaglefi 
 |-  ( k e. D -> { y e. D | y oR <_ k } e. Fin )
130 46 129 syl 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> { y e. D | y oR <_ k } e. Fin )
131 7 gsumz 
 |-  ( ( R e. Mnd /\ { y e. D | y oR <_ k } e. Fin ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> .0. ) ) = .0. )
132 128 130 131 syl2anc 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> .0. ) ) = .0. )
133 47 125 132 3eqtrd 
 |-  ( ( ph /\ k e. ( D \ A ) ) -> ( ( X ( .r ` S ) Y ) ` k ) = .0. )
134 42 133 suppss 
 |-  ( ph -> ( ( X ( .r ` S ) Y ) supp .0. ) C_ A )
135 suppssfifsupp 
 |-  ( ( ( ( X ( .r ` S ) Y ) e. _V /\ Fun ( X ( .r ` S ) Y ) /\ .0. e. _V ) /\ ( A e. Fin /\ ( ( X ( .r ` S ) Y ) supp .0. ) C_ A ) ) -> ( X ( .r ` S ) Y ) finSupp .0. )
136 18 20 22 40 134 135 syl32anc 
 |-  ( ph -> ( X ( .r ` S ) Y ) finSupp .0. )
137 2 1 12 7 3 mplelbas 
 |-  ( ( X ( .r ` S ) Y ) e. U <-> ( ( X ( .r ` S ) Y ) e. ( Base ` S ) /\ ( X ( .r ` S ) Y ) finSupp .0. ) )
138 17 136 137 sylanbrc 
 |-  ( ph -> ( X ( .r ` S ) Y ) e. U )