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 o. ( algSc ` U ) )
	selvval2lemn.q	\|- Q = ( ( I evalSub T ) ` ran D )
	selvval2lemn.w	\|- W = ( I mPoly S )
	selvval2lemn.s	\|- S = ( T \|`s ran D )
	selvval2lemn.x	\|- X = ( T ^s ( B ^m I ) )
	selvval2lemn.b	\|- B = ( Base ` T )
	selvval2lemn.i	\|- ( ph -> I e. V )
	selvval2lemn.r	\|- ( ph -> R e. CRing )
	selvval2lemn.j	\|- ( ph -> J C_ I )
Assertion	selvval2lemn	\|- ( ph -> Q e. ( 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 o. ( algSc ` U ) )
5		selvval2lemn.q	\|- Q = ( ( I evalSub T ) ` ran D )
6		selvval2lemn.w	\|- W = ( I mPoly S )
7		selvval2lemn.s	\|- S = ( T \|`s ran D )
8		selvval2lemn.x	\|- X = ( T ^s ( B ^m I ) )
9		selvval2lemn.b	\|- B = ( Base ` T )
10		selvval2lemn.i	\|- ( ph -> I e. V )
11		selvval2lemn.r	\|- ( ph -> R e. CRing )
12		selvval2lemn.j	\|- ( ph -> J C_ I )
13	10 12	ssexd	\|- ( ph -> J e. _V )
14	10	difexd	\|- ( ph -> ( I \ J ) e. _V )
15	1	mplcrng	\|- ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. CRing )
16	14 11 15	syl2anc	\|- ( ph -> U e. CRing )
17	2	mplcrng	\|- ( ( J e. _V /\ U e. CRing ) -> T e. CRing )
18	13 16 17	syl2anc	\|- ( ph -> T e. CRing )
19	1 2 3 4 14 13 11	selvval2lem3	\|- ( ph -> ran D e. ( SubRing ` T ) )
20	5 6 7 8 9	evlsrhm	\|- ( ( I e. V /\ T e. CRing /\ ran D e. ( SubRing ` T ) ) -> Q e. ( W RingHom X ) )
21	10 18 19 20	syl3anc	\|- ( ph -> Q e. ( W RingHom X ) )

Metamath Proof Explorer

Theorem selvval2lemn

Proof