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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	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.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		selvcllem4.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
12		selvcllem4.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
13		selvcllem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
14	10	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
15	10 12	ssexd	⊢ ( 𝜑 → 𝐽 ∈ V )
16	3 4 5 6 14 15 11	selvcllem2	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) )
17	3 4 5 6 14 15 11	selvcllem3	⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
18		ssidd	⊢ ( 𝜑 → ran 𝐷 ⊆ ran 𝐷 )
19	7	resrhm2b	⊢ ( ( ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐷 ⊆ ran 𝐷 ) → ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) ↔ 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) ) )
20	17 18 19	syl2anc	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) ↔ 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) ) )
21	16 20	mpbid	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) )
22		rhmghm	⊢ ( 𝐷 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐷 ∈ ( 𝑅 GrpHom 𝑆 ) )
23		ghmmhm	⊢ ( 𝐷 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐷 ∈ ( 𝑅 MndHom 𝑆 ) )
24	21 22 23	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 MndHom 𝑆 ) )
25	1 8 2 9 10 24 13	mhmcompl	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 )