![]() |
Metamath
Proof Explorer Theorem List (p. 446 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rngabl 44501 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) | ||
Theorem | rngmgp 44502 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp) | ||
Theorem | ringrng 44503 | A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng) | ||
Theorem | ringssrng 44504 | The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.) |
⊢ Ring ⊆ Rng | ||
Theorem | isringrng 44505* | The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Rng ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑦 ∧ (𝑦 · 𝑥) = 𝑦))) | ||
Theorem | rngdir 44506 | Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
Theorem | rngcl 44507 | Closure of the multiplication operation of a nonunital ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | rnglz 44508 | The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
Syntax | crngh 44509 | non-unital ring homomorphisms. |
class RngHomo | ||
Syntax | crngs 44510 | non-unital ring isomorphisms. |
class RngIsom | ||
Definition | df-rnghomo 44511* | Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
⊢ RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}) | ||
Definition | df-rngisom 44512* | Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
⊢ RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHomo 𝑟)}) | ||
Theorem | rnghmrcl 44513 | Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng)) | ||
Theorem | rnghmfn 44514 | The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
⊢ RngHomo Fn (Rng × Rng) | ||
Theorem | rnghmval 44515* | The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∗ = (.r‘𝑆) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑆) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ✚ (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) ∗ (𝑓‘𝑦)))}) | ||
Theorem | isrnghm 44516* | A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∗ = (.r‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))))) | ||
Theorem | isrnghmmul 44517 | A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MgmHom 𝑁)))) | ||
Theorem | rnghmmgmhm 44518 | A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁)) | ||
Theorem | rnghmval2 44519 | The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.) |
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MgmHom (mulGrp‘𝑆)))) | ||
Theorem | isrngisom 44520 | An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ ◡𝐹 ∈ (𝑆 RngHomo 𝑅)))) | ||
Theorem | rngimrcl 44521 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | rnghmghm 44522 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | rnghmf 44523 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹:𝐵⟶𝐶) | ||
Theorem | rnghmmul 44524 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
Theorem | isrnghm2d 44525* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | isrnghmd 44526* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmf1o 44527 | A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RngHomo 𝑅))) | ||
Theorem | isrngim 44528 | An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))) | ||
Theorem | rngimf1o 44529 | An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | rngimrnghm 44530 | An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmco 44531 | The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
⊢ ((𝐹 ∈ (𝑇 RngHomo 𝑈) ∧ 𝐺 ∈ (𝑆 RngHomo 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHomo 𝑈)) | ||
Theorem | idrnghm 44532 | The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHomo 𝑅)) | ||
Theorem | c0mgm 44533* | The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MgmHom 𝑇)) | ||
Theorem | c0mhm 44534* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | c0ghm 44535* | The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | c0rhm 44536* | The constant mapping to zero is a ring homomorphism from any ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Ring ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RingHom 𝑇)) | ||
Theorem | c0rnghm 44537* | The constant mapping to zero is a nonunital ring homomorphism from any nonunital ring to the zero ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑆 RngHomo 𝑇)) | ||
Theorem | c0snmgmhm 44538* | The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (♯‘𝐵) = 1) → 𝐻 ∈ (𝑇 MgmHom 𝑆)) | ||
Theorem | c0snmhm 44539* | The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) & ⊢ 𝑍 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 MndHom 𝑆)) | ||
Theorem | c0snghm 44540* | The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) & ⊢ 𝑍 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {𝑍}) → 𝐻 ∈ (𝑇 GrpHom 𝑆)) | ||
Theorem | zrrnghm 44541* | The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing)) → 𝐻 ∈ (𝑇 RngHomo 𝑆)) | ||
Theorem | rhmfn 44542 | The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
⊢ RingHom Fn (Ring × Ring) | ||
Theorem | rhmval 44543 | The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.) |
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))) | ||
Theorem | rhmisrnghm 44544 | Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | lidldomn1 44545* | If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 )) | ||
Theorem | lidlssbas 44546 | The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) ⊆ (Base‘𝑅)) | ||
Theorem | lidlbas 44547 | A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈) | ||
Theorem | lidlabl 44548 | A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) | ||
Theorem | lidlmmgm 44549 | The multiplicative group of a (left) ideal of a ring is a magma. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Mgm) | ||
Theorem | lidlmsgrp 44550 | The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ Smgrp) | ||
Theorem | lidlrng 44551 | A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) | ||
Theorem | zlidlring 44552 | The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring) | ||
Theorem | uzlidlring 44553 | Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿) → (𝐼 ∈ Ring ↔ (𝑈 = { 0 } ∨ 𝑈 = 𝐵))) | ||
Theorem | lidldomnnring 44554 | A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵)) → 𝐼 ∉ Ring) | ||
Theorem | 0even 44555* | 0 is an even integer. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 0 ∈ 𝐸 | ||
Theorem | 1neven 44556* | 1 is not an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 1 ∉ 𝐸 | ||
Theorem | 2even 44557* | 2 is an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 2 ∈ 𝐸 | ||
Theorem | 2zlidl 44558* | The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) ⇒ ⊢ 𝐸 ∈ 𝑈 | ||
Theorem | 2zrng 44559* | The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm 44435. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) & ⊢ 𝑅 = (ℤring ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngbas 44560* | The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝐸 = (Base‘𝑅) | ||
Theorem | 2zrngadd 44561* | The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ + = (+g‘𝑅) | ||
Theorem | 2zrng0 44562* | The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | 2zrngamgm 44563* | R is an (additive) magma. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mgm | ||
Theorem | 2zrngasgrp 44564* | R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Smgrp | ||
Theorem | 2zrngamnd 44565* | R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | 2zrngacmnd 44566* | R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | 2zrngagrp 44567* | R is an (additive) group. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Grp | ||
Theorem | 2zrngaabl 44568* | R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Abel | ||
Theorem | 2zrngmul 44569* | The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ · = (.r‘𝑅) | ||
Theorem | 2zrngmmgm 44570* | R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Mgm | ||
Theorem | 2zrngmsgrp 44571* | R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Smgrp | ||
Theorem | 2zrngALT 44572* | The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 44559, based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl 44568) and a multiplicative semigroup (see 2zrngmsgrp 44571). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngnmlid 44573* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnmrid 44574* | R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 | ||
Theorem | 2zrngnmlid2 44575* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnring 44576* | R is not a unital ring. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∉ Ring | ||
Theorem | cznrnglem 44577 | Lemma for cznrng 44579: The base set of the ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the ℤ/nℤ structure. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) ⇒ ⊢ 𝐵 = (Base‘𝑋) | ||
Theorem | cznabel 44578 | The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) | ||
Theorem | cznrng 44579* | The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng) | ||
Theorem | cznnring 44580* | The ring constructed from a ℤ/nℤ structure with 1 < 𝑛 by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐶 ∈ 𝐵) → 𝑋 ∉ Ring) | ||
The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHomo between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to non-unital rings and the morphisms to the non-unital ring homomorphisms, while the composition of morphisms is preserved, see df-rngc 44583. Alternately, the category of non-unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see df-rngcALTV 44584 or dfrngc2 44596. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are a subset of the non-unital rings (relativized to a subset or "universe" 𝑢) (𝑢 ∩ Rng), see rngcbas 44589, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo ↾ (𝐵 × 𝐵)), see rngchomfval 44590, whereas the composition is the ordinary composition of functions, see rngccofval 44594 and rngcco 44595. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset (⊆cat) of the mappings between base sets of extensible structures, see rnghmsscmap 44598, it can be shown that the non-unital ring homomorphisms between non-unital rings are a subcategory (Subcat) of the category of extensible structures, see rnghmsubcsetc 44601. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 44602 with the identity function as identity arrow, see rngcid 44603. | ||
Syntax | crngc 44581 | Extend class notation to include the category Rng. |
class RngCat | ||
Syntax | crngcALTV 44582 | Extend class notation to include the category Rng. (New usage is discouraged.) |
class RngCatALTV | ||
Definition | df-rngc 44583 | Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ RngCat = (𝑢 ∈ V ↦ ((ExtStrCat‘𝑢) ↾cat ( RngHomo ↾ ((𝑢 ∩ Rng) × (𝑢 ∩ Rng))))) | ||
Definition | df-rngcALTV 44584* | Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ RngCatALTV = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHomo 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) | ||
Theorem | rngcvalALTV 44585* | Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | rngcval 44586 | Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐶 = ((ExtStrCat‘𝑈) ↾cat 𝐻)) | ||
Theorem | rnghmresfn 44587 | The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.) |
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝐵 × 𝐵)) | ||
Theorem | rnghmresel 44588 | An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020.) |
⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐹 ∈ (𝑋𝐻𝑌)) → 𝐹 ∈ (𝑋 RngHomo 𝑌)) | ||
Theorem | rngcbas 44589 | Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) | ||
Theorem | rngchomfval 44590 | Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) | ||
Theorem | rngchom 44591 | Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHomo 𝑌)) | ||
Theorem | elrngchom 44592 | A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | rngchomfeqhom 44593 | The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Hom ‘𝐶)) | ||
Theorem | rngccofval 44594 | Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈))) | ||
Theorem | rngcco 44595 | Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) & ⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | dfrngc2 44596 | Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → · = (comp‘(ExtStrCat‘𝑈))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
Theorem | rnghmsscmap2 44597* | The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈)) ⇒ ⊢ (𝜑 → ( RngHomo ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) | ||
Theorem | rnghmsscmap 44598* | The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈)) ⇒ ⊢ (𝜑 → ( RngHomo ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))) | ||
Theorem | rnghmsubcsetclem1 44599 | Lemma 1 for rnghmsubcsetc 44601. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rnghmsubcsetclem2 44600* | Lemma 2 for rnghmsubcsetc 44601. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |