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	$⊢ \underset{˙}{0} = 0_{R}$
	mplval.u	$⊢ U = \{f \in B \| {finSupp}_{\underset{˙}{0}} (f)\}$
Assertion	mplval	$⊢ P = 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	$⊢ \underset{˙}{0} = 0_{R}$
5		mplval.u	$⊢ U = \{f \in B \| {finSupp}_{\underset{˙}{0}} (f)\}$
6		ovexd	$⊢ (i = I \land r = R) \to i mPwSer r \in V$
7		id	$⊢ s = i mPwSer r \to s = i mPwSer r$
8		oveq12	$⊢ (i = I \land r = R) \to i mPwSer r = I mPwSer R$
9	7 8	sylan9eqr	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to s = I mPwSer R$
10	9 2	eqtr4di	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to s = S$
11	10	fveq2d	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to {Base}_{s} = {Base}_{S}$
12	11 3	eqtr4di	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to {Base}_{s} = B$
13		simplr	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to r = R$
14	13	fveq2d	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to 0_{r} = 0_{R}$
15	14 4	eqtr4di	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to 0_{r} = \underset{˙}{0}$
16	15	breq2d	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to ({finSupp}_{0_{r}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} (f))$
17	12 16	rabeqbidv	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to \{f \in {Base}_{s} \| {finSupp}_{0_{r}} (f)\} = \{f \in B \| {finSupp}_{\underset{˙}{0}} (f)\}$
18	17 5	eqtr4di	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to \{f \in {Base}_{s} \| {finSupp}_{0_{r}} (f)\} = U$
19	10 18	oveq12d	$⊢ ((i = I \land r = R) \land s = i mPwSer r) \to s ↾_{𝑠} \{f \in {Base}_{s} \| {finSupp}_{0_{r}} (f)\} = S ↾_{𝑠} U$
20	6 19	csbied	$⊢ (i = I \land r = R) \to ⦋ (i mPwSer r) / s ⦌ (s ↾_{𝑠} \{f \in {Base}_{s} \| {finSupp}_{0_{r}} (f)\}) = S ↾_{𝑠} U$
21		df-mpl	$⊢ mPoly = (i \in V, r \in V ⟼ ⦋ (i mPwSer r) / s ⦌ (s ↾_{𝑠} \{f \in {Base}_{s} \| {finSupp}_{0_{r}} (f)\}))$
22		ovex	$⊢ S ↾_{𝑠} U \in V$
23	20 21 22	ovmpoa	$⊢ (I \in V \land R \in V) \to I mPoly R = S ↾_{𝑠} U$
24		reldmmpl	$⊢ Rel dom mPoly$
25	24	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPoly R = \emptyset$
26		ress0	$⊢ \emptyset ↾_{𝑠} U = \emptyset$
27	25 26	eqtr4di	$⊢ \neg (I \in V \land R \in V) \to I mPoly R = \emptyset ↾_{𝑠} U$
28		reldmpsr	$⊢ Rel dom mPwSer$
29	28	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = \emptyset$
30	2 29	eqtrid	$⊢ \neg (I \in V \land R \in V) \to S = \emptyset$
31	30	oveq1d	$⊢ \neg (I \in V \land R \in V) \to S ↾_{𝑠} U = \emptyset ↾_{𝑠} U$
32	27 31	eqtr4d	$⊢ \neg (I \in V \land R \in V) \to I mPoly R = S ↾_{𝑠} U$
33	23 32	pm2.61i	$⊢ I mPoly R = S ↾_{𝑠} U$
34	1 33	eqtri	$⊢ P = S ↾_{𝑠} U$

Metamath Proof Explorer

Theorem mplval

Proof