Home | Metamath
Proof Explorer Theorem List (p. 197 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrsnsgrp 19601 | The (additive group of the) extended reals is not a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∉ SGrp | ||
Theorem | xrsmgmdifsgrp 19602 | The (additive group of the) extended reals is a magma, but not a semigroup, and therefore also no monoid and no group, in contrast to the multiplicative group, see xrsmcmn 19588. (Contributed by AV, 30-Jan-2020.) |
⊢ ℝ*𝑠 ∈ (Mgm ∖ SGrp) | ||
Theorem | xrs1mnd 19603 | The extended real numbers, restricted to ℝ* ∖ {-∞}, form a monoid - in contrast to the full structure, see xrsmgmdifsgrp 19602. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | xrs10 19604 | The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | xrs1cmn 19605 | The extended real numbers restricted to ℝ* ∖ {-∞} form a commutative monoid. They are not a group because 1 + +∞ = 2 + +∞ even though 1 ≠ 2. (Contributed by Mario Carneiro, 27-Nov-2014.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | xrge0subm 19606 | The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑅 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ⇒ ⊢ (0[,]+∞) ∈ (SubMnd‘𝑅) | ||
Theorem | xrge0cmn 19607 | The nonnegative extended real numbers are a monoid. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd | ||
Theorem | xrsds 19608* | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))) | ||
Theorem | xrsdsval 19609 | The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝐷𝐵) = if(𝐴 ≤ 𝐵, (𝐵 +𝑒 -𝑒𝐴), (𝐴 +𝑒 -𝑒𝐵))) | ||
Theorem | xrsdsreval 19610 | The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
Theorem | xrsdsreclblem 19611 | Lemma for xrsdsreclb 19612. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒 -𝑒𝐴) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | xrsdsreclb 19612 | The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵) → ((𝐴𝐷𝐵) ∈ ℝ ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))) | ||
Theorem | cnsubmlem 19613* | Lemma for nn0subm 19620 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 19614* | Lemma for resubdrg 19773 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 19615* | Lemma for resubdrg 19773 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | cnsubdrglem 19616* | Lemma for resubdrg 19773 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐴) ∈ DivRing) | ||
Theorem | qsubdrg 19617 | The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing) | ||
Theorem | zsubrg 19618 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 19619 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 19620 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 19621 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | absabv 19622 | The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ abs ∈ (AbsVal‘ℂfld) | ||
Theorem | zsssubrg 19623 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
Theorem | qsssubdrg 19624 | The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝑅) ∈ DivRing) → ℚ ⊆ 𝑅) | ||
Theorem | cnsubrg 19625 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
Theorem | cnmgpabl 19626 | The unit group of the complex numbers is an abelian group. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ 𝑀 ∈ Abel | ||
Theorem | cnmgpid 19627 | The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by AV, 26-Aug-2021.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ (0g‘𝑀) = 1 | ||
Theorem | cnmsubglem 19628* | Lemma for rpmsubg 19629 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubGrp‘𝑀) | ||
Theorem | rpmsubg 19629 | The positive reals form a multiplicative subgroup of the complex numbers. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ ℝ+ ∈ (SubGrp‘𝑀) | ||
Theorem | gzrngunitlem 19630 | Lemma for gzrngunit 19631. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴)) | ||
Theorem | gzrngunit 19631 | The units on ℤ[i] are the gaussian integers with norm 1. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) ↔ (𝐴 ∈ ℤ[i] ∧ (abs‘𝐴) = 1)) | ||
Theorem | gsumfsum 19632* | Relate a group sum on ℂfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | regsumfsum 19633* | Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 19632. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | expmhm 19634* | Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑁 = (ℂfld ↾s ℕ0) & ⊢ 𝑀 = (mulGrp‘ℂfld) ⇒ ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℕ0 ↦ (𝐴↑𝑥)) ∈ (𝑁 MndHom 𝑀)) | ||
Theorem | nn0srg 19635 | The nonnegative integers form a semiring (commutative by subcmn 18065). (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ SRing | ||
Theorem | rge0srg 19636 | The nonnegative real numbers form a semiring (commutative by subcmn 18065). (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ (ℂfld ↾s (0[,)+∞)) ∈ SRing | ||
According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring 𝑍." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ℤ), the field of complex numbers restricted to the integers. In zringring 19640 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 19656), and zringbas 19643 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring 19638 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to ℂfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra)). | ||
Syntax | zring 19637 | Extend class notation with the (unital) ring of integers. |
class ℤring | ||
Definition | df-zring 19638 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
⊢ ℤring = (ℂfld ↾s ℤ) | ||
Theorem | zringcrng 19639 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ CRing | ||
Theorem | zringring 19640 | The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Ring | ||
Theorem | zringabl 19641 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Abel | ||
Theorem | zringgrp 19642 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
⊢ ℤring ∈ Grp | ||
Theorem | zringbas 19643 | The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤ = (Base‘ℤring) | ||
Theorem | zringplusg 19644 | The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ + = (+g‘ℤring) | ||
Theorem | zringmulg 19645 | The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴(.g‘ℤring)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | zringmulr 19646 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ · = (.r‘ℤring) | ||
Theorem | zring0 19647 | The neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 0 = (0g‘ℤring) | ||
Theorem | zring1 19648 | The multiplicative neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 1 = (1r‘ℤring) | ||
Theorem | zringnzr 19649 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ℤring ∈ NzRing | ||
Theorem | dvdsrzring 19650 | Ring divisibility in the ring of integers corresponds to ordinary divisibility in ℤ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
⊢ ∥ = (∥r‘ℤring) | ||
Theorem | zringlpirlem1 19651 | Lemma for zringlpir 19656. A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring)) & ⊢ (𝜑 → 𝐼 ≠ {0}) ⇒ ⊢ (𝜑 → (𝐼 ∩ ℕ) ≠ ∅) | ||
Theorem | zringlpirlem2 19652 | Lemma for zringlpir 19656. A nonzero ideal of integers contains the least positive element. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Revised by AV, 27-Sep-2020.) |
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring)) & ⊢ (𝜑 → 𝐼 ≠ {0}) & ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐼) | ||
Theorem | zringlpirlem3 19653 | Lemma for zringlpir 19656. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring)) & ⊢ (𝜑 → 𝐼 ≠ {0}) & ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < ) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝐺 ∥ 𝑋) | ||
Theorem | zringinvg 19654 | The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴)) | ||
Theorem | zringunit 19655 | The units of ℤ are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) | ||
Theorem | zringlpir 19656 | The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ ℤring ∈ LPIR | ||
Theorem | zringndrg 19657 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
⊢ ℤring ∉ DivRing | ||
Theorem | zringcyg 19658 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤring ∈ CycGrp | ||
Theorem | zringmpg 19659 | The multiplication group of the ring of integers is the restriction of the multiplication group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.) |
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring) | ||
Theorem | prmirredlem 19660 | A positive integer is irreducible over ℤ iff it is a prime number. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝐼 = (Irred‘ℤring) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) | ||
Theorem | dfprm2 19661 | The positive irreducible elements of ℤ are the prime numbers. This is an alternative way to define ℙ. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝐼 = (Irred‘ℤring) ⇒ ⊢ ℙ = (ℕ ∩ 𝐼) | ||
Theorem | prmirred 19662 | The irreducible elements of ℤ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝐼 = (Irred‘ℤring) ⇒ ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ)) | ||
Theorem | expghm 19663* | Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑀 = (mulGrp‘ℂfld) & ⊢ 𝑈 = (𝑀 ↾s (ℂ ∖ {0})) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈)) | ||
Theorem | mulgghm2 19664* | The powers of a group element give a homomorphism from ℤ to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) | ||
Theorem | mulgrhm 19665* | The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅)) | ||
Theorem | mulgrhm2 19666* | The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹}) | ||
Syntax | czrh 19667 | Map the rationals into a field, or the integers into a ring. |
class ℤRHom | ||
Syntax | czlm 19668 | Augment an abelian group with vector space operations to turn it into a ℤ-module. |
class ℤMod | ||
Syntax | cchr 19669 | Syntax for ring characteristic. |
class chr | ||
Syntax | czn 19670 | The ring of integers modulo 𝑛. |
class ℤ/nℤ | ||
Definition | df-zrh 19671 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 17364). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟)) | ||
Definition | df-zlm 19672 | Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet 〈(Scalar‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), (.g‘𝑔)〉)) | ||
Definition | df-chr 19673 | The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔))) | ||
Definition | df-zn 19674* | Define the ring of integers mod 𝑛. This is literally the quotient ring of ℤ by the ideal 𝑛ℤ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) | ||
Theorem | zrhval 19675 | Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ 𝐿 = ∪ (ℤring RingHom 𝑅) | ||
Theorem | zrhval2 19676* | Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) | ||
Theorem | zrhmulg 19677 | Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 )) | ||
Theorem | zrhrhmb 19678 | The ℤRHom homomorphism is the unique ring homomorphism from 𝑍. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿)) | ||
Theorem | zrhrhm 19679 | The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅)) | ||
Theorem | zrh1 19680 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 ) | ||
Theorem | zrh0 19681 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 ) | ||
Theorem | zrhpropd 19682* | The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿)) | ||
Theorem | zlmval 19683 | Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet 〈(Scalar‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), · 〉)) | ||
Theorem | zlmlem 19684 | Lemma for zlmbas 19685 and zlmplusg 19686. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 5 ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
Theorem | zlmbas 19685 | Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
Theorem | zlmplusg 19686 | Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
Theorem | zlmmulr 19687 | Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.r‘𝐺) ⇒ ⊢ · = (.r‘𝑊) | ||
Theorem | zlmsca 19688 | Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊)) | ||
Theorem | zlmvsca 19689 | Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = ( ·𝑠 ‘𝑊) | ||
Theorem | zlmlmod 19690 | The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod) | ||
Theorem | zlmassa 19691 | The ℤ-module operation turns a ring into an associative algebra over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg) | ||
Theorem | chrval 19692 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑂 = (od‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑂‘ 1 ) = 𝐶 | ||
Theorem | chrcl 19693 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0) | ||
Theorem | chrid 19694 | The canonical ℤ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘𝐶) = 0 ) | ||
Theorem | chrdvds 19695 | The ℤ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ 𝑁 ↔ (𝐿‘𝑁) = 0 )) | ||
Theorem | chrcong 19696 | If two integers are congruent relative to the ring characteristic, their images in the ring are the same. (Contributed by Mario Carneiro, 24-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ (𝑀 − 𝑁) ↔ (𝐿‘𝑀) = (𝐿‘𝑁))) | ||
Theorem | chrnzr 19697 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1)) | ||
Theorem | chrrhm 19698 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅)) | ||
Theorem | domnchr 19699 | The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝑅 ∈ Domn → ((chr‘𝑅) = 0 ∨ (chr‘𝑅) ∈ ℙ)) | ||
Theorem | znlidl 19700 | The set 𝑛ℤ is an ideal in ℤ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) ⇒ ⊢ (𝑁 ∈ ℤ → (𝑆‘{𝑁}) ∈ (LIdeal‘ℤring)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |