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\mathrm{mPoly}R$$
	selvcllem1.t	$$⊢T=J\mathrm{mPoly}U$$
	selvcllem1.i	$$⊢\phi \to I\in V$$
	selvcllem1.j	$$⊢\phi \to J\in W$$
	selvcllem1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
Assertion	selvcllem1	$$⊢\phi \to T\in \mathrm{AssAlg}$$

Proof

Step	Hyp	Ref	Expression
1		selvcllem1.u	$$⊢U=I\mathrm{mPoly}R$$
2		selvcllem1.t	$$⊢T=J\mathrm{mPoly}U$$
3		selvcllem1.i	$$⊢\phi \to I\in V$$
4		selvcllem1.j	$$⊢\phi \to J\in W$$
5		selvcllem1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6	1	mplcrng	$$⊢\left(I\in V\wedge R\in \mathrm{CRing}\right)\to U\in \mathrm{CRing}$$
7	3 5 6	syl2anc	$$⊢\phi \to U\in \mathrm{CRing}$$
8	2	mplassa	$$⊢\left(J\in W\wedge U\in \mathrm{CRing}\right)\to T\in \mathrm{AssAlg}$$
9	4 7 8	syl2anc	$$⊢\phi \to T\in \mathrm{AssAlg}$$