Metamath Proof Explorer

Theorem qusmul2

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

Ref Expression
Hypotheses qusmul2.h ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
qusmul2.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
qusmul2.p ⊢ · = ( .r ‘ 𝑅 )
qusmul2.a ⊢ × = ( .r ‘ 𝑄 )
qusmul2.1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
qusmul2.2 ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
qusmul2.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
qusmul2.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion qusmul2 ( 𝜑 → ( [ 𝑋 ] ( 𝑅 ~QG 𝐼 ) × [ 𝑌 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑋 · 𝑌 ) ] ( 𝑅 ~QG 𝐼 ) )

Proof

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