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) (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 ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )