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 ahortened by AV, 9-Mar-2025.)

Ref Expression
Hypotheses 2idlcpbl.x 
|- X = ( Base ` R )
2idlcpbl.r 
|- E = ( R ~QG S )
2idlcpbl.i 
|- I = ( 2Ideal ` R )
2idlcpbl.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 2idlcpbl.x 
 |-  X = ( Base ` R )
2 2idlcpbl.r 
 |-  E = ( R ~QG S )
3 2idlcpbl.i 
 |-  I = ( 2Ideal ` R )
4 2idlcpbl.t 
 |-  .x. = ( .r ` R )
5 simpll 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> R e. Ring )
6 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
7 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
8 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
9 6 7 8 3 2idlelb 
 |-  ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
10 9 simplbi 
 |-  ( S e. I -> S e. ( LIdeal ` R ) )
11 10 ad2antlr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` R ) )
12 6 lidlsubg 
 |-  ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) -> S e. ( SubGrp ` R ) )
13 5 11 12 syl2anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( SubGrp ` R ) )
14 1 2 eqger 
 |-  ( S e. ( SubGrp ` R ) -> E Er X )
15 13 14 syl 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> E Er X )
16 simprl 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> A E C )
17 15 16 ersym 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> C E A )
18 ringabl 
 |-  ( R e. Ring -> R e. Abel )
19 18 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> R e. Abel )
20 1 3 2idlss 
 |-  ( S e. I -> S C_ X )
21 20 ad2antlr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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 19 21 23 syl2anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C E A <-> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) ) )
25 17 24 mpbid 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) )
26 25 simp2d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> A e. X )
27 simprr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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 19 21 28 syl2anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( B e. X /\ D e. X /\ ( D ( -g ` R ) B ) e. S ) )
31 30 simp1d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> B e. X )
32 1 4 5 26 31 ringcld 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) e. X )
33 25 simp1d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> C e. X )
34 30 simp2d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> D e. X )
35 1 4 5 33 34 ringcld 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. D ) e. X )
36 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
37 36 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> R e. Grp )
38 1 4 5 33 31 ringcld 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. B ) e. X )
39 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 ) ) )
40 37 35 32 38 39 syl13anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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 ) ) )
41 1 4 22 5 33 34 31 ringsubdi 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. ( D ( -g ` R ) B ) ) = ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) )
42 30 simp3d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( D ( -g ` R ) B ) e. S )
43 6 1 4 lidlmcl 
 |-  ( ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) /\ ( C e. X /\ ( D ( -g ` R ) B ) e. S ) ) -> ( C .x. ( D ( -g ` R ) B ) ) e. S )
44 5 11 33 42 43 syl22anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. ( D ( -g ` R ) B ) ) e. S )
45 41 44 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) e. S )
46 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
47 1 4 7 46 opprmul 
 |-  ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) = ( ( A ( -g ` R ) C ) .x. B )
48 1 4 22 5 26 33 31 ringsubdir 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( A ( -g ` R ) C ) .x. B ) = ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) )
49 47 48 eqtrid 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) = ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) )
50 7 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
51 50 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( oppR ` R ) e. Ring )
52 9 simprbi 
 |-  ( S e. I -> S e. ( LIdeal ` ( oppR ` R ) ) )
53 52 ad2antlr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` ( oppR ` R ) ) )
54 25 simp3d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A ( -g ` R ) C ) e. S )
55 7 1 opprbas 
 |-  X = ( Base ` ( oppR ` R ) )
56 8 55 46 lidlmcl 
 |-  ( ( ( ( oppR ` R ) e. Ring /\ S e. ( LIdeal ` ( oppR ` R ) ) ) /\ ( B e. X /\ ( A ( -g ` R ) C ) e. S ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) e. S )
57 51 53 31 54 56 syl22anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) e. S )
58 49 57 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) e. S )
59 6 22 lidlsubcl 
 |-  ( ( ( R e. Ring /\ S e. ( LIdeal ` 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 )
60 5 11 45 58 59 syl22anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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 )
61 40 60 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) e. S )
62 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 ) ) )
63 19 21 62 syl2anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( 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 ) ) )
64 32 35 61 63 mpbir3and 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) E ( C .x. D ) )
65 64 ex 
 |-  ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )