HomeTheorem List (p. 340 of 513)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 340 of 513) | < 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-31550) |
Hilbert Space Explorer
(31551-33073) |
Users' Mathboxes
(33074-51270) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rlocmulval 33901 | Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ ⊗ = (.r‘𝐿) ⇒ ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ ) | ||
| Theorem | rloccring 33902 | The ring localization 𝐿 of a commutative ring 𝑅 by a multiplicatively closed set 𝑆 is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) ⇒ ⊢ (𝜑 → 𝐿 ∈ CRing) | ||
| Theorem | rloc0g 33903 | The zero of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ 𝑂 = [⟨ 0 , 1 ⟩] ∼ ⇒ ⊢ (𝜑 → 𝑂 = (0g‘𝐿)) | ||
| Theorem | rloc1r 33904 | The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ 𝐼 = [⟨ 1 , 1 ⟩] ∼ ⇒ ⊢ (𝜑 → 𝐼 = (1r‘𝐿)) | ||
| Theorem | rlocf1 33905* | The embedding 𝐹 of a ring 𝑅 into its localization 𝐿. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝑆 ⊆ (RLReg‘𝑅)) ⇒ ⊢ (𝜑 → (𝐹:𝐵⟶1-1((𝐵 × 𝑆) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom 𝐿))) | ||
| Theorem | rlocinvunit 33906 | In the localization of a ring 𝑅 at 𝑆, inverses of elements of 𝑆 are units. (Contributed by Thierry Arnoux, 6-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ 𝑊 = (Unit‘𝐿) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → [⟨ 1 , 𝑄⟩] ∼ ∈ 𝑊) | ||
| Theorem | rlocisunit 33907* | Characterize the units of the localization 𝐿 of a ring 𝑅 at 𝑆 as the elements with a "numerator" 𝑃 in the saturation 𝑇 of 𝑆. (Contributed by Thierry Arnoux, 6-Jun-2026.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐿 = (𝑅 RLocal 𝑆) & ⊢ 𝑊 = (Unit‘𝐿) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) & ⊢ ∼ = (𝑅 ~RL 𝑆) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) & ⊢ 𝑇 = {𝑟 ∈ 𝐵 ∣ ∃𝑠 ∈ 𝐵 (𝑟 · 𝑠) ∈ 𝑆} ⇒ ⊢ (𝜑 → ([⟨𝑃, 𝑄⟩] ∼ ∈ 𝑊 ↔ 𝑃 ∈ 𝑇)) | ||
| Theorem | domnmuln0rd 33908 | In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 · 𝑌) ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) | ||
| Theorem | domnprodn0 33909 | In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐹 ∈ Word (𝐵 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0 ) | ||
| Theorem | domnprodeq0 33910 | A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 20990 for any number of factors. See also domnprodn0 33909. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹) = 0 ↔ 0 ∈ ran 𝐹)) | ||
| Theorem | domnpropd 33911* | If two structures have the same components (properties), one is a domain iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Domn ↔ 𝐿 ∈ Domn)) | ||
| Theorem | idompropd 33912* | If two structures have the same components (properties), one is a integral domain iff the other one is. See also domnpropd 33911. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ IDomn ↔ 𝐿 ∈ IDomn)) | ||
| Theorem | idomrcan 33913 | Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) (Proof shortened by SN, 21-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ∖ { 0 })) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | 1rrg 33914 | The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025.) |
| ⊢ 1 = (1r‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 1 ∈ 𝐸) | ||
| Theorem | rrgsubm 33915 | The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) | ||
| Theorem | subrdom 33916 | A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Domn) | ||
| Theorem | subridom 33917 | A subring of an integral domain is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | subrfld 33918 | A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ Field) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ IDomn) | ||
| Theorem | ricnzr1 33919 | A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ NzRing) → 𝑆 ∈ NzRing) | ||
| Theorem | ricdomn1 33920 | A ring isomorphism maps a domain to a domain. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn) → 𝑆 ∈ Domn) | ||
| Theorem | ricdomn 33921 | A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Domn ↔ 𝑆 ∈ Domn)) | ||
| Syntax | ceuf 33922 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 33923 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 33925 instead. (New usage is discouraged.) |
| ⊢ EuclF = Slot ;21 | ||
| Theorem | eufndx 33924 | Index value of the Euclidean function slot. Use ndxarg 17403. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| ⊢ (EuclF‘ndx) = ;21 | ||
| Theorem | eufid 33925 | Utility theorem: index-independent form of df-euf 33923. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EuclF = Slot (EuclF‘ndx) | ||
| Syntax | cedom 33926 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 33927* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ EDomn = {𝑑 ∈ IDomn ∣ [(EuclF‘𝑑) / 𝑒][(Base‘𝑑) / 𝑣](Fun 𝑒 ∧ (𝑒 “ (𝑣 ∖ {(0g‘𝑑)})) ⊆ (0[,)+∞) ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ (𝑣 ∖ {(0g‘𝑑)})∃𝑞 ∈ 𝑣 ∃𝑟 ∈ 𝑣 (𝑎 = ((𝑏(.r‘𝑑)𝑞)(+g‘𝑑)𝑟) ∧ (𝑟 = (0g‘𝑑) ∨ (𝑒‘𝑟) < (𝑒‘𝑏))))} | ||
| Theorem | rndrhmcl 33928 | The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝑅 = (𝑁 ↾s ran 𝐹) & ⊢ 0 = (0g‘𝑁) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) & ⊢ (𝜑 → ran 𝐹 ≠ { 0 }) & ⊢ (𝜑 → 𝑀 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
| Theorem | qfld 33929 | The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ Field | ||
| Theorem | subsdrg 33930 | A subring of a sub-division-ring is a sub-division-ring. See also subsubrg 20880. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) ⇒ ⊢ (𝜑 → (𝐵 ∈ (SubDRing‘𝑆) ↔ (𝐵 ∈ (SubDRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
| Theorem | sdrgdvcl 33931 | A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ / = (/r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 / 𝑌) ∈ 𝐴) | ||
| Theorem | sdrginvcl 33932 | A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐼 = (invr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubDRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ 0 ) → (𝐼‘𝑋) ∈ 𝐴) | ||
| Theorem | primefldchr 33933 | The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅)) ⇒ ⊢ (𝑅 ∈ DivRing → (chr‘𝑃) = (chr‘𝑅)) | ||
| Syntax | cfrac 33934 | Syntax for the field of fractions of a given integral domain. |
| class Frac | ||
| Definition | df-frac 33935 | Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.) |
| ⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟))) | ||
| Theorem | fracval 33936 | Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ ( Frac ‘𝑅) = (𝑅 RLocal (RLReg‘𝑅)) | ||
| Theorem | fracbas 33937 | The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐹 = ( Frac ‘𝑅) & ⊢ ∼ = (𝑅 ~RL 𝐸) ⇒ ⊢ ((𝐵 × 𝐸) / ∼ ) = (Base‘𝐹) | ||
| Theorem | fracerl 33938 | Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∼ = (𝑅 ~RL (RLReg‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (RLReg‘𝑅)) & ⊢ (𝜑 → 𝐻 ∈ (RLReg‘𝑅)) ⇒ ⊢ (𝜑 → (⟨𝐸, 𝐹⟩ ∼ ⟨𝐺, 𝐻⟩ ↔ (𝐸 · 𝐻) = (𝐺 · 𝐹))) | ||
| Theorem | fracf1 33939* | The embedding of a commutative ring 𝑅 into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ∼ = (𝑅 ~RL 𝐸) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [⟨𝑥, 1 ⟩] ∼ ) ⇒ ⊢ (𝜑 → (𝐹:𝐵⟶1-1((𝐵 × 𝐸) / ∼ ) ∧ 𝐹 ∈ (𝑅 RingHom ( Frac ‘𝑅)))) | ||
| Theorem | fracfld 33940 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | ||
| Theorem | idomsubr 33941* | Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠)) | ||
| Syntax | cfldgen 33942 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 33943* | Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33946). If the base structure is a field, this is a subfield (see fldgenfld 33952 and fldsdrgfld 21085). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.) |
| ⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}) | ||
| Theorem | fldgenval 33944* | Value of the field generating function: (𝐹 fldGen 𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) | ||
| Theorem | fldgenssid 33945 | The field generated by a set of elements contains those elements. See lspssid 21290. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgensdrg 33946 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33947 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33948 | Generated subfields preserve subset ordering. ( see lspss 21289 and spanss 31980) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33949 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33950 | The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ 𝑆) | ||
| Theorem | fldgenid 33951 | The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵) | ||
| Theorem | fldgenfld 33952 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field) | ||
| Theorem | primefldgen1 33953 | The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → ∩ (SubDRing‘𝑅) = (𝑅 fldGen { 1 })) | ||
| Theorem | 1fldgenq 33954 | The field of rational numbers ℚ is generated by 1 in ℂfld, that is, ℚ is the prime field of ℂfld. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ (ℂfld fldGen {1}) = ℚ | ||
| Theorem | rhmdvd 33955 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | kerunit 33956 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝑈 ∩ (◡𝐹 “ { 0 })) ≠ ∅) → 1 = 0 ) | ||
| Syntax | cresv 33957 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 33958* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
| ⊢ ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))) | ||
| Theorem | reldmresv 33959 | The scalar restriction is a proper operator, so it can be used with ovprc1 7482. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 33960 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 33961 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 33962 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 33963 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 33964 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | resvbas 33965 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 33966 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 33967 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 33968 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 33969 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 33970 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 33971 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 33972 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | cnfldfld 33973 | The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ℂfld ∈ Field | ||
| Theorem | reofld 33974 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 33975 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | gsumind 33976 | The group sum of an indicator function of the set 𝐴 gives the size of 𝐴. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (ℂfld Σg ((𝟭‘𝑂)‘𝐴)) = (♯‘𝐴)) | ||
| Theorem | rearchi 33977 | The field of the real numbers is Archimedean. See also arch 12630. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 33978 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 33979 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ 𝑊 = (𝐺 ↾v (0[,)+∞)) ⇒ ⊢ 𝑊 ∈ SLMod | ||
| Theorem | qusker 33980* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
| Theorem | eqgvscpbl 33981 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∼ 𝑌 → (𝐾 · 𝑋) ∼ (𝐾 · 𝑌))) | ||
| Theorem | qusvscpbl 33982* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉)))) | ||
| Theorem | qusvsval 33983 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐾 ∙ [𝑋](𝑀 ~QG 𝐺)) = [(𝐾 · 𝑋)](𝑀 ~QG 𝐺)) | ||
| Theorem | imaslmod 33984* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
| ⊢ (𝜑 → 𝑁 = (𝐹 “s 𝑀)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:𝑉⟶onto𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏)))) & ⊢ (𝜑 → 𝑀 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
| Theorem | imasmhm 33985* | Given a function 𝐹 with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Mnd) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Mnd ∧ 𝐹 ∈ (𝑊 MndHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasghm 33986* | Given a function 𝐹 with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Grp) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Grp ∧ 𝐹 ∈ (𝑊 GrpHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasrhm 33987* | Given a function 𝐹 with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ · = (.r‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Ring ∧ 𝐹 ∈ (𝑊 RingHom (𝐹 “s 𝑊)))) | ||
| Theorem | imaslmhm 33988* | Given a function 𝐹 with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 × 𝑎)) = (𝐹‘(𝑘 × 𝑏)))) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ × = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ LMod ∧ 𝐹 ∈ (𝑊 LMHom (𝐹 “s 𝑊)))) | ||
| Theorem | quslmod 33989 | If 𝐺 is a submodule in 𝑀, then 𝑁 = 𝑀 / 𝐺 is a left module, called the quotient module of 𝑀 by 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
| Theorem | quslmhm 33990* | If 𝐺 is a submodule of 𝑀, then the "natural map" from elements to their cosets is a left module homomorphism from 𝑀 to 𝑀 / 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑀 LMHom 𝑁)) | ||
| Theorem | quslvec 33991 | If 𝑆 is a vector subspace in 𝑊, then 𝑄 = 𝑊 / 𝑆 is a vector space, called the quotient space of 𝑊 by 𝑆. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑄 = (𝑊 /s (𝑊 ~QG 𝑆)) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑊)) ⇒ ⊢ (𝜑 → 𝑄 ∈ LVec) | ||
| Theorem | znfermltl 33992 | Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑃) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ ↑ = (.g‘(mulGrp‘𝑍)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴) | ||
| Theorem | islinds5 33993* | A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵) → (𝑉 ∈ (LIndS‘𝑊) ↔ ∀𝑎 ∈ (𝐾 ↑m 𝑉)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))) = 𝑂) → 𝑎 = (𝑉 × { 0 })))) | ||
| Theorem | ellspds 33994* | Variation on ellspd 22138. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
| Theorem | 0ellsp 33995 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆)) | ||
| Theorem | 0nellinds 33996 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹) | ||
| Theorem | elrsp 33997* | Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐼) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝐼)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝐼 ↦ ((𝑎‘𝑖) · 𝑖)))))) | ||
| Theorem | ellpi 33998 | Elementhood in a left principal ideal in terms of the "divides" relation. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝐾‘{𝑋}) ↔ 𝑋 ∥ 𝑌)) | ||
| Theorem | lpirlidllpi 33999* | In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LPIR) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})) | ||
| Theorem | rspidlid 34000 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |