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)

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 2idlval 
 |-  I = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) )
10 9 elin2 
 |-  ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
11 10 simplbi 
 |-  ( S e. I -> S e. ( LIdeal ` R ) )
12 11 ad2antlr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` R ) )
13 6 lidlsubg 
 |-  ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) -> S e. ( SubGrp ` R ) )
14 5 12 13 syl2anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( SubGrp ` R ) )
15 1 2 eqger 
 |-  ( S e. ( SubGrp ` R ) -> E Er X )
16 14 15 syl 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> E Er X )
17 simprl 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> A E C )
18 16 17 ersym 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> C E A )
19 ringabl 
 |-  ( R e. Ring -> R e. Abel )
20 19 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> R e. Abel )
21 1 6 lidlss 
 |-  ( S e. ( LIdeal ` R ) -> S C_ X )
22 12 21 syl 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S C_ X )
23 eqid 
 |-  ( -g ` R ) = ( -g ` R )
24 1 23 2 eqgabl 
 |-  ( ( R e. Abel /\ S C_ X ) -> ( C E A <-> ( C e. X /\ A e. X /\ ( A ( -g ` R ) C ) e. S ) ) )
25 20 22 24 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 ) ) )
26 18 25 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 ) )
27 26 simp2d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> A e. X )
28 simprr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> B E D )
29 1 23 2 eqgabl 
 |-  ( ( R e. Abel /\ S C_ X ) -> ( B E D <-> ( B e. X /\ D e. X /\ ( D ( -g ` R ) B ) e. S ) ) )
30 20 22 29 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 ) ) )
31 28 30 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 ) )
32 31 simp1d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> B e. X )
33 1 4 ringcl 
 |-  ( ( R e. Ring /\ A e. X /\ B e. X ) -> ( A .x. B ) e. X )
34 5 27 32 33 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) e. X )
35 26 simp1d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> C e. X )
36 31 simp2d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> D e. X )
37 1 4 ringcl 
 |-  ( ( R e. Ring /\ C e. X /\ D e. X ) -> ( C .x. D ) e. X )
38 5 35 36 37 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. D ) e. X )
39 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
40 39 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> R e. Grp )
41 1 4 ringcl 
 |-  ( ( R e. Ring /\ C e. X /\ B e. X ) -> ( C .x. B ) e. X )
42 5 35 32 41 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. B ) e. X )
43 1 23 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 38 34 42 43 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 ) ) )
45 1 4 23 5 35 36 32 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 ) ) )
46 31 simp3d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( D ( -g ` R ) B ) e. S )
47 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 )
48 5 12 35 46 47 syl22anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( C .x. ( D ( -g ` R ) B ) ) e. S )
49 45 48 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( C .x. B ) ) e. S )
50 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
51 1 4 7 50 opprmul 
 |-  ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) = ( ( A ( -g ` R ) C ) .x. B )
52 1 4 23 5 27 35 32 rngsubdir 
 |-  ( ( ( 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 ) ) )
53 51 52 syl5eq 
 |-  ( ( ( 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 ) ) )
54 7 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
55 54 ad2antrr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( oppR ` R ) e. Ring )
56 10 simprbi 
 |-  ( S e. I -> S e. ( LIdeal ` ( oppR ` R ) ) )
57 56 ad2antlr 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> S e. ( LIdeal ` ( oppR ` R ) ) )
58 26 simp3d 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A ( -g ` R ) C ) e. S )
59 7 1 opprbas 
 |-  X = ( Base ` ( oppR ` R ) )
60 8 59 50 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 )
61 55 57 32 58 60 syl22anc 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( B ( .r ` ( oppR ` R ) ) ( A ( -g ` R ) C ) ) e. S )
62 53 61 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( A .x. B ) ( -g ` R ) ( C .x. B ) ) e. S )
63 6 23 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 )
64 5 12 49 62 63 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 )
65 44 64 eqeltrrd 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( ( C .x. D ) ( -g ` R ) ( A .x. B ) ) e. S )
66 1 23 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 ) ) )
67 20 22 66 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 ) ) )
68 34 38 65 67 mpbir3and 
 |-  ( ( ( R e. Ring /\ S e. I ) /\ ( A E C /\ B E D ) ) -> ( A .x. B ) E ( C .x. D ) )
69 68 ex 
 |-  ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )