Metamath Proof Explorer

Theorem mplval

Description: Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 25-Jun-2019)

Ref Expression
Hypotheses mplval.p 
|- P = ( I mPoly R )
mplval.s 
|- S = ( I mPwSer R )
mplval.b 
|- B = ( Base ` S )
mplval.z 
|- .0. = ( 0g ` R )
mplval.u 
|- U = { f e. B | f finSupp .0. }
Assertion mplval 
|- P = ( S |`s U )

Proof

Step Hyp Ref Expression
1 mplval.p 
 |-  P = ( I mPoly R )
2 mplval.s 
 |-  S = ( I mPwSer R )
3 mplval.b 
 |-  B = ( Base ` S )
4 mplval.z 
 |-  .0. = ( 0g ` R )
5 mplval.u 
 |-  U = { f e. B | f finSupp .0. }
6 ovexd 
 |-  ( ( i = I /\ r = R ) -> ( i mPwSer r ) e. _V )
7 id 
 |-  ( s = ( i mPwSer r ) -> s = ( i mPwSer r ) )
8 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPwSer r ) = ( I mPwSer R ) )
9 7 8 sylan9eqr 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> s = ( I mPwSer R ) )
10 9 2 eqtr4di 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> s = S )
11 10 fveq2d 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( Base ` s ) = ( Base ` S ) )
12 11 3 eqtr4di 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( Base ` s ) = B )
13 simplr 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> r = R )
14 13 fveq2d 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( 0g ` r ) = ( 0g ` R ) )
15 14 4 eqtr4di 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( 0g ` r ) = .0. )
16 15 breq2d 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( f finSupp ( 0g ` r ) <-> f finSupp .0. ) )
17 12 16 rabeqbidv 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } = { f e. B | f finSupp .0. } )
18 17 5 eqtr4di 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } = U )
19 10 18 oveq12d 
 |-  ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( s |`s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) = ( S |`s U ) )
20 6 19 csbied 
 |-  ( ( i = I /\ r = R ) -> [_ ( i mPwSer r ) / s ]_ ( s |`s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) = ( S |`s U ) )
21 df-mpl 
 |-  mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / s ]_ ( s |`s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) )
22 ovex 
 |-  ( S |`s U ) e. _V
23 20 21 22 ovmpoa 
 |-  ( ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( S |`s U ) )
24 reldmmpl 
 |-  Rel dom mPoly
25 24 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = (/) )
26 ress0 
 |-  ( (/) |`s U ) = (/)
27 25 26 eqtr4di 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( (/) |`s U ) )
28 reldmpsr 
 |-  Rel dom mPwSer
29 28 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
30 2 29 eqtrid 
 |-  ( -. ( I e. _V /\ R e. _V ) -> S = (/) )
31 30 oveq1d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( S |`s U ) = ( (/) |`s U ) )
32 27 31 eqtr4d 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( S |`s U ) )
33 23 32 pm2.61i 
 |-  ( I mPoly R ) = ( S |`s U )
34 1 33 eqtri 
 |-  P = ( S |`s U )