Metamath Proof Explorer


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 algSc U
selvval2lem2.i φ I V
selvval2lem2.j φ J W
selvval2lem2.r φ R CRing
Assertion selvval2lem2 φ D 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 algSc U
5 selvval2lem2.i φ I V
6 selvval2lem2.j φ J W
7 selvval2lem2.r φ R CRing
8 1 2 5 6 7 selvval2lem1 φ T AssAlg
9 eqid Scalar T = Scalar T
10 3 9 asclrhm T AssAlg C Scalar T RingHom T
11 8 10 syl φ C Scalar T RingHom T
12 1 mplassa I V R CRing U AssAlg
13 5 7 12 syl2anc φ U AssAlg
14 2 6 13 mplsca φ U = Scalar T
15 14 oveq1d φ U RingHom T = Scalar T RingHom T
16 11 15 eleqtrrd φ C U RingHom T
17 eqid algSc U = algSc U
18 eqid Scalar U = Scalar U
19 17 18 asclrhm U AssAlg algSc U Scalar U RingHom U
20 13 19 syl φ algSc U Scalar U RingHom U
21 rhmco C U RingHom T algSc U Scalar U RingHom U C algSc U Scalar U RingHom T
22 16 20 21 syl2anc φ C algSc U Scalar U RingHom T
23 1 5 7 mplsca φ R = Scalar U
24 23 oveq1d φ R RingHom T = Scalar U RingHom T
25 22 24 eleqtrrd φ C algSc U R RingHom T
26 4 25 eqeltrid φ D R RingHom T