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	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
	qusmulcrng.v	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qusmulcrng.p	⊢ · = ( .r ‘ 𝑅 )
	qusmulcrng.a	⊢ × = ( .r ‘ 𝑄 )
	qusmulcrng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	qusmulcrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	qusmulcrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	qusmulcrng.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	qusmulcrng	⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		qusmulcrng.h	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
2		qusmulcrng.v	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		qusmulcrng.p	⊢ · = ( .r ‘ 𝑅 )
4		qusmulcrng.a	⊢ × = ( .r ‘ 𝑄 )
5		qusmulcrng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		qusmulcrng.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7		qusmulcrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		qusmulcrng.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
11	10	crng2idl	⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
12	5 11	syl	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
13	6 12	eleqtrd	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
14	1 2 3 4 9 13 7 8	qusmul2idl	⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )