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)

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 2idlval ⊢ 𝐼 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
10 9 elin2 ⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
11 10 simplbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
12 11 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
13 6 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
14 5 12 13 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
15 1 2 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝐸 Er 𝑋 )
16 14 15 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐸 Er 𝑋 )
17 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 𝐸 𝐶 )
18 16 17 ersym ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 𝐸 𝐴 )
19 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
20 19 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Abel )
21 1 6 lidlss ⊢ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) → 𝑆 ⊆ 𝑋 )
22 12 21 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ⊆ 𝑋 )
23 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
24 1 23 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
25 20 22 24 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
26 18 25 mpbid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) )
27 26 simp2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 ∈ 𝑋 )
28 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 𝐸 𝐷 )
29 1 23 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
30 20 22 29 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
31 28 30 mpbid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) )
32 31 simp1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 ∈ 𝑋 )
33 1 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
34 5 27 32 33 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
35 26 simp1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 ∈ 𝑋 )
36 31 simp2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐷 ∈ 𝑋 )
37 1 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → ( 𝐶 · 𝐷 ) ∈ 𝑋 )
38 5 35 36 37 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐷 ) ∈ 𝑋 )
39 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
40 39 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Grp )
41 1 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐶 · 𝐵 ) ∈ 𝑋 )
42 5 35 32 41 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐵 ) ∈ 𝑋 )
43 1 23 grpnnncan2 ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐵 ) ∈ 𝑋 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
44 40 38 34 42 43 syl13anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
45 1 4 23 5 35 36 32 ringsubdi ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
46 31 simp3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 )
47 6 1 4 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐶 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
48 5 12 35 46 47 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
49 45 48 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
50 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
51 1 4 7 50 opprmul ⊢ ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 )
52 1 4 23 5 27 35 32 rngsubdir ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
53 51 52 eqtrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
54 7 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
55 54 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( oppr ‘ 𝑅 ) ∈ Ring )
56 10 simprbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
57 56 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
58 26 simp3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 )
59 7 1 opprbas ⊢ 𝑋 = ( Base ‘ ( oppr ‘ 𝑅 ) )
60 8 59 50 lidlmcl ⊢ ( ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
61 55 57 32 58 60 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
62 53 61 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
63 6 23 lidlsubcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ∧ ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
64 5 12 49 62 63 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
65 44 64 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 )
66 1 23 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
67 20 22 66 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
68 34 38 65 67 mpbir3and ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) )
69 68 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )