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

Proof

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