Theorem 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	⊢ 𝑋 = ( Base ‘ 𝑅 )
	2idlcpbl.r	⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
	2idlcpbl.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
	2idlcpbl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	2idlcpbl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2idlcpbl.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		2idlcpbl.r	⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
3		2idlcpbl.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
4		2idlcpbl.t	⊢ · = ( .r ‘ 𝑅 )
5		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Ring )
6		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
8		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
9	6 7 8 3	2idlelb	⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
10	9	simplbi	⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
11	10	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
12	6	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
13	5 11 12	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
14	1 2	eqger	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝐸 Er 𝑋 )
15	13 14	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐸 Er 𝑋 )
16		simprl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 𝐸 𝐶 )
17	15 16	ersym	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 𝐸 𝐴 )
18		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
19	18	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Abel )
20	1 3	2idlss	⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ⊆ 𝑋 )
21	20	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ⊆ 𝑋 )
22		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
23	1 22 2	eqgabl	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
24	19 21 23	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
25	17 24	mpbid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) )
26	25	simp2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 ∈ 𝑋 )
27		simprr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 𝐸 𝐷 )
28	1 22 2	eqgabl	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
29	19 21 28	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
30	27 29	mpbid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) )
31	30	simp1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 ∈ 𝑋 )
32	1 4 5 26 31	ringcld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
33	25	simp1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 ∈ 𝑋 )
34	30	simp2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐷 ∈ 𝑋 )
35	1 4 5 33 34	ringcld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐷 ) ∈ 𝑋 )
36		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
37	36	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Grp )
38	1 4 5 33 31	ringcld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐵 ) ∈ 𝑋 )
39	1 22	grpnnncan2	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐵 ) ∈ 𝑋 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
40	37 35 32 38 39	syl13anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
41	1 4 22 5 33 34 31	ringsubdi	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
42	30	simp3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 )
43	6 1 4	lidlmcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐶 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
44	5 11 33 42 43	syl22anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
45	41 44	eqeltrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
46		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
47	1 4 7 46	opprmul	⊢ ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 )
48	1 4 22 5 26 33 31	ringsubdir	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
49	47 48	eqtrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
50	7	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
51	50	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( oppr ‘ 𝑅 ) ∈ Ring )
52	9	simprbi	⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
53	52	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
54	25	simp3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 )
55	7 1	opprbas	⊢ 𝑋 = ( Base ‘ ( oppr ‘ 𝑅 ) )
56	8 55 46	lidlmcl	⊢ ( ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
57	51 53 31 54 56	syl22anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
58	49 57	eqeltrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
59	6 22	lidlsubcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ∧ ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
60	5 11 45 58 59	syl22anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
61	40 60	eqeltrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 )
62	1 22 2	eqgabl	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
63	19 21 62	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
64	32 35 61 63	mpbir3and	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) )
65	64	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )