Metamath Proof Explorer

Theorem mplmulmvr

Description: Multiply a polynomial F with a variable X (i.e. with a monic monomial). (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses mplmulmvr.1 
|- P = ( I mPoly R )
mplmulmvr.2 
|- X = ( ( I mVar R ) ` Y )
mplmulmvr.3 
|- M = ( Base ` P )
mplmulmvr.4 
|- .x. = ( .r ` P )
mplmulmvr.5 
|- .0. = ( 0g ` R )
mplmulmvr.6 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
mplmulmvr.7 
|- A = ( ( _Ind ` I ) ` { Y } )
mplmulmvr.8 
|- ( ph -> I e. V )
mplmulmvr.9 
|- ( ph -> Y e. I )
mplmulmvr.10 
|- ( ph -> R e. Ring )
mplmulmvr.11 
|- ( ph -> F e. M )
Assertion mplmulmvr 
|- ( ph -> ( X .x. F ) = ( b e. D |-> if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplmulmvr.1 
 |-  P = ( I mPoly R )
2 mplmulmvr.2 
 |-  X = ( ( I mVar R ) ` Y )
3 mplmulmvr.3 
 |-  M = ( Base ` P )
4 mplmulmvr.4 
 |-  .x. = ( .r ` P )
5 mplmulmvr.5 
 |-  .0. = ( 0g ` R )
6 mplmulmvr.6 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
7 mplmulmvr.7 
 |-  A = ( ( _Ind ` I ) ` { Y } )
8 mplmulmvr.8 
 |-  ( ph -> I e. V )
9 mplmulmvr.9 
 |-  ( ph -> Y e. I )
10 mplmulmvr.10 
 |-  ( ph -> R e. Ring )
11 mplmulmvr.11 
 |-  ( ph -> F e. M )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 6 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
14 eqid 
 |-  ( I mVar R ) = ( I mVar R )
15 1 14 3 8 10 9 mvrcl 
 |-  ( ph -> ( ( I mVar R ) ` Y ) e. M )
16 2 15 eqeltrid 
 |-  ( ph -> X e. M )
17 1 3 12 4 13 16 11 mplmul 
 |-  ( ph -> ( X .x. F ) = ( b e. D |-> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) ) )
18 eqeq2 
 |-  ( .0. = if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) -> ( ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = .0. <-> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) ) )
19 eqeq2 
 |-  ( ( F ` ( b oF - A ) ) = if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) -> ( ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = ( F ` ( b oF - A ) ) <-> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) ) )
20 simplll 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ph )
21 ssrab2 
 |-  { y e. D | y oR <_ b } C_ D
22 21 a1i 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> { y e. D | y oR <_ b } C_ D )
23 22 sselda 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. D )
24 2 fveq1i 
 |-  ( X ` x ) = ( ( ( I mVar R ) ` Y ) ` x )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 8 adantr 
 |-  ( ( ph /\ x e. D ) -> I e. V )
27 10 adantr 
 |-  ( ( ph /\ x e. D ) -> R e. Ring )
28 9 adantr 
 |-  ( ( ph /\ x e. D ) -> Y e. I )
29 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
30 14 13 5 25 26 27 28 29 7 mvrvalind 
 |-  ( ( ph /\ x e. D ) -> ( ( ( I mVar R ) ` Y ) ` x ) = if ( x = A , ( 1r ` R ) , .0. ) )
31 24 30 eqtrid 
 |-  ( ( ph /\ x e. D ) -> ( X ` x ) = if ( x = A , ( 1r ` R ) , .0. ) )
32 20 23 31 syl2anc 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( X ` x ) = if ( x = A , ( 1r ` R ) , .0. ) )
33 32 oveq1d 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( if ( x = A , ( 1r ` R ) , .0. ) ( .r ` R ) ( F ` ( b oF - x ) ) ) )
34 simpr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> x = A )
35 34 fveq1d 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) = ( A ` Y ) )
36 0ne1 
 |-  0 =/= 1
37 36 a1i 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> 0 =/= 1 )
38 20 8 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> I e. V )
39 nn0ex 
 |-  NN0 e. _V
40 39 a1i 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> NN0 e. _V )
41 6 ssrab3 
 |-  D C_ ( NN0 ^m I )
42 22 41 sstrdi 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> { y e. D | y oR <_ b } C_ ( NN0 ^m I ) )
43 42 sselda 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. ( NN0 ^m I ) )
44 38 40 43 elmaprd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x : I --> NN0 )
45 44 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> x : I --> NN0 )
46 9 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> Y e. I )
47 45 46 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) e. NN0 )
48 44 ffnd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x Fn I )
49 8 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. V )
50 39 a1i 
 |-  ( ( ph /\ b e. D ) -> NN0 e. _V )
51 41 a1i 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
52 51 sselda 
 |-  ( ( ph /\ b e. D ) -> b e. ( NN0 ^m I ) )
53 49 50 52 elmaprd 
 |-  ( ( ph /\ b e. D ) -> b : I --> NN0 )
54 53 ad2antrr 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> b : I --> NN0 )
55 54 ffnd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> b Fn I )
56 breq1 
 |-  ( y = x -> ( y oR <_ b <-> x oR <_ b ) )
57 simpr 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. { y e. D | y oR <_ b } )
58 56 57 elrabrd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x oR <_ b )
59 20 9 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> Y e. I )
60 48 55 38 58 59 fnfvor 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( x ` Y ) <_ ( b ` Y ) )
61 60 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) <_ ( b ` Y ) )
62 simpllr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( b ` Y ) = 0 )
63 61 62 breqtrd 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) <_ 0 )
64 nn0le0eq0 
 |-  ( ( x ` Y ) e. NN0 -> ( ( x ` Y ) <_ 0 <-> ( x ` Y ) = 0 ) )
65 64 biimpa 
 |-  ( ( ( x ` Y ) e. NN0 /\ ( x ` Y ) <_ 0 ) -> ( x ` Y ) = 0 )
66 47 63 65 syl2anc 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) = 0 )
67 7 fveq1i 
 |-  ( A ` Y ) = ( ( ( _Ind ` I ) ` { Y } ) ` Y )
68 9 snssd 
 |-  ( ph -> { Y } C_ I )
69 snidg 
 |-  ( Y e. I -> Y e. { Y } )
70 9 69 syl 
 |-  ( ph -> Y e. { Y } )
71 ind1 
 |-  ( ( I e. V /\ { Y } C_ I /\ Y e. { Y } ) -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
72 8 68 70 71 syl3anc 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
73 67 72 eqtrid 
 |-  ( ph -> ( A ` Y ) = 1 )
74 73 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( A ` Y ) = 1 )
75 37 66 74 3netr4d 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( x ` Y ) =/= ( A ` Y ) )
76 75 neneqd 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> -. ( x ` Y ) = ( A ` Y ) )
77 35 76 pm2.65da 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> -. x = A )
78 77 iffalsed 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> if ( x = A , ( 1r ` R ) , .0. ) = .0. )
79 78 oveq1d 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( if ( x = A , ( 1r ` R ) , .0. ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) )
80 eqid 
 |-  ( Base ` R ) = ( Base ` R )
81 20 10 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> R e. Ring )
82 1 80 3 13 11 mplelf 
 |-  ( ph -> F : D --> ( Base ` R ) )
83 20 82 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> F : D --> ( Base ` R ) )
84 simpllr 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> b e. D )
85 13 psrbagcon 
 |-  ( ( b e. D /\ x : I --> NN0 /\ x oR <_ b ) -> ( ( b oF - x ) e. D /\ ( b oF - x ) oR <_ b ) )
86 85 simpld 
 |-  ( ( b e. D /\ x : I --> NN0 /\ x oR <_ b ) -> ( b oF - x ) e. D )
87 84 44 58 86 syl3anc 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( b oF - x ) e. D )
88 83 87 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( F ` ( b oF - x ) ) e. ( Base ` R ) )
89 80 12 5 81 88 ringlzd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) = .0. )
90 33 79 89 3eqtrd 
 |-  ( ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = .0. )
91 90 mpteq2dva 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ b } |-> .0. ) )
92 91 oveq2d 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ b } |-> .0. ) ) )
93 10 ringgrpd 
 |-  ( ph -> R e. Grp )
94 93 grpmndd 
 |-  ( ph -> R e. Mnd )
95 94 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> R e. Mnd )
96 ovex 
 |-  ( NN0 ^m I ) e. _V
97 6 96 rab2ex 
 |-  { y e. D | y oR <_ b } e. _V
98 97 a1i 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> { y e. D | y oR <_ b } e. _V )
99 5 gsumz 
 |-  ( ( R e. Mnd /\ { y e. D | y oR <_ b } e. _V ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> .0. ) ) = .0. )
100 95 98 99 syl2anc 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> .0. ) ) = .0. )
101 92 100 eqtrd 
 |-  ( ( ( ph /\ b e. D ) /\ ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = .0. )
102 simplll 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ph )
103 21 a1i 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> { y e. D | y oR <_ b } C_ D )
104 103 sselda 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. D )
105 102 104 31 syl2anc 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( X ` x ) = if ( x = A , ( 1r ` R ) , .0. ) )
106 105 oveq1d 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( if ( x = A , ( 1r ` R ) , .0. ) ( .r ` R ) ( F ` ( b oF - x ) ) ) )
107 ovif 
 |-  ( if ( x = A , ( 1r ` R ) , .0. ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = if ( x = A , ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) , ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) )
108 107 a1i 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( if ( x = A , ( 1r ` R ) , .0. ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = if ( x = A , ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) , ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) ) )
109 102 10 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> R e. Ring )
110 102 82 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> F : D --> ( Base ` R ) )
111 simpllr 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> b e. D )
112 102 8 syl 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> I e. V )
113 39 a1i 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> NN0 e. _V )
114 41 104 sselid 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. ( NN0 ^m I ) )
115 112 113 114 elmaprd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x : I --> NN0 )
116 simpr 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x e. { y e. D | y oR <_ b } )
117 56 116 elrabrd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> x oR <_ b )
118 111 115 117 86 syl3anc 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( b oF - x ) e. D )
119 110 118 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( F ` ( b oF - x ) ) e. ( Base ` R ) )
120 80 12 25 109 119 ringlidmd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( F ` ( b oF - x ) ) )
121 120 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( F ` ( b oF - x ) ) )
122 oveq2 
 |-  ( x = A -> ( b oF - x ) = ( b oF - A ) )
123 122 adantl 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( b oF - x ) = ( b oF - A ) )
124 123 fveq2d 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( F ` ( b oF - x ) ) = ( F ` ( b oF - A ) ) )
125 121 124 eqtrd 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ x = A ) -> ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = ( F ` ( b oF - A ) ) )
126 80 12 5 109 119 ringlzd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) = .0. )
127 126 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) /\ -. x = A ) -> ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) = .0. )
128 125 127 ifeq12da 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> if ( x = A , ( ( 1r ` R ) ( .r ` R ) ( F ` ( b oF - x ) ) ) , ( .0. ( .r ` R ) ( F ` ( b oF - x ) ) ) ) = if ( x = A , ( F ` ( b oF - A ) ) , .0. ) )
129 106 108 128 3eqtrd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ x e. { y e. D | y oR <_ b } ) -> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) = if ( x = A , ( F ` ( b oF - A ) ) , .0. ) )
130 129 mpteq2dva 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ b } |-> if ( x = A , ( F ` ( b oF - A ) ) , .0. ) ) )
131 130 oveq2d 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ b } |-> if ( x = A , ( F ` ( b oF - A ) ) , .0. ) ) ) )
132 94 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> R e. Mnd )
133 97 a1i 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> { y e. D | y oR <_ b } e. _V )
134 breq1 
 |-  ( y = A -> ( y oR <_ b <-> A oR <_ b ) )
135 breq1 
 |-  ( h = A -> ( h finSupp 0 <-> A finSupp 0 ) )
136 39 a1i 
 |-  ( ph -> NN0 e. _V )
137 indf 
 |-  ( ( I e. V /\ { Y } C_ I ) -> ( ( _Ind ` I ) ` { Y } ) : I --> { 0 , 1 } )
138 8 68 137 syl2anc 
 |-  ( ph -> ( ( _Ind ` I ) ` { Y } ) : I --> { 0 , 1 } )
139 7 feq1i 
 |-  ( A : I --> { 0 , 1 } <-> ( ( _Ind ` I ) ` { Y } ) : I --> { 0 , 1 } )
140 138 139 sylibr 
 |-  ( ph -> A : I --> { 0 , 1 } )
141 0nn0 
 |-  0 e. NN0
142 141 a1i 
 |-  ( ph -> 0 e. NN0 )
143 1nn0 
 |-  1 e. NN0
144 143 a1i 
 |-  ( ph -> 1 e. NN0 )
145 142 144 prssd 
 |-  ( ph -> { 0 , 1 } C_ NN0 )
146 140 145 fssd 
 |-  ( ph -> A : I --> NN0 )
147 136 8 146 elmapdd 
 |-  ( ph -> A e. ( NN0 ^m I ) )
148 146 ffund 
 |-  ( ph -> Fun A )
149 7 oveq1i 
 |-  ( A supp 0 ) = ( ( ( _Ind ` I ) ` { Y } ) supp 0 )
150 indsupp 
 |-  ( ( I e. V /\ { Y } C_ I ) -> ( ( ( _Ind ` I ) ` { Y } ) supp 0 ) = { Y } )
151 8 68 150 syl2anc 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) supp 0 ) = { Y } )
152 149 151 eqtrid 
 |-  ( ph -> ( A supp 0 ) = { Y } )
153 snfi 
 |-  { Y } e. Fin
154 152 153 eqeltrdi 
 |-  ( ph -> ( A supp 0 ) e. Fin )
155 147 142 148 154 isfsuppd 
 |-  ( ph -> A finSupp 0 )
156 135 147 155 elrabd 
 |-  ( ph -> A e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
157 156 6 eleqtrrdi 
 |-  ( ph -> A e. D )
158 157 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A e. D )
159 breq1 
 |-  ( 1 = if ( u e. { Y } , 1 , 0 ) -> ( 1 <_ ( b ` u ) <-> if ( u e. { Y } , 1 , 0 ) <_ ( b ` u ) ) )
160 breq1 
 |-  ( 0 = if ( u e. { Y } , 1 , 0 ) -> ( 0 <_ ( b ` u ) <-> if ( u e. { Y } , 1 , 0 ) <_ ( b ` u ) ) )
161 53 adantr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> b : I --> NN0 )
162 161 ffvelcdmda 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> ( b ` u ) e. NN0 )
163 162 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> ( b ` u ) e. NN0 )
164 elsni 
 |-  ( u e. { Y } -> u = Y )
165 164 adantl 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> u = Y )
166 165 fveq2d 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> ( b ` u ) = ( b ` Y ) )
167 simpllr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> -. ( b ` Y ) = 0 )
168 167 neqned 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> ( b ` Y ) =/= 0 )
169 166 168 eqnetrd 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> ( b ` u ) =/= 0 )
170 elnnne0 
 |-  ( ( b ` u ) e. NN <-> ( ( b ` u ) e. NN0 /\ ( b ` u ) =/= 0 ) )
171 163 169 170 sylanbrc 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> ( b ` u ) e. NN )
172 171 nnge1d 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ u e. { Y } ) -> 1 <_ ( b ` u ) )
173 162 nn0ge0d 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> 0 <_ ( b ` u ) )
174 173 adantr 
 |-  ( ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) /\ -. u e. { Y } ) -> 0 <_ ( b ` u ) )
175 159 160 172 174 ifbothda 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> if ( u e. { Y } , 1 , 0 ) <_ ( b ` u ) )
176 175 ralrimiva 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A. u e. I if ( u e. { Y } , 1 , 0 ) <_ ( b ` u ) )
177 8 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> I e. V )
178 143 a1i 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> 1 e. NN0 )
179 141 a1i 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> 0 e. NN0 )
180 178 179 ifexd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> if ( u e. { Y } , 1 , 0 ) e. _V )
181 fvexd 
 |-  ( ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) /\ u e. I ) -> ( b ` u ) e. _V )
