This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 ) )