This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem selvcllem2

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

Ref Expression
Hypotheses selvcllem2.u ⊢ 𝑈 = ( 𝐼 mPoly 𝑅 )
selvcllem2.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvcllem2.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
selvcllem2.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
selvcllem2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvcllem2.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
selvcllem2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion selvcllem2 ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 selvcllem2.u ⊢ 𝑈 = ( 𝐼 mPoly 𝑅 )
2 selvcllem2.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3 selvcllem2.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
4 selvcllem2.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
5 selvcllem2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 selvcllem2.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
7 selvcllem2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 1 2 5 6 7 selvcllem1 ⊢ ( 𝜑 → 𝑇 ∈ AssAlg )
9 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
10 3 9 asclrhm ⊢ ( 𝑇 ∈ AssAlg → 𝐶 ∈ ( ( Scalar ‘ 𝑇 ) RingHom 𝑇 ) )
11 8 10 syl ⊢ ( 𝜑 → 𝐶 ∈ ( ( Scalar ‘ 𝑇 ) RingHom 𝑇 ) )
12 1 mplassa ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ AssAlg )
13 5 7 12 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ AssAlg )
14 2 6 13 mplsca ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑇 ) )
15 14 oveq1d ⊢ ( 𝜑 → ( 𝑈 RingHom 𝑇 ) = ( ( Scalar ‘ 𝑇 ) RingHom 𝑇 ) )
16 11 15 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 RingHom 𝑇 ) )
17 eqid ⊢ ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
18 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
19 17 18 asclrhm ⊢ ( 𝑈 ∈ AssAlg → ( algSc ‘ 𝑈 ) ∈ ( ( Scalar ‘ 𝑈 ) RingHom 𝑈 ) )
20 13 19 syl ⊢ ( 𝜑 → ( algSc ‘ 𝑈 ) ∈ ( ( Scalar ‘ 𝑈 ) RingHom 𝑈 ) )
21 rhmco ⊢ ( ( 𝐶 ∈ ( 𝑈 RingHom 𝑇 ) ∧ ( algSc ‘ 𝑈 ) ∈ ( ( Scalar ‘ 𝑈 ) RingHom 𝑈 ) ) → ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∈ ( ( Scalar ‘ 𝑈 ) RingHom 𝑇 ) )
22 16 20 21 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∈ ( ( Scalar ‘ 𝑈 ) RingHom 𝑇 ) )
23 1 5 7 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑈 ) )
24 23 oveq1d ⊢ ( 𝜑 → ( 𝑅 RingHom 𝑇 ) = ( ( Scalar ‘ 𝑈 ) RingHom 𝑇 ) )
25 22 24 eleqtrrd ⊢ ( 𝜑 → ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 RingHom 𝑇 ) )
26 4 25 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) )