Theorem selvcllem4

Description: The fourth argument passed to evalSub is in the domain (a polynomial in ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ). (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	selvcllem4.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvcllem4.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvcllem4.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
	selvcllem4.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
	selvcllem4.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
	selvcllem4.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
	selvcllem4.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
	selvcllem4.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
	selvcllem4.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	selvcllem4.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvcllem4.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
	selvcllem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	selvcllem4	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		selvcllem4.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		selvcllem4.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		selvcllem4.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
4		selvcllem4.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
5		selvcllem4.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
6		selvcllem4.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
7		selvcllem4.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
8		selvcllem4.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
9		selvcllem4.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
10		selvcllem4.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
11		selvcllem4.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
12		selvcllem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
13	1 2	mplrcl	⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
14	12 13	syl	⊢ ( 𝜑 → 𝐼 ∈ V )
15	14	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
16	14 11	ssexd	⊢ ( 𝜑 → 𝐽 ∈ V )
17	3 4 5 6 15 16 10	selvcllem2	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) )
18	3 4 5 6 15 16 10	selvcllem3	⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
19		ssidd	⊢ ( 𝜑 → ran 𝐷 ⊆ ran 𝐷 )
20	7	resrhm2b	⊢ ( ( ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐷 ⊆ ran 𝐷 ) → ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) ↔ 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) ) )
21	18 19 20	syl2anc	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) ↔ 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) ) )
22	17 21	mpbid	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) )
23		rhmghm	⊢ ( 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐷 ∈ ( 𝑅 GrpHom 𝑆 ) )
24		ghmmhm	⊢ ( 𝐷 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐷 ∈ ( 𝑅 MndHom 𝑆 ) )
25	22 23 24	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 MndHom 𝑆 ) )
26	1 8 2 9 25 12	mhmcompl	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 )