Metamath Proof Explorer

Theorem qusmulrng

Description: Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng . Similar to qusmul2 . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 28-Feb-2025)

Ref Expression
Hypotheses qusmulrng.e ⊢ ∼ = ( 𝑅 ~QG 𝑆 )
qusmulrng.h ⊢ 𝐻 = ( 𝑅 /s ∼ )
qusmulrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
qusmulrng.p ⊢ · = ( .r ‘ 𝑅 )
qusmulrng.a ⊢ ∙ = ( .r ‘ 𝐻 )
Assertion qusmulrng ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )

Proof

Step Hyp Ref Expression
1 qusmulrng.e ⊢ ∼ = ( 𝑅 ~QG 𝑆 )
2 qusmulrng.h ⊢ 𝐻 = ( 𝑅 /s ∼ )
3 qusmulrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 qusmulrng.p ⊢ · = ( .r ‘ 𝑅 )
5 qusmulrng.a ⊢ ∙ = ( .r ‘ 𝐻 )
6 2 a1i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐻 = ( 𝑅 /s ∼ ) )
7 3 a1i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐵 = ( Base ‘ 𝑅 ) )
8 3 1 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ∼ Er 𝐵 )
9 8 3ad2ant3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ∼ Er 𝐵 )
10 simp1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Rng )
11 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
12 3 1 11 4 2idlcpblrng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑 ) → ( 𝑎 · 𝑐 ) ∼ ( 𝑏 · 𝑑 ) ) )
13 10 anim1i ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) )
14 3anass ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) )
15 13 14 sylibr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) )
16 3 4 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑏 · 𝑑 ) ∈ 𝐵 )
17 15 16 syl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑏 · 𝑑 ) ∈ 𝐵 )
18 6 7 9 10 12 17 4 5 qusmulval ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )
19 18 3expb ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )