2idlcpbl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 2idlcpbl		GIF version

Theorem 2idlcpbl 14971

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)

**Hypotheses**
Ref	Expression
2idlcpblrng.x	⊢ 𝑋 = (Base‘𝑅)
2idlcpblrng.r	⊢ 𝐸 = (𝑅 ~_QG 𝑆)
2idlcpblrng.i	⊢ 𝐼 = (2Ideal‘𝑅)
2idlcpblrng.t	⊢ · = (._r‘𝑅)

**Assertion**
Ref	Expression
2idlcpbl	⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))

**Proof of Theorem 2idlcpbl**
Step	Hyp	Ref	Expression
1		ringrng 14449	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng)
2	1	adantr 276	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑅 ∈ Rng)
3		simpr 110	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑆 ∈ 𝐼)
4		eqid 2238	. . . . 5 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
5		eqid 2238	. . . . 5 ⊢ (opp_r‘𝑅) = (opp_r‘𝑅)
6		eqid 2238	. . . . 5 ⊢ (LIdeal‘(opp_r‘𝑅)) = (LIdeal‘(opp_r‘𝑅))
7		2idlcpblrng.i	. . . . 5 ⊢ 𝐼 = (2Ideal‘𝑅)
8	4, 5, 6, 7	2idlelb 14952	. . . 4 ⊢ (𝑆 ∈ 𝐼 ↔ (𝑆 ∈ (LIdeal‘𝑅) ∧ 𝑆 ∈ (LIdeal‘(opp_r‘𝑅))))
9	8	simplbi 274	. . 3 ⊢ (𝑆 ∈ 𝐼 → 𝑆 ∈ (LIdeal‘𝑅))
10	4	lidlsubg 14933	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ (LIdeal‘𝑅)) → 𝑆 ∈ (SubGrp‘𝑅))
11	9, 10	sylan2 286	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → 𝑆 ∈ (SubGrp‘𝑅))
12		2idlcpblrng.x	. . 3 ⊢ 𝑋 = (Base‘𝑅)
13		2idlcpblrng.r	. . 3 ⊢ 𝐸 = (𝑅 ~_QG 𝑆)
14		2idlcpblrng.t	. . 3 ⊢ · = (._r‘𝑅)
15	12, 13, 7, 14	2idlcpblrng 14970	. 2 ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ (SubGrp‘𝑅)) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))
16	2, 3, 11, 15	syl3anc 1278	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼) → ((𝐴𝐸𝐶 ∧ 𝐵𝐸𝐷) → (𝐴 · 𝐵)𝐸(𝐶 · 𝐷)))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 = wceq 1402 ∈ wcel 2209 class class class wbr 4131 ‘cfv 5380 (class class class)co 6088 Basecbs 13411 ._rcmulr 13492 SubGrpcsubg 14030 ~_QG cqg 14032 Rngcrng 14339 Ringcrg 14408 opp_rcoppr 14482 LIdealclidl 14914 2Idealc2idl 14946

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-cnex 8277 ax-resscn 8278 ax-1cn 8279 ax-1re 8280 ax-icn 8281 ax-addcl 8282 ax-addrcl 8283 ax-mulcl 8284 ax-addcom 8286 ax-addass 8288 ax-i2m1 8291 ax-0lt1 8292 ax-0id 8294 ax-rnegex 8295 ax-pre-ltirr 8298 ax-pre-lttrn 8300 ax-pre-ltadd 8302

This proof depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-id 4440 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-tpos 6520 df-er 6811 df-pnf 8369 df-mnf 8370 df-ltxr 8372 df-inn 9315 df-2 9373 df-3 9374 df-4 9375 df-5 9376 df-6 9377 df-7 9378 df-8 9379 df-ndx 13414 df-slot 13415 df-base 13417 df-sets 13418 df-iress 13419 df-plusg 13504 df-mulr 13505 df-sca 13507 df-vsca 13508 df-ip 13509 df-0g 13672 df-mgm 13736 df-sgrp 13777 df-mnd 13790 df-grp 13868 df-minusg 13869 df-sbg 13870 df-subg 14033 df-eqg 14035 df-cmn 14180 df-abl 14181 df-mgp 14326 df-rng 14340 df-ur 14371 df-ring 14410 df-oppr 14483 df-subrg 14637 df-lmod 14735 df-lssm 14800 df-sra 14882 df-rgmod 14883 df-lidl 14916 df-2idl 14947

This theorem is used by: qus1 14973 qusrhm 14975 qusmul2 14976

W3C validator