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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	2idlcpbl	$⊢ (R \in Ring \land S \in I) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} 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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simpll	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to R \in 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	2idlelb	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
10	9	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
11	10	ad2antlr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in LIdeal (R)$
12	6	lidlsubg	$⊢ (R \in Ring \land S \in LIdeal (R)) \to S \in SubGrp (R)$
13	5 11 12	syl2anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in SubGrp (R)$
14	1 2	eqger	$⊢ S \in SubGrp (R) \to E Er X$
15	13 14	syl	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to E Er X$
16		simprl	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A E C$
17	15 16	ersym	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C E A$
18		ringabl	$⊢ R \in Ring \to R \in Abel$
19	18	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to R \in Abel$
20	1 3	2idlss	$⊢ S \in I \to S \subseteq X$
21	20	ad2antlr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \subseteq X$
22		eqid	$⊢ -_{R} = -_{R}$
23	1 22 2	eqgabl	$⊢ (R \in Abel \land S \subseteq X) \to (C E A \leftrightarrow (C \in X \land A \in X \land A -_{R} C \in S))$
24	19 21 23	syl2anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (C E A \leftrightarrow (C \in X \land A \in X \land A -_{R} C \in S))$
25	17 24	mpbid	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (C \in X \land A \in X \land A -_{R} C \in S)$
26	25	simp2d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A \in X$
27		simprr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B E D$
28	1 22 2	eqgabl	$⊢ (R \in Abel \land S \subseteq X) \to (B E D \leftrightarrow (B \in X \land D \in X \land D -_{R} B \in S))$
29	19 21 28	syl2anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (B E D \leftrightarrow (B \in X \land D \in X \land D -_{R} B \in S))$
30	27 29	mpbid	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (B \in X \land D \in X \land D -_{R} B \in S)$
31	30	simp1d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B \in X$
32	1 4 5 26 31	ringcld	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A \underset{˙}{\cdot} B \in X$
33	25	simp1d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \in X$
34	30	simp2d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to D \in X$
35	1 4 5 33 34	ringcld	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} D \in X$
36		ringgrp	$⊢ R \in Ring \to R \in Grp$
37	36	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to R \in Grp$
38	1 4 5 33 31	ringcld	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} B \in X$
39	1 22	grpnnncan2	$⊢ (R \in Grp \land (C \underset{˙}{\cdot} D \in X \land A \underset{˙}{\cdot} B \in X \land C \underset{˙}{\cdot} B \in X)) \to ((C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B)) -_{R} ((A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)) = (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B)$
40	37 35 32 38 39	syl13anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to ((C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B)) -_{R} ((A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)) = (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B)$
41	1 4 22 5 33 34 31	ringsubdi	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} (D -_{R} B) = (C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B)$
42	30	simp3d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to D -_{R} B \in S$
43	6 1 4	lidlmcl	$⊢ ((R \in Ring \land S \in LIdeal (R)) \land (C \in X \land D -_{R} B \in S)) \to C \underset{˙}{\cdot} (D -_{R} B) \in S$
44	5 11 33 42 43	syl22anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} (D -_{R} B) \in S$
45	41 44	eqeltrrd	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B) \in S$
46		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
47	1 4 7 46	opprmul	$⊢ B \cdot_{{opp}_{r} (R)} (A -_{R} C) = (A -_{R} C) \underset{˙}{\cdot} B$
48	1 4 22 5 26 33 31	ringsubdir	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (A -_{R} C) \underset{˙}{\cdot} B = (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)$
49	47 48	eqtrid	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B \cdot_{{opp}_{r} (R)} (A -_{R} C) = (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)$
50	7	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
51	50	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to {opp}_{r} (R) \in Ring$
52	9	simprbi	$⊢ S \in I \to S \in LIdeal ({opp}_{r} (R))$
53	52	ad2antlr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in LIdeal ({opp}_{r} (R))$
54	25	simp3d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A -_{R} C \in S$
55	7 1	opprbas	$⊢ X = {Base}_{{opp}_{r} (R)}$
56	8 55 46	lidlmcl	$⊢ (({opp}_{r} (R) \in Ring \land S \in LIdeal ({opp}_{r} (R))) \land (B \in X \land A -_{R} C \in S)) \to B \cdot_{{opp}_{r} (R)} (A -_{R} C) \in S$
57	51 53 31 54 56	syl22anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B \cdot_{{opp}_{r} (R)} (A -_{R} C) \in S$
58	49 57	eqeltrrd	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B) \in S$
59	6 22	lidlsubcl	$⊢ ((R \in Ring \land S \in LIdeal (R)) \land ((C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B) \in S \land (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B) \in S)) \to ((C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B)) -_{R} ((A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)) \in S$
60	5 11 45 58 59	syl22anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to ((C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B)) -_{R} ((A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)) \in S$
61	40 60	eqeltrrd	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B) \in S$
62	1 22 2	eqgabl	$⊢ (R \in Abel \land S \subseteq X) \to ((A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D) \leftrightarrow (A \underset{˙}{\cdot} B \in X \land C \underset{˙}{\cdot} D \in X \land (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B) \in S))$
63	19 21 62	syl2anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to ((A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D) \leftrightarrow (A \underset{˙}{\cdot} B \in X \land C \underset{˙}{\cdot} D \in X \land (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B) \in S))$
64	32 35 61 63	mpbir3and	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D)$
65	64	ex	$⊢ (R \in Ring \land S \in I) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$

Metamath Proof Explorer

Theorem 2idlcpbl

Proof