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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplval.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	mplval.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplval.u	⊢ 𝑈 = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }
Assertion	mplval	⊢ 𝑃 = ( 𝑆 ↾s 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mplval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplval.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3		mplval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		mplval.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		mplval.u	⊢ 𝑈 = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }
6		ovexd	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPwSer 𝑟 ) ∈ V )
7		id	⊢ ( 𝑠 = ( 𝑖 mPwSer 𝑟 ) → 𝑠 = ( 𝑖 mPwSer 𝑟 ) )
8		oveq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPwSer 𝑟 ) = ( 𝐼 mPwSer 𝑅 ) )
9	7 8	sylan9eqr	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → 𝑠 = ( 𝐼 mPwSer 𝑅 ) )
10	9 2	eqtr4di	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → 𝑠 = 𝑆 )
11	10	fveq2d	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
12	11 3	eqtr4di	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( Base ‘ 𝑠 ) = 𝐵 )
13		simplr	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → 𝑟 = 𝑅 )
14	13	fveq2d	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
15	14 4	eqtr4di	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( 0g ‘ 𝑟 ) = 0 )
16	15	breq2d	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( 𝑓 finSupp ( 0g ‘ 𝑟 ) ↔ 𝑓 finSupp 0 ) )
17	12 16	rabeqbidv	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } )
18	17 5	eqtr4di	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } = 𝑈 )
19	10 18	oveq12d	⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ∧ 𝑠 = ( 𝑖 mPwSer 𝑟 ) ) → ( 𝑠 ↾s { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) = ( 𝑆 ↾s 𝑈 ) )
20	6 19	csbied	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑠 ⦌ ( 𝑠 ↾s { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) = ( 𝑆 ↾s 𝑈 ) )
21		df-mpl	⊢ mPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑠 ⦌ ( 𝑠 ↾s { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) )
22		ovex	⊢ ( 𝑆 ↾s 𝑈 ) ∈ V
23	20 21 22	ovmpoa	⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPoly 𝑅 ) = ( 𝑆 ↾s 𝑈 ) )
24		reldmmpl	⊢ Rel dom mPoly
25	24	ovprc	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPoly 𝑅 ) = ∅ )
26		ress0	⊢ ( ∅ ↾s 𝑈 ) = ∅
27	25 26	eqtr4di	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPoly 𝑅 ) = ( ∅ ↾s 𝑈 ) )
28		reldmpsr	⊢ Rel dom mPwSer
29	28	ovprc	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
30	2 29	syl5eq	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ∅ )
31	30	oveq1d	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑆 ↾s 𝑈 ) = ( ∅ ↾s 𝑈 ) )
32	27 31	eqtr4d	⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPoly 𝑅 ) = ( 𝑆 ↾s 𝑈 ) )
33	23 32	pm2.61i	⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝑆 ↾s 𝑈 )
34	1 33	eqtri	⊢ 𝑃 = ( 𝑆 ↾s 𝑈 )