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	⊢ 𝑈 = ( 𝐼 mPoly 𝑅 )
	selvcllem1.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
	selvcllem1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvcllem1.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
	selvcllem1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	selvcllem1	⊢ ( 𝜑 → 𝑇 ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		selvcllem1.u	⊢ 𝑈 = ( 𝐼 mPoly 𝑅 )
2		selvcllem1.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3		selvcllem1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		selvcllem1.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
5		selvcllem1.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6	1	mplcrng	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ CRing )
7	3 5 6	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ CRing )
8	2	mplassa	⊢ ( ( 𝐽 ∈ 𝑊 ∧ 𝑈 ∈ CRing ) → 𝑇 ∈ AssAlg )
9	4 7 8	syl2anc	⊢ ( 𝜑 → 𝑇 ∈ AssAlg )