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