2idlcpblrng

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025) TODO: Replace 2idlcpbl if moved to main.

	Ref	Expression
Hypotheses	2idlcpblrng.x	$⊢ X = {Base}_{R}$
	2idlcpblrng.r	$⊢ E = R ~_{QG} S$
	2idlcpblrng.i	$⊢ I = 2Ideal (R)$
	2idlcpblrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	2idlcpblrng	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$

Proof

Step	Hyp	Ref	Expression
1		2idlcpblrng.x	$⊢ X = {Base}_{R}$
2		2idlcpblrng.r	$⊢ E = R ~_{QG} S$
3		2idlcpblrng.i	$⊢ I = 2Ideal (R)$
4		2idlcpblrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simpl1	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to R \in Rng$
6		simpl3	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to S \in SubGrp (R)$
7	1 2	eqger	$⊢ S \in SubGrp (R) \to E Er X$
8	6 7	syl	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to E Er X$
9		simprl	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to A E C$
10	8 9	ersym	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to C E A$
11		rngabl	$⊢ R \in Rng \to R \in Abel$
12	11	3ad2ant1	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to R \in Abel$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
15		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
16	13 14 15 3	2idlelb	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
17	16	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
18	17	3ad2ant2	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to S \in LIdeal (R)$
19	18	adantr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to S \in LIdeal (R)$
20	1 13	lidlss	$⊢ S \in LIdeal (R) \to S \subseteq X$
21	19 20	syl	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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	12 21 23	syl2an2r	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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	10 24	mpbid	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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 Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to A \in X$
27		simprr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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	12 21 28	syl2an2r	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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 Rng \land S \in I \land S \in SubGrp (R)) \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 Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to B \in X$
32	1 4	rngcl	$⊢ (R \in Rng \land A \in X \land B \in X) \to A \underset{˙}{\cdot} B \in X$
33	5 26 31 32	syl3anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to A \underset{˙}{\cdot} B \in X$
34	25	simp1d	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to C \in X$
35	30	simp2d	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to D \in X$
36	1 4	rngcl	$⊢ (R \in Rng \land C \in X \land D \in X) \to C \underset{˙}{\cdot} D \in X$
37	5 34 35 36	syl3anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} D \in X$
38		rnggrp	$⊢ R \in Rng \to R \in Grp$
39	38	3ad2ant1	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to R \in Grp$
40	39	adantr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to R \in Grp$
41	1 4	rngcl	$⊢ (R \in Rng \land C \in X \land B \in X) \to C \underset{˙}{\cdot} B \in X$
42	5 34 31 41	syl3anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} B \in X$
43	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)$
44	40 37 33 42 43	syl13anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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 22 5 34 35 31	rngsubdi	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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		eqid	$⊢ 0_{R} = 0_{R}$
47	46	subg0cl	$⊢ S \in SubGrp (R) \to 0_{R} \in S$
48	47	3ad2ant3	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to 0_{R} \in S$
49	48	adantr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to 0_{R} \in S$
50	30	simp3d	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to D -_{R} B \in S$
51	46 1 4 13	rnglidlmcl	$⊢ ((R \in Rng \land S \in LIdeal (R) \land 0_{R} \in S) \land (C \in X \land D -_{R} B \in S)) \to C \underset{˙}{\cdot} (D -_{R} B) \in S$
52	5 19 49 34 50 51	syl32anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to C \underset{˙}{\cdot} (D -_{R} B) \in S$
53	45 52	eqeltrrd	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to (C \underset{˙}{\cdot} D) -_{R} (C \underset{˙}{\cdot} B) \in S$
54		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
55	1 4 14 54	opprmul	$⊢ B \cdot_{{opp}_{r} (R)} (A -_{R} C) = (A -_{R} C) \underset{˙}{\cdot} B$
56	1 4 22 5 26 34 31	rngsubdir	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to (A -_{R} C) \underset{˙}{\cdot} B = (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B)$
57	55 56	eqtrid	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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)$
58	14	opprrng	$⊢ R \in Rng \to {opp}_{r} (R) \in Rng$
59	58	3ad2ant1	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to {opp}_{r} (R) \in Rng$
60	59	adantr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to {opp}_{r} (R) \in Rng$
61	16	simprbi	$⊢ S \in I \to S \in LIdeal ({opp}_{r} (R))$
62	61	3ad2ant2	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to S \in LIdeal ({opp}_{r} (R))$
63	62	adantr	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to S \in LIdeal ({opp}_{r} (R))$
64	25	simp3d	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to A -_{R} C \in S$
65	14 46	oppr0	$⊢ 0_{R} = 0_{{opp}_{r} (R)}$
66	14 1	opprbas	$⊢ X = {Base}_{{opp}_{r} (R)}$
67	65 66 54 15	rnglidlmcl	$⊢ (({opp}_{r} (R) \in Rng \land S \in LIdeal ({opp}_{r} (R)) \land 0_{R} \in S) \land (B \in X \land A -_{R} C \in S)) \to B \cdot_{{opp}_{r} (R)} (A -_{R} C) \in S$
68	60 63 49 31 64 67	syl32anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to B \cdot_{{opp}_{r} (R)} (A -_{R} C) \in S$
69	57 68	eqeltrrd	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to (A \underset{˙}{\cdot} B) -_{R} (C \underset{˙}{\cdot} B) \in S$
70	22	subgsubcl	$⊢ (S \in SubGrp (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$
71	6 53 69 70	syl3anc	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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$
72	44 71	eqeltrrd	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to (C \underset{˙}{\cdot} D) -_{R} (A \underset{˙}{\cdot} B) \in S$
73	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))$
74	12 21 73	syl2an2r	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \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))$
75	33 37 72 74	mpbir3and	$⊢ ((R \in Rng \land S \in I \land S \in SubGrp (R)) \land (A E C \land B E D)) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D)$
76	75	ex	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$

Metamath Proof Explorer

Theorem 2idlcpblrng

Proof