qusrng - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > qusrng		Structured version Visualization version GIF version

Theorem qusrng 20104

Description: The quotient structure of a non-unital ring is a non-unital ring (qusring2 20252 analog). (Contributed by AV, 23-Feb-2025.)

**Hypotheses**
Ref	Expression
qusrng.u	⊢ (𝜑 → 𝑈 = (𝑅 /_s ∼ ))
qusrng.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
qusrng.p	⊢ + = (+_g‘𝑅)
qusrng.t	⊢ · = (._r‘𝑅)
qusrng.r	⊢ (𝜑 → ∼ Er 𝑉)
qusrng.e1	⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))
qusrng.e2	⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))
qusrng.x	⊢ (𝜑 → 𝑅 ∈ Rng)

**Assertion**
Ref	Expression
qusrng	⊢ (𝜑 → 𝑈 ∈ Rng)

Distinct variable groups: 𝑅,𝑎,𝑏,𝑝,𝑞 𝑈,𝑎,𝑏,𝑝,𝑞 𝑉,𝑎,𝑏,𝑝,𝑞 ∼ ,𝑎,𝑏,𝑝,𝑞 + ,𝑝,𝑞 · ,𝑝,𝑞 𝜑,𝑎,𝑏,𝑝,𝑞 Allowed substitution hints: + (𝑎,𝑏) · (𝑎,𝑏)

Proof of Theorem qusrng Dummy variables 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		qusrng.u	. . 3 ⊢ (𝜑 → 𝑈 = (𝑅 /_s ∼ ))
2		qusrng.v	. . 3 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		eqid 2727	. . 3 ⊢ (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ) = (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )
4		qusrng.r	. . . 4 ⊢ (𝜑 → ∼ Er 𝑉)
5		fvex 6904	. . . . 5 ⊢ (Base‘𝑅) ∈ V
6	2, 5	eqeltrdi 2836	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
7		erex 8740	. . . 4 ⊢ ( ∼ Er 𝑉 → (𝑉 ∈ V → ∼ ∈ V))
8	4, 6, 7	sylc 65	. . 3 ⊢ (𝜑 → ∼ ∈ V)
9		qusrng.x	. . 3 ⊢ (𝜑 → 𝑅 ∈ Rng)
10	1, 2, 3, 8, 9	qusval 17509	. 2 ⊢ (𝜑 → 𝑈 = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ) “_s 𝑅))
11		qusrng.p	. 2 ⊢ + = (+_g‘𝑅)
12		qusrng.t	. 2 ⊢ · = (._r‘𝑅)
13	1, 2, 3, 8, 9	quslem 17510	. 2 ⊢ (𝜑 → (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ):𝑉–onto→(𝑉 / ∼ ))
14	9	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑅 ∈ Rng)
15		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
16	2	eleq2d 2814	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝑉 ↔ 𝑥 ∈ (Base‘𝑅)))
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∈ 𝑉 ↔ 𝑥 ∈ (Base‘𝑅)))
18	15, 17	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ (Base‘𝑅))
19		simprr 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉)
20	2	eleq2d 2814	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑉 ↔ 𝑦 ∈ (Base‘𝑅)))
21	20	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑦 ∈ 𝑉 ↔ 𝑦 ∈ (Base‘𝑅)))
22	19, 21	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ (Base‘𝑅))
23		eqid 2727	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
24	23, 11	rngacl 20086	. . . . 5 ⊢ ((𝑅 ∈ Rng ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥 + 𝑦) ∈ (Base‘𝑅))
25	14, 18, 22, 24	syl3anc 1369	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ (Base‘𝑅))
26	2	eleq2d 2814	. . . . 5 ⊢ (𝜑 → ((𝑥 + 𝑦) ∈ 𝑉 ↔ (𝑥 + 𝑦) ∈ (Base‘𝑅)))
27	26	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑥 + 𝑦) ∈ 𝑉 ↔ (𝑥 + 𝑦) ∈ (Base‘𝑅)))
28	25, 27	mpbird 257	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
29		qusrng.e1	. . 3 ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))
30	4, 6, 3, 28, 29	ercpbl 17516	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑎) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑝) ∧ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑏) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑞)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑎 + 𝑏)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑝 + 𝑞))))
31	23, 12	rngcl 20088	. . . . 5 ⊢ ((𝑅 ∈ Rng ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥 · 𝑦) ∈ (Base‘𝑅))
32	14, 18, 22, 31	syl3anc 1369	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 · 𝑦) ∈ (Base‘𝑅))
33	2	eleq2d 2814	. . . . 5 ⊢ (𝜑 → ((𝑥 · 𝑦) ∈ 𝑉 ↔ (𝑥 · 𝑦) ∈ (Base‘𝑅)))
34	33	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑥 · 𝑦) ∈ 𝑉 ↔ (𝑥 · 𝑦) ∈ (Base‘𝑅)))
35	32, 34	mpbird 257	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 · 𝑦) ∈ 𝑉)
36		qusrng.e2	. . 3 ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞)))
37	4, 6, 3, 35, 36	ercpbl 17516	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑎) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑝) ∧ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑏) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑞)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑎 · 𝑏)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑝 · 𝑞))))
38	10, 2, 11, 12, 13, 30, 37, 9	imasrng 20101	1 ⊢ (𝜑 → 𝑈 ∈ Rng)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1534 ∈ wcel 2099 Vcvv 3469 class class class wbr 5142 ↦ cmpt 5225 ‘cfv 6542 (class class class)co 7414 Er wer 8713 [cec 8714 / cqs 8715 Basecbs 17165 +_gcplusg 17218 ._rcmulr 17219 /_s cqus 17472 Rngcrng 20076

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7732 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7863 df-1st 7985 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-er 8716 df-ec 8718 df-qs 8722 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-sup 9451 df-inf 9452 df-pnf 11266 df-mnf 11267 df-xr 11268 df-ltxr 11269 df-le 11270 df-sub 11462 df-neg 11463 df-nn 12229 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12489 df-z 12575 df-dec 12694 df-uz 12839 df-fz 13503 df-struct 17101 df-sets 17118 df-slot 17136 df-ndx 17148 df-base 17166 df-plusg 17231 df-mulr 17232 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-0g 17408 df-imas 17475 df-qus 17476 df-mgm 18585 df-sgrp 18664 df-mnd 18680 df-grp 18878 df-minusg 18879 df-cmn 19721 df-abl 19722 df-mgp 20059 df-rng 20077

This theorem is referenced by: qus2idrng 21149

W3C validator