![]() |
Metamath
Proof Explorer Theorem List (p. 425 of 431) | < 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-28080) |
![]() (28081-29605) |
![]() (29606-43060) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rnghmval2 42401 | 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 42402 | 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 42403 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | rnghmghm 42404 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | rnghmf 42405 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹:𝐵⟶𝐶) | ||
Theorem | rnghmmul 42406 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
Theorem | isrnghm2d 42407* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | isrnghmd 42408* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmf1o 42409 | 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 42410 | 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 42411 | An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | rngimrnghm 42412 | An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmco 42413 | The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
⊢ ((𝐹 ∈ (𝑇 RngHomo 𝑈) ∧ 𝐺 ∈ (𝑆 RngHomo 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHomo 𝑈)) | ||
Theorem | idrnghm 42414 | The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHomo 𝑅)) | ||
Theorem | c0mgm 42415* | 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 42416* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | c0ghm 42417* | The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → 𝐻 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | c0rhm 42418* | 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 42419* | 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 42420* | 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 42421* | 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 42422* | 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 42423* | 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 42424 | 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 42425 | The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.) |
⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) → (𝑅 RingHom 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))) | ||
Theorem | rhmisrnghm 42426 | Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | lidldomn1 42427* | 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 42428 | 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 42429 | 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 42430 | A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) | ||
Theorem | lidlmmgm 42431 | 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 42432 | The multiplicative group of a (left) ideal of a ring is a semigroup. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → (mulGrp‘𝐼) ∈ SGrp) | ||
Theorem | lidlrng 42433 | A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) | ||
Theorem | zlidlring 42434 | 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 42435 | 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 42436 | 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 42437* | 0 is an even integer. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 0 ∈ 𝐸 | ||
Theorem | 1neven 42438* | 1 is not an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 1 ∉ 𝐸 | ||
Theorem | 2even 42439* | 2 is an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 2 ∈ 𝐸 | ||
Theorem | 2zlidl 42440* | The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) ⇒ ⊢ 𝐸 ∈ 𝑈 | ||
Theorem | 2zrng 42441* | 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 42321. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) & ⊢ 𝑅 = (ℤring ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngbas 42442* | The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝐸 = (Base‘𝑅) | ||
Theorem | 2zrngadd 42443* | The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ + = (+g‘𝑅) | ||
Theorem | 2zrng0 42444* | The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | 2zrngamgm 42445* | R is an (additive) magma. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mgm | ||
Theorem | 2zrngasgrp 42446* | R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ SGrp | ||
Theorem | 2zrngamnd 42447* | R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | 2zrngacmnd 42448* | R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | 2zrngagrp 42449* | R is an (additive) group. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Grp | ||
Theorem | 2zrngaabl 42450* | R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Abel | ||
Theorem | 2zrngmul 42451* | The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ · = (.r‘𝑅) | ||
Theorem | 2zrngmmgm 42452* | R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Mgm | ||
Theorem | 2zrngmsgrp 42453* | R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ SGrp | ||
Theorem | 2zrngALT 42454* | The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng 42441, 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 42450) and a multiplicative semigroup (see 2zrngmsgrp 42453). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngnmlid 42455* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnmrid 42456* | R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 | ||
Theorem | 2zrngnmlid2 42457* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnring 42458* | R is not a unital ring. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∉ Ring | ||
Theorem | cznrnglem 42459 | Lemma for cznrng 42461: 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 42460 | 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 42461* | 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 42462* | 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 42465. 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 42466 or dfrngc2 42478. 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 42471, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo ↾ (𝐵 × 𝐵)), see rngchomfval 42472, whereas the composition is the ordinary composition of functions, see rngccofval 42476 and rngcco 42477. 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 42480, 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 42483. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 42484 with the identity function as identity arrow, see rngcid 42485. | ||
Syntax | crngc 42463 | Extend class notation to include the category Rng. |
class RngCat | ||
Syntax | crngcALTV 42464 | Extend class notation to include the category Rng. (New usage is discouraged.) |
class RngCatALTV | ||
Definition | df-rngc 42465 | 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 42466* | 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 42467* | 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 42468 | 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 42469 | 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 42470 | 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 42471 | 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 42472 | 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 42473 | 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 42474 | A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | rngchomfeqhom 42475 | 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 42476 | 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 42477 | 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 42478 | 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 42479* | 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‘𝑦) ↑𝑚 (Base‘𝑥)))) | ||
Theorem | rnghmsscmap 42480* | 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‘𝑦) ↑𝑚 (Base‘𝑥)))) | ||
Theorem | rnghmsubcsetclem1 42481 | Lemma 1 for rnghmsubcsetc 42483. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐶)‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rnghmsubcsetclem2 42482* | Lemma 2 for rnghmsubcsetc 42483. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rnghmsubcsetc 42483 | The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.) |
⊢ 𝐶 = (ExtStrCat‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (Rng ∩ 𝑈)) & ⊢ (𝜑 → 𝐻 = ( RngHomo ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) | ||
Theorem | rngccat 42484 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | rngcid 42485 | The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 10-Mar-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑆 = (Base‘𝑋) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆)) | ||
Theorem | rngcsect 42486 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Base‘𝑋) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) | ||
Theorem | rngcinv 42487 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIsom 𝑌) ∧ 𝐺 = ◡𝐹))) | ||
Theorem | rngciso 42488 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) |
⊢ 𝐶 = (RngCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIsom 𝑌))) | ||
Theorem | rngcbasALTV 42489 | Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) | ||
Theorem | rngchomfvalALTV 42490* | Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHomo 𝑦))) | ||
Theorem | rngchomALTV 42491 | Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHomo 𝑌)) | ||
Theorem | elrngchomALTV 42492 | A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | rngccofvalALTV 42493* | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHomo 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHomo (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) | ||
Theorem | rngccoALTV 42494 | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 RngHomo 𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌 RngHomo 𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | rngccatidALTV 42495* | Lemma for rngccatALTV 42496. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥))))) | ||
Theorem | rngccatALTV 42496 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | rngcidALTV 42497 | The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑆 = (Base‘𝑋) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆)) | ||
Theorem | rngcsectALTV 42498 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Base‘𝑋) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHomo 𝑌) ∧ 𝐺 ∈ (𝑌 RngHomo 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) | ||
Theorem | rngcinvALTV 42499 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIsom 𝑌) ∧ 𝐺 = ◡𝐹))) | ||
Theorem | rngcisoALTV 42500 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIsom 𝑌))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |