Theorem selvval2lem4

Description: The fourth argument passed to evalSub is in the domain (a polynomial in ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ). (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	selvval2lem4.p	$$⊢P=I\mathrm{mPoly}R$$
	selvval2lem4.b	$$⊢B={\mathrm{Base}}_P$$
	selvval2lem4.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
	selvval2lem4.t	$$⊢T=J\mathrm{mPoly}U$$
	selvval2lem4.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
	selvval2lem4.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
	selvval2lem4.s	$$⊢S=T{\upharpoonright }_{𝑠}\mathrm{ran}D$$
	selvval2lem4.w	$$⊢W=I\mathrm{mPoly}S$$
	selvval2lem4.x	$$⊢X={\mathrm{Base}}_W$$
	selvval2lem4.i	$$⊢\phi \to I\in V$$
	selvval2lem4.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	selvval2lem4.j	$$⊢\phi \to J\subseteq I$$
	selvval2lem4.f	$$⊢\phi \to F\in B$$
Assertion	selvval2lem4	$$⊢\phi \to D\circ F\in X$$

Proof

Step	Hyp	Ref	Expression
1		selvval2lem4.p	$$⊢P=I\mathrm{mPoly}R$$
2		selvval2lem4.b	$$⊢B={\mathrm{Base}}_P$$
3		selvval2lem4.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
4		selvval2lem4.t	$$⊢T=J\mathrm{mPoly}U$$
5		selvval2lem4.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
6		selvval2lem4.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
7		selvval2lem4.s	$$⊢S=T{\upharpoonright }_{𝑠}\mathrm{ran}D$$
8		selvval2lem4.w	$$⊢W=I\mathrm{mPoly}S$$
9		selvval2lem4.x	$$⊢X={\mathrm{Base}}_W$$
10		selvval2lem4.i	$$⊢\phi \to I\in V$$
11		selvval2lem4.r	$$⊢\phi \to R\in \mathrm{CRing}$$
12		selvval2lem4.j	$$⊢\phi \to J\subseteq I$$
13		selvval2lem4.f	$$⊢\phi \to F\in B$$
14	10	difexd	$$⊢\phi \to I\setminus J\in \mathrm{V}$$
15	10 12	ssexd	$$⊢\phi \to J\in \mathrm{V}$$
16	3 4 5 6 14 15 11	selvval2lem2	$$⊢\phi \to D\in \left(R\mathrm{RingHom}T\right)$$
17		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
18		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
19	17 18	rhmf	$$⊢D\in \left(R\mathrm{RingHom}T\right)\to D:{\mathrm{Base}}_R⟶{\mathrm{Base}}_T$$
20		ffrn	$$⊢D:{\mathrm{Base}}_R⟶{\mathrm{Base}}_T\to D:{\mathrm{Base}}_R⟶\mathrm{ran}D$$
21	16 19 20	3syl	$$⊢\phi \to D:{\mathrm{Base}}_R⟶\mathrm{ran}D$$
22	3 4 5 6 14 15 11	selvval2lem3	$$⊢\phi \to \mathrm{ran}D\in \mathrm{SubRing}\left(T\right)$$
23	18	subrgss	$$⊢\mathrm{ran}D\in \mathrm{SubRing}\left(T\right)\to \mathrm{ran}D\subseteq {\mathrm{Base}}_T$$
24	7 18	ressbas2	$$⊢\mathrm{ran}D\subseteq {\mathrm{Base}}_T\to \mathrm{ran}D={\mathrm{Base}}_S$$
25	22 23 24	3syl	$$⊢\phi \to \mathrm{ran}D={\mathrm{Base}}_S$$
26	25	feq3d	$$⊢\phi \to \left(D:{\mathrm{Base}}_R⟶\mathrm{ran}D\leftrightarrow D:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S\right)$$
27	21 26	mpbid	$$⊢\phi \to D:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
28		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
29	1 17 2 28 13	mplelf	$$⊢\phi \to F:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
30	27 29	fcod	$$⊢\phi \to \left(D\circ F\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_S$$
31		fvexd	$$⊢\phi \to {\mathrm{Base}}_S\in \mathrm{V}$$
32		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
33	32	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
34	33	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
35	31 34	elmapd	$$⊢\phi \to \left(D\circ F\in \left({{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\leftrightarrow \left(D\circ F\right):\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_S\right)$$
36	30 35	mpbird	$$⊢\phi \to D\circ F\in \left({{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
37		eqid	$$⊢I\mathrm{mPwSer}S=I\mathrm{mPwSer}S$$
38		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
39		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
40	37 38 28 39 10	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={{\mathrm{Base}}_S}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
41	36 40	eleqtrrd	$$⊢\phi \to D\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
42		fvexd	$$⊢\phi \to 0_S\in \mathrm{V}$$
43		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
44		eqid	$$⊢0_R=0_R$$
45	17 44	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
46	11 43 45	3syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
47		ssidd	$$⊢\phi \to {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
48		fvexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
49	1 2 44 13 11	mplelsfi	$$⊢\phi \to {finSupp}_{0_R}\left(F\right)$$
50	6	a1i	$$⊢\phi \to D=C\circ \mathrm{algSc}\left(U\right)$$
51	50	fveq1d	$$⊢\phi \to D\left(0_R\right)=\left(C\circ \mathrm{algSc}\left(U\right)\right)\left(0_R\right)$$
52		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
53		eqid	$$⊢\mathrm{algSc}\left(U\right)=\mathrm{algSc}\left(U\right)$$
54	11 43	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
55	3 52 17 53 14 54	mplasclf	$$⊢\phi \to \mathrm{algSc}\left(U\right):{\mathrm{Base}}_R⟶{\mathrm{Base}}_U$$
56	55 46	fvco3d	$$⊢\phi \to \left(C\circ \mathrm{algSc}\left(U\right)\right)\left(0_R\right)=C\left(\mathrm{algSc}\left(U\right)\left(0_R\right)\right)$$
57	3 14 11	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(U\right)$$
58	57	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(U\right)}$$
59	58	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(0_R\right)=\mathrm{algSc}\left(U\right)\left(0_{\mathrm{Scalar}\left(U\right)}\right)$$
60		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
61	3	mplassa	$$⊢\left(I\setminus J\in \mathrm{V}\wedge R\in \mathrm{CRing}\right)\to U\in \mathrm{AssAlg}$$
62	14 11 61	syl2anc	$$⊢\phi \to U\in \mathrm{AssAlg}$$
63		assalmod	$$⊢U\in \mathrm{AssAlg}\to U\in \mathrm{LMod}$$
64	62 63	syl	$$⊢\phi \to U\in \mathrm{LMod}$$
65		assaring	$$⊢U\in \mathrm{AssAlg}\to U\in \mathrm{Ring}$$
66	62 65	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
67	53 60 64 66	ascl0	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(0_{\mathrm{Scalar}\left(U\right)}\right)=0_U$$
68	59 67	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(0_R\right)=0_U$$
69	68	fveq2d	$$⊢\phi \to C\left(\mathrm{algSc}\left(U\right)\left(0_R\right)\right)=C\left(0_U\right)$$
70	4 15 62	mplsca	$$⊢\phi \to U=\mathrm{Scalar}\left(T\right)$$
71	70	fveq2d	$$⊢\phi \to 0_U=0_{\mathrm{Scalar}\left(T\right)}$$
72	71	fveq2d	$$⊢\phi \to C\left(0_U\right)=C\left(0_{\mathrm{Scalar}\left(T\right)}\right)$$
73		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
74	3 4 14 15 11	selvval2lem1	$$⊢\phi \to T\in \mathrm{AssAlg}$$
75		assalmod	$$⊢T\in \mathrm{AssAlg}\to T\in \mathrm{LMod}$$
76	74 75	syl	$$⊢\phi \to T\in \mathrm{LMod}$$
77		assaring	$$⊢T\in \mathrm{AssAlg}\to T\in \mathrm{Ring}$$
78	74 77	syl	$$⊢\phi \to T\in \mathrm{Ring}$$
79	5 73 76 78	ascl0	$$⊢\phi \to C\left(0_{\mathrm{Scalar}\left(T\right)}\right)=0_T$$
80		subrgsubg	$$⊢\mathrm{ran}D\in \mathrm{SubRing}\left(T\right)\to \mathrm{ran}D\in \mathrm{SubGrp}\left(T\right)$$
81		eqid	$$⊢0_T=0_T$$
82	7 81	subg0	$$⊢\mathrm{ran}D\in \mathrm{SubGrp}\left(T\right)\to 0_T=0_S$$
83	22 80 82	3syl	$$⊢\phi \to 0_T=0_S$$
84	79 83	eqtrd	$$⊢\phi \to C\left(0_{\mathrm{Scalar}\left(T\right)}\right)=0_S$$
85	69 72 84	3eqtrd	$$⊢\phi \to C\left(\mathrm{algSc}\left(U\right)\left(0_R\right)\right)=0_S$$
86	51 56 85	3eqtrd	$$⊢\phi \to D\left(0_R\right)=0_S$$
87	42 46 29 21 47 34 48 49 86	fsuppcor	$$⊢\phi \to {finSupp}_{0_S}\left(\left(D\circ F\right)\right)$$
88		eqid	$$⊢0_S=0_S$$
89	8 37 39 88 9	mplelbas	$$⊢D\circ F\in X\leftrightarrow \left(D\circ F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}\wedge {finSupp}_{0_S}\left(\left(D\circ F\right)\right)\right)$$
90	41 87 89	sylanbrc	$$⊢\phi \to D\circ F\in X$$