Theorem qusmulcrng

Description: Value of the ring operation in a quotient ring of a commutative ring. (Contributed by Thierry Arnoux, 1-Sep-2024) (Proof shortened by metakunt, 3-Jun-2025)

	Ref	Expression
Hypotheses	qusmulcrng.h	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
	qusmulcrng.v	$$⊢B={\mathrm{Base}}_R$$
	qusmulcrng.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	qusmulcrng.a	$$⊢\underset{\dot{}}{\times }={\cdot }_Q$$
	qusmulcrng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	qusmulcrng.i	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
	qusmulcrng.x	$$⊢\phi \to X\in B$$
	qusmulcrng.y	$$⊢\phi \to Y\in B$$
Assertion	qusmulcrng	$$⊢\phi \to \left[X\right]\left(R{~}_{\mathit{QG}}I\right)\underset{\dot{}}{\times }\left[Y\right]\left(R{~}_{\mathit{QG}}I\right)=\left[\left(X\underset{\dot{}}{·}Y\right)\right]\left(R{~}_{\mathit{QG}}I\right)$$

Proof

Step	Hyp	Ref	Expression
1		qusmulcrng.h	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
2		qusmulcrng.v	$$⊢B={\mathrm{Base}}_R$$
3		qusmulcrng.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		qusmulcrng.a	$$⊢\underset{\dot{}}{\times }={\cdot }_Q$$
5		qusmulcrng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		qusmulcrng.i	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
7		qusmulcrng.x	$$⊢\phi \to X\in B$$
8		qusmulcrng.y	$$⊢\phi \to Y\in B$$
9	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
10		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
11	10	crng2idl	$$⊢R\in \mathrm{CRing}\to \mathrm{LIdeal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
12	5 11	syl	$$⊢\phi \to \mathrm{LIdeal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
13	6 12	eleqtrd	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
14	1 2 3 4 9 13 7 8	qusmul2idl	$$⊢\phi \to \left[X\right]\left(R{~}_{\mathit{QG}}I\right)\underset{\dot{}}{\times }\left[Y\right]\left(R{~}_{\mathit{QG}}I\right)=\left[\left(X\underset{\dot{}}{·}Y\right)\right]\left(R{~}_{\mathit{QG}}I\right)$$