Theorem selvval2lem1

Description: T is an associative algebra. For simplicity, I stands for ( I \ J ) and we have J e. W instead of J C_ I . (Contributed by SN, 15-Dec-2023)

	Ref	Expression
Hypotheses	selvval2lem1.u	|- U = ( I mPoly R )
	selvval2lem1.t	|- T = ( J mPoly U )
	selvval2lem1.i	|- ( ph -> I e. V )
	selvval2lem1.j	|- ( ph -> J e. W )
	selvval2lem1.r	|- ( ph -> R e. CRing )
Assertion	selvval2lem1	|- ( ph -> T e. AssAlg )

Proof

Step	Hyp	Ref	Expression
1		selvval2lem1.u	|- U = ( I mPoly R )
2		selvval2lem1.t	|- T = ( J mPoly U )
3		selvval2lem1.i	|- ( ph -> I e. V )
4		selvval2lem1.j	|- ( ph -> J e. W )
5		selvval2lem1.r	|- ( ph -> R e. CRing )
6	1	mplcrng	|- ( ( I e. V /\ R e. CRing ) -> U e. CRing )
7	3 5 6	syl2anc	|- ( ph -> U e. CRing )
8	2	mplassa	|- ( ( J e. W /\ U e. CRing ) -> T e. AssAlg )
9	4 7 8	syl2anc	|- ( ph -> T e. AssAlg )