Theorem mplmon

Description: A monomial is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplmon.s	$$⊢P=I\mathrm{mPoly}R$$
2		mplmon.b	$$⊢B={\mathrm{Base}}_P$$
3		mplmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mplmon.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mplmon.i	$$⊢\phi \to I\in W$$
7		mplmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		mplmon.x	$$⊢\phi \to X\in D$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	9 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
11	9 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
12	10 11	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
13	7 12	syl	$$⊢\phi \to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
14	13	adantr	$$⊢\left(\phi \wedge y\in D\right)\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
15	14	fmpttd	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
16		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
17		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
18	5 17	rabex2	$$⊢D\in \mathrm{V}$$
19	16 18	elmap	$$⊢\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
20	15 19	sylibr	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)$$
21		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
22		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
23	21 9 5 22 6	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^D$$
24	20 23	eleqtrrd	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
25	18	mptex	$$⊢\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
26		funmpt	$$⊢\mathrm{Fun}\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
27	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
28	25 26 27	3pm3.2i	$$⊢\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
29	28	a1i	$$⊢\phi \to \left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
30		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
31	30	a1i	$$⊢\phi \to \left\{X\right\}\in \mathrm{Fin}$$
32		eldifsni	$$⊢y\in \left(D\setminus \left\{X\right\}\right)\to y\ne X$$
33	32	adantl	$$⊢\left(\phi \wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to y\ne X$$
34	33	neneqd	$$⊢\left(\phi \wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to \neg y=X$$
35	34	iffalsed	$$⊢\left(\phi \wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
36	18	a1i	$$⊢\phi \to D\in \mathrm{V}$$
37	35 36	suppss2	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
38		suppssfifsupp	$$⊢\left(\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(\left\{X\right\}\in \mathrm{Fin}\wedge \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
39	29 31 37 38	syl12anc	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
40	1 21 22 3 2	mplelbas	$$⊢\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B\leftrightarrow \left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right)$$
41	24 39 40	sylanbrc	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$