Theorem mplval 17952

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

Hypotheses

Ref	Expression
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

Ref	Expression
mplval	|- P = ( S ↾s U )

Distinct variable groups:   B, f   f, I   R, f   .0. , f

Allowed substitution hints:   P( f)   S( f)   U( f)

Proof of Theorem mplval

Dummy variables i r s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplval.p	. 2 |- P = ( I mPoly R )
2		ovex 6320	. . . . . 6 |- ( i mPwSer r ) e. _V
3	2	a1i 11	. . . . 5 |- ( ( i = I /\ r = R ) -> ( i mPwSer r ) e. _V )
4		id 22	. . . . . . . 8 |- ( s = ( i mPwSer r ) -> s = ( i mPwSer r ) )
5		oveq12 6304	. . . . . . . 8 |- ( ( i = I /\ r = R ) -> ( i mPwSer r ) = ( I mPwSer R ) )
6	4, 5	sylan9eqr 2530	. . . . . . 7 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> s = ( I mPwSer R ) )
7		mplval.s	. . . . . . 7 |- S = ( I mPwSer R )
8	6, 7	syl6eqr 2526	. . . . . 6 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> s = S )
9	8	fveq2d 5876	. . . . . . . . 9 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( Base ` s ) = ( Base ` S ) )
10		mplval.b	. . . . . . . . 9 |- B = ( Base ` S )
11	9, 10	syl6eqr 2526	. . . . . . . 8 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( Base ` s ) = B )
12		simplr 754	. . . . . . . . . . 11 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> r = R )
13	12	fveq2d 5876	. . . . . . . . . 10 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( 0g ` r ) = ( 0g ` R ) )
14		mplval.z	. . . . . . . . . 10 |- .0. = ( 0g ` R )
15	13, 14	syl6eqr 2526	. . . . . . . . 9 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( 0g ` r ) = .0. )
16	15	breq2d 4465	. . . . . . . 8 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( f finSupp ( 0g ` r ) <-> f finSupp .0. ) )
17	11, 16	rabeqbidv 3113	. . . . . . 7 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } = { f e. B | f finSupp .0. } )
18		mplval.u	. . . . . . 7 |- U = { f e. B | f finSupp .0. }
19	17, 18	syl6eqr 2526	. . . . . 6 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } = U )
20	8, 19	oveq12d 6313	. . . . 5 |- ( ( ( i = I /\ r = R ) /\ s = ( i mPwSer r ) ) -> ( s ↾s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) = ( S ↾s U ) )
21	3, 20	csbied 3467	. . . 4 |- ( ( i = I /\ r = R ) -> [_ ( i mPwSer r ) / s ]_ ( s ↾s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) = ( S ↾s U ) )
22		df-mpl 17875	. . . 4 |- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / s ]_ ( s ↾s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) )
23		ovex 6320	. . . 4 |- ( S ↾s U ) e. _V
24	21, 22, 23	ovmpt2a 6428	. . 3 |- ( ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( S ↾s U ) )
25		reldmmpl 17951	. . . . . 6 |- Rel dom mPoly
26	25	ovprc 6322	. . . . 5 |- ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = (/) )
27		ress0 14565	. . . . 5 |- ( (/) ↾s U ) = (/)
28	26, 27	syl6eqr 2526	. . . 4 |- ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( (/) ↾s U ) )
29		reldmpsr 17878	. . . . . . 7 |- Rel dom mPwSer
30	29	ovprc 6322	. . . . . 6 |- ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
31	7, 30	syl5eq 2520	. . . . 5 |- ( -. ( I e. _V /\ R e. _V ) -> S = (/) )
32	31	oveq1d 6310	. . . 4 |- ( -. ( I e. _V /\ R e. _V ) -> ( S ↾s U ) = ( (/) ↾s U ) )
33	28, 32	eqtr4d 2511	. . 3 |- ( -. ( I e. _V /\ R e. _V ) -> ( I mPoly R ) = ( S ↾s U ) )
34	24, 33	pm2.61i 164	. 2 |- ( I mPoly R ) = ( S ↾s U )
35	1, 34	eqtri 2496	1 |- P = ( S ↾s U )

Syntax hints:   -. wn 3   /\ wa 369   = wceq 1379   e. wcel 1767   {crab 2821   _Vcvv 3118   [_csb 3440   (/)c0 3790   class class class wbr 4453   ` cfv 5594  (class class class)co 6295   finSupp cfsupp 7841   Basecbs 14506   ↾_s cress 14507   0gc0g 14711   mPwSer cmps 17868   mPoly cmpl 17870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-slot 14510  df-base 14511  df-ress 14513  df-psr 17873  df-mpl 17875

This theorem is referenced by:  mplvalOLD  17953  mplbas  17954  mplval2  17958