Theorem selvval2lemn

Description: A lemma to illustrate the purpose of selvval2lem3 and the value of Q . Will be renamed in the future when this section is moved to main. (Contributed by SN, 5-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		selvval2lemn.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
2		selvval2lemn.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3		selvval2lemn.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
4		selvval2lemn.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
5		selvval2lemn.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
6		selvval2lemn.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
7		selvval2lemn.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
8		selvval2lemn.x	⊢ 𝑋 = ( 𝑇 ↑s ( 𝐵 ↑m 𝐼 ) )
9		selvval2lemn.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
10		selvval2lemn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		selvval2lemn.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
12		selvval2lemn.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	selvval2lem3	⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
20	5 6 7 8 9	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ CRing ∧ ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )
21	10 18 19 20	syl3anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )