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	$⊢ P = I mPoly R$
	selvcllem4.b	$⊢ B = {Base}_{P}$
	selvcllem4.u	$⊢ U = (I ∖ J) mPoly R$
	selvcllem4.t	$⊢ T = J mPoly U$
	selvcllem4.c	$⊢ C = algSc (T)$
	selvcllem4.d	$⊢ D = C \circ algSc (U)$
	selvcllem4.s	$⊢ S = T ↾_{𝑠} ran D$
	selvcllem4.w	$⊢ W = I mPoly S$
	selvcllem4.x	$⊢ X = {Base}_{W}$
	selvcllem4.r	$⊢ φ \to R \in CRing$
	selvcllem4.j	$⊢ φ \to J \subseteq I$
	selvcllem4.f	$⊢ φ \to F \in B$
Assertion	selvcllem4	$⊢ φ \to D \circ F \in X$

Proof

Step	Hyp	Ref	Expression
1		selvcllem4.p	$⊢ P = I mPoly R$
2		selvcllem4.b	$⊢ B = {Base}_{P}$
3		selvcllem4.u	$⊢ U = (I ∖ J) mPoly R$
4		selvcllem4.t	$⊢ T = J mPoly U$
5		selvcllem4.c	$⊢ C = algSc (T)$
6		selvcllem4.d	$⊢ D = C \circ algSc (U)$
7		selvcllem4.s	$⊢ S = T ↾_{𝑠} ran D$
8		selvcllem4.w	$⊢ W = I mPoly S$
9		selvcllem4.x	$⊢ X = {Base}_{W}$
10		selvcllem4.r	$⊢ φ \to R \in CRing$
11		selvcllem4.j	$⊢ φ \to J \subseteq I$
12		selvcllem4.f	$⊢ φ \to F \in B$
13	1 2	mplrcl	$⊢ F \in B \to I \in V$
14	12 13	syl	$⊢ φ \to I \in V$
15	14	difexd	$⊢ φ \to I ∖ J \in V$
16	14 11	ssexd	$⊢ φ \to J \in V$
17	3 4 5 6 15 16 10	selvcllem2	$⊢ φ \to D \in (R RingHom T)$
18	3 4 5 6 15 16 10	selvcllem3	$⊢ φ \to ran D \in SubRing (T)$
19		ssidd	$⊢ φ \to ran D \subseteq ran D$
20	7	resrhm2b	$⊢ (ran D \in SubRing (T) \land ran D \subseteq ran D) \to (D \in (R RingHom T) \leftrightarrow D \in (R RingHom S))$
21	18 19 20	syl2anc	$⊢ φ \to (D \in (R RingHom T) \leftrightarrow D \in (R RingHom S))$
22	17 21	mpbid	$⊢ φ \to D \in (R RingHom S)$
23		rhmghm	$⊢ D \in (R RingHom S) \to D \in (R GrpHom S)$
24		ghmmhm	$⊢ D \in (R GrpHom S) \to D \in (R MndHom S)$
25	22 23 24	3syl	$⊢ φ \to D \in (R MndHom S)$
26	1 8 2 9 25 12	mhmcompl	$⊢ φ \to D \circ F \in X$

Metamath Proof Explorer

Theorem selvcllem4

Proof