182 indval 
 |-  ( ( I e. V /\ { Y } C_ I ) -> ( ( _Ind ` I ) ` { Y } ) = ( u e. I |-> if ( u e. { Y } , 1 , 0 ) ) )
183 8 68 182 syl2anc 
 |-  ( ph -> ( ( _Ind ` I ) ` { Y } ) = ( u e. I |-> if ( u e. { Y } , 1 , 0 ) ) )
184 7 183 eqtrid 
 |-  ( ph -> A = ( u e. I |-> if ( u e. { Y } , 1 , 0 ) ) )
185 184 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A = ( u e. I |-> if ( u e. { Y } , 1 , 0 ) ) )
186 53 feqmptd 
 |-  ( ( ph /\ b e. D ) -> b = ( u e. I |-> ( b ` u ) ) )
187 186 adantr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> b = ( u e. I |-> ( b ` u ) ) )
188 177 180 181 185 187 ofrfval2 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( A oR <_ b <-> A. u e. I if ( u e. { Y } , 1 , 0 ) <_ ( b ` u ) ) )
189 176 188 mpbird 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A oR <_ b )
190 134 158 189 elrabd 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A e. { y e. D | y oR <_ b } )
191 eqid 
 |-  ( x e. { y e. D | y oR <_ b } |-> if ( x = A , ( F ` ( b oF - A ) ) , .0. ) ) = ( x e. { y e. D | y oR <_ b } |-> if ( x = A , ( F ` ( b oF - A ) ) , .0. ) )
192 82 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> F : D --> ( Base ` R ) )
193 simplr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> b e. D )
194 146 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> A : I --> NN0 )
195 13 psrbagcon 
 |-  ( ( b e. D /\ A : I --> NN0 /\ A oR <_ b ) -> ( ( b oF - A ) e. D /\ ( b oF - A ) oR <_ b ) )
