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 𝑇 ) )