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 /s ( R ~QG I ) )
	qusmulcrng.v	|- B = ( Base ` R )
	qusmulcrng.p	|- .x. = ( .r ` R )
	qusmulcrng.a	|- .X. = ( .r ` Q )
	qusmulcrng.r	|- ( ph -> R e. CRing )
	qusmulcrng.i	|- ( ph -> I e. ( LIdeal ` R ) )
	qusmulcrng.x	|- ( ph -> X e. B )
	qusmulcrng.y	|- ( ph -> Y e. B )
Assertion	qusmulcrng	|- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )

Proof

Step	Hyp	Ref	Expression
1		qusmulcrng.h	|- Q = ( R /s ( R ~QG I ) )
2		qusmulcrng.v	|- B = ( Base ` R )
3		qusmulcrng.p	|- .x. = ( .r ` R )
4		qusmulcrng.a	|- .X. = ( .r ` Q )
5		qusmulcrng.r	|- ( ph -> R e. CRing )
6		qusmulcrng.i	|- ( ph -> I e. ( LIdeal ` R ) )
7		qusmulcrng.x	|- ( ph -> X e. B )
8		qusmulcrng.y	|- ( ph -> Y e. B )
9	5	crngringd	|- ( ph -> R e. Ring )
10		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
11	10	crng2idl	|- ( R e. CRing -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
12	5 11	syl	|- ( ph -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
13	6 12	eleqtrd	|- ( ph -> I e. ( 2Ideal ` R ) )
14	1 2 3 4 9 13 7 8	qusmul2idl	|- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )