Home | Metamath
Proof Explorer Theorem List (p. 313 of 463) | < 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-29031) |
Hilbert Space Explorer
(29032-30554) |
Users' Mathboxes
(30555-46226) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | archiabllem2b 31201* | Lemma for archiabl 31203. (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ≤ = (le‘𝑊) & ⊢ < = (lt‘𝑊) & ⊢ · = (.g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ oGrp) & ⊢ (𝜑 → 𝑊 ∈ Archi) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → (oppg‘𝑊) ∈ oGrp) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎) → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | archiabllem2 31202* | Archimedean ordered groups with no minimal positive value are abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ ≤ = (le‘𝑊) & ⊢ < = (lt‘𝑊) & ⊢ · = (.g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ oGrp) & ⊢ (𝜑 → 𝑊 ∈ Archi) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → (oppg‘𝑊) ∈ oGrp) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎) → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) ⇒ ⊢ (𝜑 → 𝑊 ∈ Abel) | ||
Theorem | archiabl 31203 | Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ ((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) → 𝑊 ∈ Abel) | ||
Syntax | cslmd 31204 | Extend class notation with class of all semimodules. |
class SLMod | ||
Definition | df-slmd 31205* | Define the class of all (left) modules over semirings, i.e. semimodules, which are generalizations of left modules. A semimodule is a commutative monoid (=vectors) together with a semiring (=scalars) and a left scalar product connecting them. (0[,]+∞) for example is not a full fledged left module, but is a semimodule. Definition of [Golan] p. 149. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ SLMod = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][( ·𝑠 ‘𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0g‘𝑓)𝑠𝑤) = (0g‘𝑔))))} | ||
Theorem | isslmd 31206* | The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))) | ||
Theorem | slmdlema 31207 | Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌 ∧ (𝑂 · 𝑌) = 0 ))) | ||
Theorem | lmodslmd 31208 | Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ SLMod) | ||
Theorem | slmdcmn 31209 | A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (𝑊 ∈ SLMod → 𝑊 ∈ CMnd) | ||
Theorem | slmdmnd 31210 | A semimodule is a monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (𝑊 ∈ SLMod → 𝑊 ∈ Mnd) | ||
Theorem | slmdsrg 31211 | The scalar component of a semimodule is a semiring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ SLMod → 𝐹 ∈ SRing) | ||
Theorem | slmdbn0 31212 | The base set of a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ SLMod → 𝐵 ≠ ∅) | ||
Theorem | slmdacl 31213 | Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
Theorem | slmdmcl 31214 | Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
Theorem | slmdsn0 31215 | The set of scalars in a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 𝐵 ≠ ∅) | ||
Theorem | slmdvacl 31216 | Closure of vector addition for a semiring left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) | ||
Theorem | slmdass 31217 | Semiring left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | slmdvscl 31218 | Closure of scalar product for a semiring left module. (hvmulcl 29126 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉) | ||
Theorem | slmdvsdi 31219 | Distributive law for scalar product. (ax-hvdistr1 29121 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) | ||
Theorem | slmdvsdir 31220 | Distributive law for scalar product. (ax-hvdistr1 29121 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
Theorem | slmdvsass 31221 | Associative law for scalar product. (ax-hvmulass 29120 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
Theorem | slmd0cl 31222 | The ring zero in a semimodule belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 0 ∈ 𝐾) | ||
Theorem | slmd1cl 31223 | The ring unit in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ (𝑊 ∈ SLMod → 1 ∈ 𝐾) | ||
Theorem | slmdvs1 31224 | Scalar product with ring unit. (ax-hvmulid 29119 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) | ||
Theorem | slmd0vcl 31225 | The zero vector is a vector. (ax-hv0cl 29116 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ SLMod → 0 ∈ 𝑉) | ||
Theorem | slmd0vlid 31226 | Left identity law for the zero vector. (hvaddid2 29136 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | slmd0vrid 31227 | Right identity law for the zero vector. (ax-hvaddid 29117 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | slmd0vs 31228 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 29123 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) | ||
Theorem | slmdvs0 31229 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 29137 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 ) | ||
Theorem | gsumvsca1 31230* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐺 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ SLMod) & ⊢ (𝜑 → 𝑃 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑄 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) | ||
Theorem | gsumvsca2 31231* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) (Proof shortened by AV, 12-Dec-2019.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐺 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ SLMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄)) | ||
Theorem | prmsimpcyc 31232 | A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((♯‘𝐵) ∈ ℙ → (𝐺 ∈ SimpGrp ↔ 𝐺 ∈ CycGrp)) | ||
Theorem | rngurd 31233* | Deduce the unit of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) ⇒ ⊢ (𝜑 → 1 = (1r‘𝑅)) | ||
Theorem | dvdschrmulg 31234 | In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016.) |
⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵) → (𝑁 · 𝐴) = 0 ) | ||
Theorem | freshmansdream 31235 | For a prime number 𝑃, if 𝑋 and 𝑌 are members of a commutative ring 𝑅 of characteristic 𝑃, then ((𝑋 + 𝑌)↑𝑃) = ((𝑋↑𝑃) + (𝑌↑𝑃)). This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) | ||
Theorem | frobrhm 31236* | In a commutative ring with prime characteristic, the Frobenius function 𝐹 is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑃 ↑ 𝑥)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑅)) | ||
Theorem | ress1r 31237 | 1r is unaffected by restriction. This is a bit more generic than subrg1 19843. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 1 = (1r‘𝑆)) | ||
Theorem | dvrdir 31238 | Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 + 𝑌) / 𝑍) = ((𝑋 / 𝑍) + (𝑌 / 𝑍))) | ||
Theorem | rdivmuldivd 31239 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 · 𝑍) / (𝑌 · 𝑊))) | ||
Theorem | ringinvval 31240* | The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) = (℩𝑦 ∈ 𝑈 (𝑦 ∗ 𝑋) = 1 )) | ||
Theorem | dvrcan5 31241 | Cancellation law for common factor in ratio. (divcan5 11564 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ / = (/r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 / 𝑌)) | ||
Theorem | subrgchr 31242 | If 𝐴 is a subring of 𝑅, then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → (chr‘(𝑅 ↾s 𝐴)) = (chr‘𝑅)) | ||
Theorem | rmfsupp2 31243* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023.) |
⊢ 𝑅 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Ring) & ⊢ (𝜑 → 𝑉 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ 𝑅) & ⊢ (𝜑 → 𝐴:𝑉⟶𝑅) & ⊢ (𝜑 → 𝐴 finSupp (0g‘𝑀)) ⇒ ⊢ (𝜑 → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) finSupp (0g‘𝑀)) | ||
Theorem | primefldchr 31244 | 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 | corng 31245 | Extend class notation with the class of all ordered rings. |
class oRing | ||
Syntax | cofld 31246 | Extend class notation with the class of all ordered fields. |
class oField | ||
Definition | df-orng 31247* | Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))} | ||
Definition | df-ofld 31248 | Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
⊢ oField = (Field ∩ oRing) | ||
Theorem | isorng 31249* | An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ≤ = (le‘𝑅) ⇒ ⊢ (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) | ||
Theorem | orngring 31250 | An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) | ||
Theorem | orngogrp 31251 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) | ||
Theorem | isofld 31252 | An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ (𝐹 ∈ oField ↔ (𝐹 ∈ Field ∧ 𝐹 ∈ oRing)) | ||
Theorem | orngmul 31253 | In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ≤ = (le‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌)) → 0 ≤ (𝑋 · 𝑌)) | ||
Theorem | orngsqr 31254 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ≤ = (le‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋)) | ||
Theorem | ornglmulle 31255 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ≤ = (le‘𝑅) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 0 ≤ 𝑍) ⇒ ⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌)) | ||
Theorem | orngrmulle 31256 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ≤ = (le‘𝑅) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 0 ≤ 𝑍) ⇒ ⊢ (𝜑 → (𝑋 · 𝑍) ≤ (𝑌 · 𝑍)) | ||
Theorem | ornglmullt 31257 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 0 < 𝑍) ⇒ ⊢ (𝜑 → (𝑍 · 𝑋) < (𝑍 · 𝑌)) | ||
Theorem | orngrmullt 31258 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 0 < 𝑍) ⇒ ⊢ (𝜑 → (𝑋 · 𝑍) < (𝑌 · 𝑍)) | ||
Theorem | orngmullt 31259 | In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 0 < 𝑌) ⇒ ⊢ (𝜑 → 0 < (𝑋 · 𝑌)) | ||
Theorem | ofldfld 31260 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ (𝐹 ∈ oField → 𝐹 ∈ Field) | ||
Theorem | ofldtos 31261 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ (𝐹 ∈ oField → 𝐹 ∈ Toset) | ||
Theorem | orng0le1 31262 | In an ordered ring, the ring unit is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ 0 = (0g‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ ≤ = (le‘𝐹) ⇒ ⊢ (𝐹 ∈ oRing → 0 ≤ 1 ) | ||
Theorem | ofldlt1 31263 | In an ordered field, the ring unit is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ 0 = (0g‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ < = (lt‘𝐹) ⇒ ⊢ (𝐹 ∈ oField → 0 < 1 ) | ||
Theorem | ofldchr 31264 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
⊢ (𝐹 ∈ oField → (chr‘𝐹) = 0) | ||
Theorem | suborng 31265 | Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing) | ||
Theorem | subofld 31266 | Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ((𝐹 ∈ oField ∧ (𝐹 ↾s 𝐴) ∈ Field) → (𝐹 ↾s 𝐴) ∈ oField) | ||
Theorem | isarchiofld 31267* | Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐻 = (ℤRHom‘𝑊) & ⊢ < = (lt‘𝑊) ⇒ ⊢ (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛))) | ||
Theorem | rhmdvdsr 31268 | A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ / = (∥r‘𝑆) ⇒ ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ∥ 𝐵) → (𝐹‘𝐴) / (𝐹‘𝐵)) | ||
Theorem | rhmopp 31269 | A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((oppr‘𝑅) RingHom (oppr‘𝑆))) | ||
Theorem | elrhmunit 31270 | Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆)) | ||
Theorem | rhmdvd 31271 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
Theorem | rhmunitinv 31272 | Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴))) | ||
Theorem | kerunit 31273 | 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 31274 | Extend class notation with the scalar restriction operation. |
class ↾v | ||
Definition | df-resv 31275* | 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 31276 | The scalar restriction is a proper operator, so it can be used with ovprc1 7274. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ Rel dom ↾v | ||
Theorem | resvval 31277 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Scalar‘ndx), (𝐹 ↾s 𝐴)〉))) | ||
Theorem | resvid2 31278 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
Theorem | resvval2 31279 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Scalar‘ndx), (𝐹 ↾s 𝐴)〉)) | ||
Theorem | resvsca 31280 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
Theorem | resvlem 31281 | Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 5 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
Theorem | resvbas 31282 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
Theorem | resvplusg 31283 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
Theorem | resvvsca 31284 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | resvmulr 31285 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
Theorem | resv0g 31286 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
Theorem | resv1r 31287 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
Theorem | resvcmn 31288 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
Theorem | gzcrng 31289 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
Theorem | reofld 31290 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ℝfld ∈ oField | ||
Theorem | nn0omnd 31291 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
Theorem | rearchi 31292 | The field of the real numbers is Archimedean. See also arch 12117. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
⊢ ℝfld ∈ Archi | ||
Theorem | nn0archi 31293 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
Theorem | xrge0slmod 31294 | 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 31295* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
Theorem | eqgvscpbl 31296 | 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 31297* | 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 | qusscaval 31298 | 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 31299* | 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 | quslmod 31300 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |