selvcllemh

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

Step	Hyp	Ref	Expression
1		selvcllemh.u	$⊢ U = (I ∖ J) mPoly R$
2		selvcllemh.t	$⊢ T = J mPoly U$
3		selvcllemh.c	$⊢ C = algSc (T)$
4		selvcllemh.d	$⊢ D = C \circ algSc (U)$
5		selvcllemh.q	$⊢ Q = (I evalSub T) (ran D)$
6		selvcllemh.w	$⊢ W = I mPoly S$
7		selvcllemh.s	$⊢ S = T ↾_{𝑠} ran D$
8		selvcllemh.x	$⊢ X = T ↑_{𝑠} (B^{I})$
9		selvcllemh.b	$⊢ B = {Base}_{T}$
10		selvcllemh.i	$⊢ φ \to I \in V$
11		selvcllemh.r	$⊢ φ \to R \in CRing$
12		selvcllemh.j	$⊢ φ \to J \subseteq I$
13	10 12	ssexd	$⊢ φ \to J \in V$
14	10	difexd	$⊢ φ \to I ∖ J \in V$
15	1	mplcrng	$⊢ (I ∖ J \in V \land R \in CRing) \to U \in CRing$
16	14 11 15	syl2anc	$⊢ φ \to U \in CRing$
17	2	mplcrng	$⊢ (J \in V \land U \in CRing) \to T \in CRing$
18	13 16 17	syl2anc	$⊢ φ \to T \in CRing$
19	1 2 3 4 14 13 11	selvcllem3	$⊢ φ \to ran D \in SubRing (T)$
20	5 6 7 8 9	evlsrhm	$⊢ (I \in V \land T \in CRing \land ran D \in SubRing (T)) \to Q \in (W RingHom X)$
21	10 18 19 20	syl3anc	$⊢ φ \to Q \in (W RingHom X)$

Metamath Proof Explorer