Metamath Proof Explorer

Theorem qusmul

Description: Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024)

Ref Expression
Hypotheses qusmul.h ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
qusmul.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
qusmul.p ⊢ · = ( .r ‘ 𝑅 )
qusmul.a ⊢ × = ( .r ‘ 𝑄 )
qusmul.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
qusmul.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
qusmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
qusmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion qusmul ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )

Proof

Step Hyp Ref Expression
1 qusmul.h ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
2 qusmul.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 qusmul.p ⊢ · = ( .r ‘ 𝑅 )
4 qusmul.a ⊢ × = ( .r ‘ 𝑄 )
5 qusmul.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 qusmul.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7 qusmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 qusmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 1 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
10 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
11 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
12 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
13 12 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
14 11 6 13 syl2anc ⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
15 eqid ⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
16 2 15 eqger ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝐼 ) Er 𝐵 )
17 14 16 syl ⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) Er 𝐵 )
18 12 crng2idl ⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
19 5 18 syl ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
20 6 19 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
21 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
22 2 15 21 3 2idlcpbl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( 𝑥 ( 𝑅 ~QG 𝐼 ) 𝑦 ∧ 𝑧 ( 𝑅 ~QG 𝐼 ) 𝑡 ) → ( 𝑥 · 𝑧 ) ( 𝑅 ~QG 𝐼 ) ( 𝑦 · 𝑡 ) ) )
23 11 20 22 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ( 𝑅 ~QG 𝐼 ) 𝑦 ∧ 𝑧 ( 𝑅 ~QG 𝐼 ) 𝑡 ) → ( 𝑥 · 𝑧 ) ( 𝑅 ~QG 𝐼 ) ( 𝑦 · 𝑡 ) ) )
24 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
25 24 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
26 11 25 sylan ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝐵 )
27 26 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ) → ( 𝑦 · 𝑡 ) ∈ 𝐵 )
28 9 10 17 5 23 27 3 4 qusmulval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )
29 7 8 28 mpd3an23 ⊢ ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )