Theorem selvcllem4

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

Proof

Step	Hyp	Ref	Expression
1		selvcllem4.p	$$⊢P=I\mathrm{mPoly}R$$
2		selvcllem4.b	$$⊢B={\mathrm{Base}}_P$$
3		selvcllem4.u	$$⊢U=\left(I\setminus J\right)\mathrm{mPoly}R$$
4		selvcllem4.t	$$⊢T=J\mathrm{mPoly}U$$
5		selvcllem4.c	$$⊢C=\mathrm{algSc}\left(T\right)$$
6		selvcllem4.d	$$⊢D=C\circ \mathrm{algSc}\left(U\right)$$
7		selvcllem4.s	$$⊢S=T{\upharpoonright }_{𝑠}\mathrm{ran}D$$
8		selvcllem4.w	$$⊢W=I\mathrm{mPoly}S$$
9		selvcllem4.x	$$⊢X={\mathrm{Base}}_W$$
10		selvcllem4.i	$$⊢\phi \to I\in V$$
11		selvcllem4.r	$$⊢\phi \to R\in \mathrm{CRing}$$
12		selvcllem4.j	$$⊢\phi \to J\subseteq I$$
13		selvcllem4.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	selvcllem2	$$⊢\phi \to D\in \left(R\mathrm{RingHom}T\right)$$
17	3 4 5 6 14 15 11	selvcllem3	$$⊢\phi \to \mathrm{ran}D\in \mathrm{SubRing}\left(T\right)$$
18		ssidd	$$⊢\phi \to \mathrm{ran}D\subseteq \mathrm{ran}D$$
19	7	resrhm2b	$$⊢\left(\mathrm{ran}D\in \mathrm{SubRing}\left(T\right)\wedge \mathrm{ran}D\subseteq \mathrm{ran}D\right)\to \left(D\in \left(R\mathrm{RingHom}T\right)\leftrightarrow D\in \left(R\mathrm{RingHom}S\right)\right)$$
20	17 18 19	syl2anc	$$⊢\phi \to \left(D\in \left(R\mathrm{RingHom}T\right)\leftrightarrow D\in \left(R\mathrm{RingHom}S\right)\right)$$
21	16 20	mpbid	$$⊢\phi \to D\in \left(R\mathrm{RingHom}S\right)$$
22		rhmghm	$$⊢D\in \left(R\mathrm{RingHom}S\right)\to D\in \left(R\mathrm{GrpHom}S\right)$$
23		ghmmhm	$$⊢D\in \left(R\mathrm{GrpHom}S\right)\to D\in \left(R\mathrm{MndHom}S\right)$$
24	21 22 23	3syl	$$⊢\phi \to D\in \left(R\mathrm{MndHom}S\right)$$
25	1 8 2 9 10 24 13	mhmcompl	$$⊢\phi \to D\circ F\in X$$