Theorem selvcllemh

Description: Apply the third argument ( selvcllem3 ) to show that Q is a (ring) homomorphism. (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	selvcllemh.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
	selvcllemh.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
	selvcllemh.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
	selvcllemh.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
	selvcllemh.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
	selvcllemh.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
	selvcllemh.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
	selvcllemh.x	⊢ 𝑋 = ( 𝑇 ↑s ( 𝐵 ↑m 𝐼 ) )
	selvcllemh.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	selvcllemh.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvcllemh.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvcllemh.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion	selvcllemh	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		selvcllemh.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
2		selvcllemh.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3		selvcllemh.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
4		selvcllemh.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
5		selvcllemh.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
6		selvcllemh.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
7		selvcllemh.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
8		selvcllemh.x	⊢ 𝑋 = ( 𝑇 ↑s ( 𝐵 ↑m 𝐼 ) )
9		selvcllemh.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
10		selvcllemh.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		selvcllemh.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
12		selvcllemh.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
13	10 12	ssexd	⊢ ( 𝜑 → 𝐽 ∈ V )
14	10	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
15	1	mplcrng	⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ CRing )
16	14 11 15	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ CRing )
17	2	mplcrng	⊢ ( ( 𝐽 ∈ V ∧ 𝑈 ∈ CRing ) → 𝑇 ∈ CRing )
18	13 16 17	syl2anc	⊢ ( 𝜑 → 𝑇 ∈ CRing )
19	1 2 3 4 14 13 11	selvcllem3	⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
20	5 6 7 8 9	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ CRing ∧ ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )
21	10 18 19 20	syl3anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )