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