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 mPoly R )
	selvcllem4.b	|- B = ( Base ` P )
	selvcllem4.u	|- U = ( ( I \ J ) mPoly R )
	selvcllem4.t	|- T = ( J mPoly U )
	selvcllem4.c	|- C = ( algSc ` T )
	selvcllem4.d	|- D = ( C o. ( algSc ` U ) )
	selvcllem4.s	|- S = ( T |`s ran D )
	selvcllem4.w	|- W = ( I mPoly S )
	selvcllem4.x	|- X = ( Base ` W )
	selvcllem4.r	|- ( ph -> R e. CRing )
	selvcllem4.j	|- ( ph -> J C_ I )
	selvcllem4.f	|- ( ph -> F e. B )
Assertion	selvcllem4	|- ( ph -> ( D o. F ) e. X )

Proof

Step	Hyp	Ref	Expression
1		selvcllem4.p	|- P = ( I mPoly R )
2		selvcllem4.b	|- B = ( Base ` P )
3		selvcllem4.u	|- U = ( ( I \ J ) mPoly R )
4		selvcllem4.t	|- T = ( J mPoly U )
5		selvcllem4.c	|- C = ( algSc ` T )
6		selvcllem4.d	|- D = ( C o. ( algSc ` U ) )
7		selvcllem4.s	|- S = ( T |`s ran D )
8		selvcllem4.w	|- W = ( I mPoly S )
9		selvcllem4.x	|- X = ( Base ` W )
10		selvcllem4.r	|- ( ph -> R e. CRing )
11		selvcllem4.j	|- ( ph -> J C_ I )
12		selvcllem4.f	|- ( ph -> F e. B )
13	1 2	mplrcl	|- ( F e. B -> I e. _V )
14	12 13	syl	|- ( ph -> I e. _V )
15	14	difexd	|- ( ph -> ( I \ J ) e. _V )
16	14 11	ssexd	|- ( ph -> J e. _V )
17	3 4 5 6 15 16 10	selvcllem2	|- ( ph -> D e. ( R RingHom T ) )
18	3 4 5 6 15 16 10	selvcllem3	|- ( ph -> ran D e. ( SubRing ` T ) )
19		ssidd	|- ( ph -> ran D C_ ran D )
20	7	resrhm2b	|- ( ( ran D e. ( SubRing ` T ) /\ ran D C_ ran D ) -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) )
21	18 19 20	syl2anc	|- ( ph -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) )
22	17 21	mpbid	|- ( ph -> D e. ( R RingHom S ) )
23		rhmghm	|- ( D e. ( R RingHom S ) -> D e. ( R GrpHom S ) )
24		ghmmhm	|- ( D e. ( R GrpHom S ) -> D e. ( R MndHom S ) )
25	22 23 24	3syl	|- ( ph -> D e. ( R MndHom S ) )
26	1 8 2 9 25 12	mhmcompl	|- ( ph -> ( D o. F ) e. X )