Theorem selvcllemh

Description: Apply the third argument ( selvcllem3 ) to show that Q is a (ring) homomorphism. (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	selvcllemh.u	|- U = ( ( I \ J ) mPoly R )
	selvcllemh.t	|- T = ( J mPoly U )
	selvcllemh.c	|- C = ( algSc ` T )
	selvcllemh.d	|- D = ( C o. ( algSc ` U ) )
	selvcllemh.q	|- Q = ( ( I evalSub T ) ` ran D )
	selvcllemh.w	|- W = ( I mPoly S )
	selvcllemh.s	|- S = ( T |`s ran D )
	selvcllemh.x	|- X = ( T ^s ( B ^m I ) )
	selvcllemh.b	|- B = ( Base ` T )
	selvcllemh.i	|- ( ph -> I e. V )
	selvcllemh.r	|- ( ph -> R e. CRing )
	selvcllemh.j	|- ( ph -> J C_ I )
Assertion	selvcllemh	|- ( ph -> Q e. ( W RingHom X ) )

Proof

Step	Hyp	Ref	Expression
1		selvcllemh.u	|- U = ( ( I \ J ) mPoly R )
2		selvcllemh.t	|- T = ( J mPoly U )
3		selvcllemh.c	|- C = ( algSc ` T )
4		selvcllemh.d	|- D = ( C o. ( algSc ` U ) )
5		selvcllemh.q	|- Q = ( ( I evalSub T ) ` ran D )
6		selvcllemh.w	|- W = ( I mPoly S )
7		selvcllemh.s	|- S = ( T |`s ran D )
8		selvcllemh.x	|- X = ( T ^s ( B ^m I ) )
9		selvcllemh.b	|- B = ( Base ` T )
10		selvcllemh.i	|- ( ph -> I e. V )
11		selvcllemh.r	|- ( ph -> R e. CRing )
12		selvcllemh.j	|- ( ph -> J C_ I )
13	10 12	ssexd	|- ( ph -> J e. _V )
14	10	difexd	|- ( ph -> ( I \ J ) e. _V )
15	1	mplcrng	|- ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. CRing )
16	14 11 15	syl2anc	|- ( ph -> U e. CRing )
17	2	mplcrng	|- ( ( J e. _V /\ U e. CRing ) -> T e. CRing )
18	13 16 17	syl2anc	|- ( ph -> T e. CRing )
19	1 2 3 4 14 13 11	selvcllem3	|- ( ph -> ran D e. ( SubRing ` T ) )
20	5 6 7 8 9	evlsrhm	|- ( ( I e. V /\ T e. CRing /\ ran D e. ( SubRing ` T ) ) -> Q e. ( W RingHom X ) )
21	10 18 19 20	syl3anc	|- ( ph -> Q e. ( W RingHom X ) )