This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )