Theorem selvcllem1

Description: T is an associative algebra. For simplicity, I stands for ( I \ J ) and we have J e. W instead of J C_ I . TODO-SN: In practice, this "simplification" makes the lemmas harder to use. (Contributed by SN, 15-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		selvcllem1.u	|- U = ( I mPoly R )
2		selvcllem1.t	|- T = ( J mPoly U )
3		selvcllem1.i	|- ( ph -> I e. V )
4		selvcllem1.j	|- ( ph -> J e. W )
5		selvcllem1.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 )