Theorem 2idlcpbl

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015) (Proof shortened by AV, 31-Mar-2025)

	Ref	Expression
Hypotheses	2idlcpblrng.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	2idlcpblrng.r	⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
	2idlcpblrng.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
	2idlcpblrng.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	2idlcpbl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2idlcpblrng.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		2idlcpblrng.r	⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
3		2idlcpblrng.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
4		2idlcpblrng.t	⊢ · = ( .r ‘ 𝑅 )
5		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
6	5	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Rng )
7		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ 𝐼 )
8		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
9		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
10		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
11	8 9 10 3	2idlelb	⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
12	11	simplbi	⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
13	8	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
14	12 13	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
15	1 2 3 4	2idlcpblrng	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )
16	6 7 14 15	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )