Theorem selvval2lem2

Description: D is a ring homomorphism. (Contributed by SN, 15-Dec-2023)

	Ref	Expression
Hypotheses	selvval2lem2.u	|- U = ( I mPoly R )
	selvval2lem2.t	|- T = ( J mPoly U )
	selvval2lem2.c	|- C = ( algSc ` T )
	selvval2lem2.d	|- D = ( C o. ( algSc ` U ) )
	selvval2lem2.i	|- ( ph -> I e. V )
	selvval2lem2.j	|- ( ph -> J e. W )
	selvval2lem2.r	|- ( ph -> R e. CRing )
Assertion	selvval2lem2	|- ( ph -> D e. ( R RingHom T ) )

Proof

Step	Hyp	Ref	Expression
1		selvval2lem2.u	|- U = ( I mPoly R )
2		selvval2lem2.t	|- T = ( J mPoly U )
3		selvval2lem2.c	|- C = ( algSc ` T )
4		selvval2lem2.d	|- D = ( C o. ( algSc ` U ) )
5		selvval2lem2.i	|- ( ph -> I e. V )
6		selvval2lem2.j	|- ( ph -> J e. W )
7		selvval2lem2.r	|- ( ph -> R e. CRing )
8	1 2 5 6 7	selvval2lem1	|- ( ph -> T e. AssAlg )
9		eqid	|- ( Scalar ` T ) = ( Scalar ` T )
10	3 9	asclrhm	|- ( T e. AssAlg -> C e. ( ( Scalar ` T ) RingHom T ) )
11	8 10	syl	|- ( ph -> C e. ( ( Scalar ` T ) RingHom T ) )
12	1	mplassa	|- ( ( I e. V /\ R e. CRing ) -> U e. AssAlg )
13	5 7 12	syl2anc	|- ( ph -> U e. AssAlg )
14	2 6 13	mplsca	|- ( ph -> U = ( Scalar ` T ) )
15	14	oveq1d	|- ( ph -> ( U RingHom T ) = ( ( Scalar ` T ) RingHom T ) )
16	11 15	eleqtrrd	|- ( ph -> C e. ( U RingHom T ) )
17		eqid	|- ( algSc ` U ) = ( algSc ` U )
18		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
19	17 18	asclrhm	|- ( U e. AssAlg -> ( algSc ` U ) e. ( ( Scalar ` U ) RingHom U ) )
20	13 19	syl	|- ( ph -> ( algSc ` U ) e. ( ( Scalar ` U ) RingHom U ) )
21		rhmco	|- ( ( C e. ( U RingHom T ) /\ ( algSc ` U ) e. ( ( Scalar ` U ) RingHom U ) ) -> ( C o. ( algSc ` U ) ) e. ( ( Scalar ` U ) RingHom T ) )
22	16 20 21	syl2anc	|- ( ph -> ( C o. ( algSc ` U ) ) e. ( ( Scalar ` U ) RingHom T ) )
23	1 5 7	mplsca	|- ( ph -> R = ( Scalar ` U ) )
24	23	oveq1d	|- ( ph -> ( R RingHom T ) = ( ( Scalar ` U ) RingHom T ) )
25	22 24	eleqtrrd	|- ( ph -> ( C o. ( algSc ` U ) ) e. ( R RingHom T ) )
26	4 25	eqeltrid	|- ( ph -> D e. ( R RingHom T ) )