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	$⊢ \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	2idlval	$⊢ I = LIdeal (R) \cap LIdeal ({opp}_{r} (R))$
10	9	elin2	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
11	10	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
12	11	ad2antlr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in LIdeal (R)$
13	6	lidlsubg	$⊢ (R \in Ring \land S \in LIdeal (R)) \to S \in SubGrp (R)$
14	5 12 13	syl2anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in SubGrp (R)$
15	1 2	eqger	$⊢ S \in SubGrp (R) \to E Er X$
16	14 15	syl	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to E Er X$
17		simprl	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A E C$
18	16 17	ersym	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C E A$
19		ringabl	$⊢ R \in Ring \to R \in Abel$
20	19	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to R \in Abel$
21	1 6	lidlss	$⊢ S \in LIdeal (R) \to S \subseteq X$
22	12 21	syl	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \subseteq X$
23		eqid	$⊢ -_{R} = -_{R}$
24	1 23 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))$
25	20 22 24	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))$
26	18 25	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)$
27	26	simp2d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A \in X$
28		simprr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B E D$
29	1 23 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))$
30	20 22 29	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))$
31	28 30	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)$
32	31	simp1d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to B \in X$
33	1 4	ringcl	$⊢ (R \in Ring \land A \in X \land B \in X) \to A \underset{˙}{\cdot} B \in X$
34	5 27 32 33	syl3anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A \underset{˙}{\cdot} B \in X$
35	26	simp1d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \in X$
36	31	simp2d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to D \in X$
37	1 4	ringcl	$⊢ (R \in Ring \land C \in X \land D \in X) \to C \underset{˙}{\cdot} D \in X$
38	5 35 36 37	syl3anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} D \in X$
39		ringgrp	$⊢ R \in Ring \to R \in Grp$
40	39	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to R \in Grp$
41	1 4	ringcl	$⊢ (R \in Ring \land C \in X \land B \in X) \to C \underset{˙}{\cdot} B \in X$
42	5 35 32 41	syl3anc	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} B \in X$
43	1 23	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)$
44	40 38 34 42 43	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)$
45	1 4 23 5 35 36 32	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)$
46	31	simp3d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to D -_{R} B \in S$
47	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$
48	5 12 35 46 47	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$
49	45 48	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$
50		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
51	1 4 7 50	opprmul	$⊢ B \cdot_{{opp}_{r} (R)} (A -_{R} C) = (A -_{R} C) \underset{˙}{\cdot} B$
52	1 4 23 5 27 35 32	rngsubdir	$⊢ ((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)$
53	51 52	syl5eq	$⊢ ((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)$
54	7	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
55	54	ad2antrr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to {opp}_{r} (R) \in Ring$
56	10	simprbi	$⊢ S \in I \to S \in LIdeal ({opp}_{r} (R))$
57	56	ad2antlr	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to S \in LIdeal ({opp}_{r} (R))$
58	26	simp3d	$⊢ ((R \in Ring \land S \in I) \land (A E C \land B E D)) \to A -_{R} C \in S$
59	7 1	opprbas	$⊢ X = {Base}_{{opp}_{r} (R)}$
60	8 59 50	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$
61	55 57 32 58 60	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$
62	53 61	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$
63	6 23	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$
64	5 12 49 62 63	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$
65	44 64	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$
66	1 23 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))$
67	20 22 66	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))$
68	34 38 65 67	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)$
69	68	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