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