196 195 simpld 
 |-  ( ( b e. D /\ A : I --> NN0 /\ A oR <_ b ) -> ( b oF - A ) e. D )
197 193 194 189 196 syl3anc 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( b oF - A ) e. D )
198 192 197 ffvelcdmd 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( F ` ( b oF - A ) ) e. ( Base ` R ) )
199 5 132 133 190 191 198 gsummptif1n0 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> if ( x = A , ( F ` ( b oF - A ) ) , .0. ) ) ) = ( F ` ( b oF - A ) ) )
200 131 199 eqtrd 
 |-  ( ( ( ph /\ b e. D ) /\ -. ( b ` Y ) = 0 ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = ( F ` ( b oF - A ) ) )
201 18 19 101 200 ifbothda 
 |-  ( ( ph /\ b e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) = if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) )
202 201 mpteq2dva 
 |-  ( ph -> ( b e. D |-> ( R gsum ( x e. { y e. D | y oR <_ b } |-> ( ( X ` x ) ( .r ` R ) ( F ` ( b oF - x ) ) ) ) ) ) = ( b e. D |-> if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) ) )
203 17 202 eqtrd 
 |-  ( ph -> ( X .x. F ) = ( b e. D |-> if ( ( b ` Y ) = 0 , .0. , ( F ` ( b oF - A ) ) ) ) )