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