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 
|- X = ( Base ` R )
2idlcpblrng.r 
|- E = ( R ~QG S )
2idlcpblrng.i 
|- I = ( 2Ideal ` R )
2idlcpblrng.t 
|- .x. = ( .r ` R )
Assertion 2idlcpbl 
|- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )

Proof

Step Hyp Ref Expression
1 2idlcpblrng.x 
 |-  X = ( Base ` R )
2 2idlcpblrng.r 
 |-  E = ( R ~QG S )
3 2idlcpblrng.i 
 |-  I = ( 2Ideal ` R )
4 2idlcpblrng.t 
 |-  .x. = ( .r ` R )
5 ringrng 
 |-  ( R e. Ring -> R e. Rng )
6 5 adantr 
 |-  ( ( R e. Ring /\ S e. I ) -> R e. Rng )
7 simpr 
 |-  ( ( R e. Ring /\ S e. I ) -> S e. I )
8 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
9 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
10 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
11 8 9 10 3 2idlelb 
 |-  ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
12 11 simplbi 
 |-  ( S e. I -> S e. ( LIdeal ` R ) )
13 8 lidlsubg 
 |-  ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) -> S e. ( SubGrp ` R ) )
14 12 13 sylan2 
 |-  ( ( R e. Ring /\ S e. I ) -> S e. ( SubGrp ` R ) )
15 1 2 3 4 2idlcpblrng 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
16 6 7 14 15 syl3anc 
 |-  ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )