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 syl5eq
 |-  ( -. ( 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 )