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.i	|- ( ph -> I e. V )
	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.i	|- ( ph -> I e. V )
11		selvcllem4.r	|- ( ph -> R e. CRing )
12		selvcllem4.j	|- ( ph -> J C_ I )
13		selvcllem4.f	|- ( ph -> F e. B )
14	10	difexd	|- ( ph -> ( I \ J ) e. _V )
15	10 12	ssexd	|- ( ph -> J e. _V )
16	3 4 5 6 14 15 11	selvcllem2	|- ( ph -> D e. ( R RingHom T ) )
17	3 4 5 6 14 15 11	selvcllem3	|- ( ph -> ran D e. ( SubRing ` T ) )
18		ssidd	|- ( ph -> ran D C_ ran D )
19	7	resrhm2b	|- ( ( ran D e. ( SubRing ` T ) /\ ran D C_ ran D ) -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) )
20	17 18 19	syl2anc	|- ( ph -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) )
21	16 20	mpbid	|- ( ph -> D e. ( R RingHom S ) )
22		rhmghm	|- ( D e. ( R RingHom S ) -> D e. ( R GrpHom S ) )
23		ghmmhm	|- ( D e. ( R GrpHom S ) -> D e. ( R MndHom S ) )
24	21 22 23	3syl	|- ( ph -> D e. ( R MndHom S ) )
25	1 8 2 9 10 24 13	mhmcompl	|- ( ph -> ( D o. F ) e. X )