Metamath Proof Explorer

Theorem selvcllem2

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

Ref Expression
Hypotheses selvcllem2.u ⊢U=ImPolyR
selvcllem2.t ⊢T=JmPolyU
selvcllem2.c ⊢C=algSc⁡T
selvcllem2.d ⊢D=C∘algSc⁡U
selvcllem2.i ⊢φ→I∈V
selvcllem2.j ⊢φ→J∈W
selvcllem2.r ⊢φ→R∈CRing
Assertion selvcllem2 ⊢φ→D∈RRingHomT

Proof

Step Hyp Ref Expression
1 selvcllem2.u ⊢U=ImPolyR
2 selvcllem2.t ⊢T=JmPolyU
3 selvcllem2.c ⊢C=algSc⁡T
4 selvcllem2.d ⊢D=C∘algSc⁡U
5 selvcllem2.i ⊢φ→I∈V
6 selvcllem2.j ⊢φ→J∈W
7 selvcllem2.r ⊢φ→R∈CRing
8 1 2 5 6 7 selvcllem1 ⊢φ→T∈AssAlg
9 eqid ⊢Scalar⁡T=Scalar⁡T
10 3 9 asclrhm ⊢T∈AssAlg→C∈Scalar⁡TRingHomT
11 8 10 syl ⊢φ→C∈Scalar⁡TRingHomT
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 ⊢φ→URingHomT=Scalar⁡TRingHomT
16 11 15 eleqtrrd ⊢φ→C∈URingHomT
17 eqid ⊢algSc⁡U=algSc⁡U
18 eqid ⊢Scalar⁡U=Scalar⁡U
19 17 18 asclrhm ⊢U∈AssAlg→algSc⁡U∈Scalar⁡URingHomU
20 13 19 syl ⊢φ→algSc⁡U∈Scalar⁡URingHomU
21 rhmco ⊢C∈URingHomT∧algSc⁡U∈Scalar⁡URingHomU→C∘algSc⁡U∈Scalar⁡URingHomT
22 16 20 21 syl2anc ⊢φ→C∘algSc⁡U∈Scalar⁡URingHomT
23 1 5 7 mplsca ⊢φ→R=Scalar⁡U
24 23 oveq1d ⊢φ→RRingHomT=Scalar⁡URingHomT
25 22 24 eleqtrrd ⊢φ→C∘algSc⁡U∈RRingHomT
26 4 25 eqeltrid ⊢φ→D∈RRingHomT