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) TODO: Use in proof of quscrng if moved to main.

	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 ‘ 𝑅 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( [ 𝑋 ] ∼ ∙ [ 𝑌 ] ∼ ) = [ ( 𝑋 · 𝑌 ) ] ∼ )