Metamath Proof Explorer

Theorem 2idlcpblrng

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-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 2idlcpblrng 
|- ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( 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 simpl1 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> R e. Rng )
6 simpl3 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> S e. ( SubGrp ` R ) )
7 1 2 eqger 
 |-  ( S e. ( SubGrp ` R ) -> E Er X )
8 6 7 syl 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> E Er X )
9 simprl 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> A E C )
10 8 9 ersym 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> C E A )
11 rngabl 
 |-  ( R e. Rng -> R e. Abel )
12 11 3ad2ant1 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> R e. Abel )
13 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
14 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
15 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
16 13 14 15 3 2idlelb 
 |-  ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
17 16 simplbi 
 |-  ( S e. I -> S e. ( LIdeal ` R ) )
18 17 3ad2ant2 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> S e. ( LIdeal ` R ) )
19 18 adantr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` R ) )
20 1 13 lidlss 
 |-  ( S e. ( LIdeal ` R ) -> S C_ X )
21 19 20 syl 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> S C_ X )
22 eqid 
 |-  ( -g ` R ) = ( -g ` R )
23 1 22 2 eqgabl 
 |-  ( ( R e. Abel /\ S C_ X ) -> ( C E A <-> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) ) )
24 12 21 23 syl2an2r 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C E A <-> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) ) )
25 10 24 mpbid 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) )
26 25 simp2d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> A e. X )
27 simprr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> B E D )
28 1 22 2 eqgabl 
 |-  ( ( R e. Abel /\ S C_ X ) -> ( B E D <-> ( B e. X /\ D e. X /\ ( D ( -g ` R ) B ) e. S ) ) )
29 12 21 28 syl2an2r 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( B E D <-> ( B e. X /\ D e. X /\ ( D ( -g ` R ) B ) e. S ) ) )
30 27 29 mpbid 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( B e. X /\ D e. X /\ ( D ( -g ` R ) B ) e. S ) )
31 30 simp1d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> B e. X )
32 1 4 rngcl 
 |-  ( ( R e. Rng /\ A e. X /\ B e. X ) -> ( A .x. B ) e. X )
33 5 26 31 32 syl3anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) e. X )
34 25 simp1d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> C e. X )
35 30 simp2d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> D e. X )
36 1 4 rngcl 
 |-  ( ( R e. Rng /\ C e. X /\ D e. X ) -> ( C .x. D ) e. X )
37 5 34 35 36 syl3anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C .x. D ) e. X )
38 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
39 38 3ad2ant1 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> R e. Grp )
40 39 adantr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> R e. Grp )
41 1 4 rngcl 
 |-  ( ( R e. Rng /\ C e. X /\ B e. X ) -> ( C .x. B ) e. X )
42 5 34 31 41 syl3anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C .x. B ) e. X )
43 1 22 grpnnncan2 
 |-  ( ( R e. Grp /\ ( ( C .x. D ) e. X /\ ( A .x. B ) e. X /\ ( C .x. B ) e. X ) ) -> ( ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) ( -g ` R ) ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) ) = ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) )
44 40 37 33 42 43 syl13anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) ( -g ` R ) ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) ) = ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) )
45 1 4 22 5 34 35 31 rngsubdi 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C .x. ( D ( -g ` R ) B ) ) = ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) )
46 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
47 46 subg0cl 
 |-  ( S e. ( SubGrp ` R ) -> ( 0g ` R ) e. S )
48 47 3ad2ant3 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( 0g ` R ) e. S )
49 48 adantr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( 0g ` R ) e. S )
50 30 simp3d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( D ( -g ` R ) B ) e. S )
51 46 1 4 13 rnglidlmcl 
 |-  ( ( ( R e. Rng /\ S e. ( LIdeal ` R ) /\ ( 0g ` R ) e. S ) /\ ( C e. X /\ ( D ( -g ` R ) B ) e. S ) ) -> ( C .x. ( D ( -g ` R ) B ) ) e. S )
52 5 19 49 34 50 51 syl32anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( C .x. ( D ( -g ` R ) B ) ) e. S )
53 45 52 eqeltrrd 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) e. S )
54 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
55 1 4 14 54 opprmul 
 |-  ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) = ( ( A ( -g ` R ) C ) .x. B )
56 1 4 22 5 26 34 31 rngsubdir 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( A ( -g ` R ) C ) .x. B ) = ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) )
57 55 56 eqtrid 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) = ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) )
58 14 opprrng 
 |-  ( R e. Rng -> ( oppR ` R ) e. Rng )
59 58 3ad2ant1 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( oppR ` R ) e. Rng )
60 59 adantr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( oppR ` R ) e. Rng )
61 16 simprbi 
 |-  ( S e. I -> S e. ( LIdeal ` ( oppR ` R ) ) )
62 61 3ad2ant2 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> S e. ( LIdeal ` ( oppR ` R ) ) )
63 62 adantr 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` ( oppR ` R ) ) )
64 25 simp3d 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( A ( -g ` R ) C ) e. S )
65 14 46 oppr0 
 |-  ( 0g ` R ) = ( 0g ` ( oppR ` R ) )
66 14 1 opprbas 
 |-  X = ( Base ` ( oppR ` R ) )
67 65 66 54 15 rnglidlmcl 
 |-  ( ( ( ( oppR ` R ) e. Rng /\ S e. ( LIdeal ` ( oppR ` R ) ) /\ ( 0g ` R ) e. S ) /\ ( B e. X /\ ( A ( -g ` R ) C ) e. S ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) e. S )
68 60 63 49 31 64 67 syl32anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) e. S )
69 57 68 eqeltrrd 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) e. S )
70 22 subgsubcl 
 |-  ( ( S e. ( SubGrp ` R ) /\ ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) e. S /\ ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) e. S ) -> ( ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) ( -g ` R ) ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) ) e. S )
71 6 53 69 70 syl3anc 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) ( -g ` R ) ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) ) e. S )
72 44 71 eqeltrrd 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) e. S )
73 1 22 2 eqgabl 
 |-  ( ( R e. Abel /\ S C_ X ) -> ( ( A .x. B ) E ( C .x. D ) <-> ( ( A .x. B ) e. X /\ ( C .x. D ) e. X /\ ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) e. S ) ) )
74 12 21 73 syl2an2r 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( ( A .x. B ) E ( C .x. D ) <-> ( ( A .x. B ) e. X /\ ( C .x. D ) e. X /\ ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) e. S ) ) )
75 33 37 72 74 mpbir3and 
 |-  ( ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) E ( C .x. D ) )
76 75 ex 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )