Theorem mplmon2

Description: Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	mplmon2.p	$$⊢P=I\mathrm{mPoly}R$$
	mplmon2.v	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	mplmon2.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplmon2.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mplmon2.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplmon2.b	$$⊢B={\mathrm{Base}}_R$$
	mplmon2.i	$$⊢\phi \to I\in W$$
	mplmon2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplmon2.k	$$⊢\phi \to K\in D$$
	mplmon2.x	$$⊢\phi \to X\in B$$
Assertion	mplmon2	$$⊢\phi \to X\underset{\dot{}}{·}\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=K,X,\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplmon2.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplmon2.v	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
3		mplmon2.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
4		mplmon2.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mplmon2.z	$$⊢\underset{\dot{}}{0}=0_R$$
6		mplmon2.b	$$⊢B={\mathrm{Base}}_R$$
7		mplmon2.i	$$⊢\phi \to I\in W$$
8		mplmon2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
9		mplmon2.k	$$⊢\phi \to K\in D$$
10		mplmon2.x	$$⊢\phi \to X\in B$$
11		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
12		eqid	$$⊢{\cdot }_R={\cdot }_R$$
13	1 11 5 4 3 7 8 9	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_P$$
14	1 2 6 11 12 3 10 13	mplvsca	$$⊢\phi \to X\underset{\dot{}}{·}\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(D\times \left\{X\right\}\right){{\cdot }_R}_f\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
15		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
16	3 15	rabex2	$$⊢D\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to D\in \mathrm{V}$$
18	10	adantr	$$⊢\left(\phi \wedge y\in D\right)\to X\in B$$
19	4	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
20	5	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
21	19 20	ifex	$$⊢if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
22	21	a1i	$$⊢\left(\phi \wedge y\in D\right)\to if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
23		fconstmpt	$$⊢D\times \left\{X\right\}=\left(y\in D⟼X\right)$$
24	23	a1i	$$⊢\phi \to D\times \left\{X\right\}=\left(y\in D⟼X\right)$$
25		eqidd	$$⊢\phi \to \left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
26	17 18 22 24 25	offval2	$$⊢\phi \to \left(D\times \left\{X\right\}\right){{\cdot }_R}_f\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
27		oveq2	$$⊢\underset{\dot{}}{1}=if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\to X{\cdot }_R\underset{\dot{}}{1}=X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
28	27	eqeq1d	$$⊢\underset{\dot{}}{1}=if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\to \left(X{\cdot }_R\underset{\dot{}}{1}=if\left(y=K,X,\underset{\dot{}}{0}\right)\leftrightarrow X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=K,X,\underset{\dot{}}{0}\right)\right)$$
29		oveq2	$$⊢\underset{\dot{}}{0}=if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\to X{\cdot }_R\underset{\dot{}}{0}=X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
30	29	eqeq1d	$$⊢\underset{\dot{}}{0}=if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\to \left(X{\cdot }_R\underset{\dot{}}{0}=if\left(y=K,X,\underset{\dot{}}{0}\right)\leftrightarrow X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=K,X,\underset{\dot{}}{0}\right)\right)$$
31	6 12 4	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X{\cdot }_R\underset{\dot{}}{1}=X$$
32	8 10 31	syl2anc	$$⊢\phi \to X{\cdot }_R\underset{\dot{}}{1}=X$$
33		iftrue	$$⊢y=K\to if\left(y=K,X,\underset{\dot{}}{0}\right)=X$$
34	33	eqcomd	$$⊢y=K\to X=if\left(y=K,X,\underset{\dot{}}{0}\right)$$
35	32 34	sylan9eq	$$⊢\left(\phi \wedge y=K\right)\to X{\cdot }_R\underset{\dot{}}{1}=if\left(y=K,X,\underset{\dot{}}{0}\right)$$
36	6 12 5	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
37	8 10 36	syl2anc	$$⊢\phi \to X{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
38		iffalse	$$⊢\neg y=K\to if\left(y=K,X,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
39	38	eqcomd	$$⊢\neg y=K\to \underset{\dot{}}{0}=if\left(y=K,X,\underset{\dot{}}{0}\right)$$
40	37 39	sylan9eq	$$⊢\left(\phi \wedge \neg y=K\right)\to X{\cdot }_R\underset{\dot{}}{0}=if\left(y=K,X,\underset{\dot{}}{0}\right)$$
41	28 30 35 40	ifbothda	$$⊢\phi \to X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=K,X,\underset{\dot{}}{0}\right)$$
42	41	mpteq2dv	$$⊢\phi \to \left(y\in D⟼X{\cdot }_{R}if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=K,X,\underset{\dot{}}{0}\right)\right)$$
43	14 26 42	3eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}\left(y\in D⟼if\left(y=K,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=K,X,\underset{\dot{}}{0}\right)\right)$$