Home | Metamath
Proof Explorer Theorem List (p. 207 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gzsubrg 20601 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 20602 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 20603 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | absabv 20604 | 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 20605 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
Theorem | qsssubdrg 20606 | 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 20607 | There are no subrings of the complex numbers strictly between ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝑅 ∈ (SubRing‘ℂfld) ∧ ℝ ⊆ 𝑅) → 𝑅 ∈ {ℝ, ℂ}) | ||
Theorem | cnmgpabl 20608 | 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 20609 | 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 20610* | Lemma for rpmsubg 20611 and friends. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 ≠ 0) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ (𝑥 ∈ 𝐴 → (1 / 𝑥) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubGrp‘𝑀) | ||
Theorem | rpmsubg 20611 | 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 20612 | Lemma for gzrngunit 20613. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑍 = (ℂfld ↾s ℤ[i]) ⇒ ⊢ (𝐴 ∈ (Unit‘𝑍) → 1 ≤ (abs‘𝐴)) | ||
Theorem | gzrngunit 20613 | 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 20614* | 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 20615* | Relate a group sum on (ℂfld ↾s ℝ) to a finite sum on the reals. Cf. gsumfsum 20614. (Contributed by Thierry Arnoux, 7-Sep-2018.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((ℂfld ↾s ℝ) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | expmhm 20616* | 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 20617 | The nonnegative integers form a semiring (commutative by subcmn 18959). (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ SRing | ||
Theorem | rge0srg 20618 | The nonnegative real numbers form a semiring (commutative by subcmn 18959). (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 20622 it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir 20638), and zringbas 20625 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring 20620 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) 20620). | ||
Syntax | zring 20619 | Extend class notation with the (unital) ring of integers. |
class ℤring | ||
Definition | df-zring 20620 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
⊢ ℤring = (ℂfld ↾s ℤ) | ||
Theorem | zringcrng 20621 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ CRing | ||
Theorem | zringring 20622 | 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 20623 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Abel | ||
Theorem | zringgrp 20624 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
⊢ ℤring ∈ Grp | ||
Theorem | zringbas 20625 | 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 20626 | 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 20627 | 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 20628 | 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 20629 | 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 20630 | 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 20631 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ℤring ∈ NzRing | ||
Theorem | dvdsrzring 20632 | 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 20633 | Lemma for zringlpir 20638. 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 20634 | Lemma for zringlpir 20638. 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 20635 | Lemma for zringlpir 20638. 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 20636 | 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 20637 | 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 20638 | 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 20639 | The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021.) |
⊢ ℤring ∉ DivRing | ||
Theorem | zringcyg 20640 | The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤring ∈ CycGrp | ||
Theorem | zringmpg 20641 | 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 20642 | 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 20643 | 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 20644 | 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 20645* | 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 20646* | 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 20647* | 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 20648* | 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 20649 | Map the rationals into a field, or the integers into a ring. |
class ℤRHom | ||
Syntax | czlm 20650 | Augment an abelian group with vector space operations to turn it into a ℤ-module. |
class ℤMod | ||
Syntax | cchr 20651 | Syntax for ring characteristic. |
class chr | ||
Syntax | czn 20652 | The ring of integers modulo 𝑛. |
class ℤ/nℤ | ||
Definition | df-zrh 20653 | 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 18227). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟)) | ||
Definition | df-zlm 20654 | 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 20655 | 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 20656* | 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 20657 | 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 20658* | Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) | ||
Theorem | zrhmulg 20659 | Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 )) | ||
Theorem | zrhrhmb 20660 | 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 20661 | 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 20662 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 ) | ||
Theorem | zrh0 20663 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 ) | ||
Theorem | zrhpropd 20664* | 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 20665 | 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 20666 | Lemma for zlmbas 20667 and zlmplusg 20668. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 5 ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
Theorem | zlmbas 20667 | Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
Theorem | zlmplusg 20668 | Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
Theorem | zlmmulr 20669 | Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.r‘𝐺) ⇒ ⊢ · = (.r‘𝑊) | ||
Theorem | zlmsca 20670 | Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊)) | ||
Theorem | zlmvsca 20671 | Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = ( ·𝑠 ‘𝑊) | ||
Theorem | zlmlmod 20672 | 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 20673 | The ℤ-module operation turns a ring into an associative algebra over ℤ. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Ring ↔ 𝑊 ∈ AssAlg) | ||
Theorem | chrval 20674 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑂 = (od‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑂‘ 1 ) = 𝐶 | ||
Theorem | chrcl 20675 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0) | ||
Theorem | chrid 20676 | 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 20677 | 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 20678 | 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 20679 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1)) | ||
Theorem | chrrhm 20680 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅)) | ||
Theorem | domnchr 20681 | 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 20682 | The set 𝑛ℤ is an ideal in ℤ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) ⇒ ⊢ (𝑁 ∈ ℤ → (𝑆‘{𝑁}) ∈ (LIdeal‘ℤring)) | ||
Theorem | zncrng2 20683 | The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) ⇒ ⊢ (𝑁 ∈ ℤ → 𝑈 ∈ CRing) | ||
Theorem | znval 20684 | The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | znle 20685 | The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | ||
Theorem | znval2 20686 | Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet 〈(le‘ndx), ≤ 〉)) | ||
Theorem | znbaslem 20687 | Lemma for znbas 20692. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐸 = Slot 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐾 < ;10 ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌)) | ||
Theorem | znbas2 20688 | The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌)) | ||
Theorem | znadd 20689 | The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌)) | ||
Theorem | znmul 20690 | The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌)) | ||
Theorem | znzrh 20691 | The ℤ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑈) = (ℤRHom‘𝑌)) | ||
Theorem | znbas 20692 | The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑅 = (ℤring ~QG (𝑆‘{𝑁})) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℤ / 𝑅) = (Base‘𝑌)) | ||
Theorem | zncrng 20693 | ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing) | ||
Theorem | znzrh2 20694* | The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁})) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐿 = (𝑥 ∈ ℤ ↦ [𝑥] ∼ )) | ||
Theorem | znzrhval 20695 | The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑆 = (RSpan‘ℤring) & ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁})) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) = [𝐴] ∼ ) | ||
Theorem | znzrhfo 20696 | The ℤ ring homomorphism is a surjection onto ℤ / 𝑛ℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→𝐵) | ||
Theorem | zncyg 20697 | The group ℤ / 𝑛ℤ is cyclic for all 𝑛 (including 𝑛 = 0). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp) | ||
Theorem | zndvds 20698 | Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
Theorem | zndvds0 20699 | Special case of zndvds 20698 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴)) | ||
Theorem | znf1o 20700 | The function 𝐹 enumerates all equivalence classes in ℤ/nℤ for each 𝑛. When 𝑛 = 0, ℤ / 0ℤ = ℤ / {0} ≈ ℤ so we let 𝑊 = ℤ; otherwise 𝑊 = {0, ..., 𝑛 − 1} enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1-onto→𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |