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	$⊢ U = (I ∖ J) mPoly R$
	selvval2lemn.t	$⊢ T = J mPoly U$
	selvval2lemn.c	$⊢ C = algSc (T)$
	selvval2lemn.d	$⊢ D = C \circ algSc (U)$
	selvval2lemn.q	$⊢ Q = (I evalSub T) (ran D)$
	selvval2lemn.w	$⊢ W = I mPoly S$
	selvval2lemn.s	$⊢ S = T ↾_{𝑠} ran D$
	selvval2lemn.x	$⊢ X = T ↑_{𝑠} (B^{I})$
	selvval2lemn.b	$⊢ B = {Base}_{T}$
	selvval2lemn.i	$⊢ φ \to I \in V$
	selvval2lemn.r	$⊢ φ \to R \in CRing$
	selvval2lemn.j	$⊢ φ \to J \subseteq I$
Assertion	selvval2lemn	$⊢ φ \to Q \in (W RingHom X)$

Proof

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

Metamath Proof Explorer

Theorem selvval2lemn

Proof