Home | Metamath
Proof Explorer Theorem List (p. 196 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | csdrg 19501 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 19502* | A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ SubDRing = (𝑤 ∈ DivRing ↦ {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing}) | ||
Theorem | issdrg 19503 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)) | ||
Theorem | sdrgid 19504 | Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝑅)) | ||
Theorem | sdrgss 19505 | A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑆 ⊆ 𝐵) | ||
Theorem | issdrg2 19506* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐼 = (invr‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑆 ∖ { 0 })(𝐼‘𝑥) ∈ 𝑆)) | ||
Theorem | acsfn1p 19507* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑌 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ (𝑎 ∩ 𝑌)𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | subrgacs 19508 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | sdrgacs 19509 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → (SubDRing‘𝑅) ∈ (ACS‘𝐵)) | ||
Theorem | cntzsdrg 19510 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubDRing‘𝑅)) | ||
Theorem | subdrgint 19511* | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐿 = (𝑅 ↾s ∩ 𝑆) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑆 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (𝑅 ↾s 𝑠) ∈ DivRing) ⇒ ⊢ (𝜑 → 𝐿 ∈ DivRing) | ||
Theorem | sdrgint 19512 | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ⊆ (SubDRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubDRing‘𝑅)) | ||
Theorem | primefld 19513 | The smallest sub division ring of a division ring, here named 𝑃, is a field, called the Prime Field of 𝑅. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅)) ⇒ ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ Field) | ||
Theorem | primefld0cl 19514 | The prime field contains the neutral element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 0 ∈ ∩ (SubDRing‘𝑅)) | ||
Theorem | primefld1cl 19515 | The prime field contains the multiplicative neutral element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 1 ∈ ∩ (SubDRing‘𝑅)) | ||
Syntax | cabv 19516 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 19517* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 14583 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) | ||
Theorem | abvfval 19518* | Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴 = {𝑓 ∈ ((0[,)+∞) ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) | ||
Theorem | isabv 19519* | Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) | ||
Theorem | isabvd 19520* | Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝜑 → 𝐴 = (AbsVal‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 0 = (0g‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ) & ⊢ (𝜑 → (𝐹‘ 0 ) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → 0 < (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐴) | ||
Theorem | abvrcl 19521 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring) | ||
Theorem | abvfge0 19522 | An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶(0[,)+∞)) | ||
Theorem | abvf 19523 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ) | ||
Theorem | abvcl 19524 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ) | ||
Theorem | abvge0 19525 | The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝐹‘𝑋)) | ||
Theorem | abveq0 19526 | The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ((𝐹‘𝑋) = 0 ↔ 𝑋 = 0 )) | ||
Theorem | abvne0 19527 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0) | ||
Theorem | abvgt0 19528 | The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 < (𝐹‘𝑋)) | ||
Theorem | abvmul 19529 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌))) | ||
Theorem | abvtri 19530 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abv0 19531 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0) | ||
Theorem | abv1z 19532 | The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → (𝐹‘ 1 ) = 1) | ||
Theorem | abv1 19533 | The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) → (𝐹‘ 1 ) = 1) | ||
Theorem | abvneg 19534 | The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁‘𝑋)) = (𝐹‘𝑋)) | ||
Theorem | abvsubtri 19535 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abvrec 19536 | The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋))) | ||
Theorem | abvdiv 19537 | The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌))) | ||
Theorem | abvdom 19538 | Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝑋 · 𝑌) ≠ 0 ) | ||
Theorem | abvres 19539 | The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐶) & ⊢ 𝐵 = (AbsVal‘𝑆) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹 ↾ 𝐶) ∈ 𝐵) | ||
Theorem | abvtrivd 19540* | The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦 · 𝑧) ≠ 0 ) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐴) | ||
Theorem | abvtriv 19541* | The trivial absolute value. (This theorem is true as long as 𝑅 is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 19538 is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) ⇒ ⊢ (𝑅 ∈ DivRing → 𝐹 ∈ 𝐴) | ||
Theorem | abvpropd 19542* | If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
Syntax | cstf 19543 | Extend class notation with the functionalization of the *-ring involution. |
class *rf | ||
Syntax | csr 19544 | Extend class notation with class of all *-rings. |
class *-Ring | ||
Definition | df-staf 19545* | Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *𝑟 as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ *rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥))) | ||
Definition | df-srng 19546* | Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.) |
⊢ *-Ring = {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)} | ||
Theorem | staffval 19547* | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) | ||
Theorem | stafval 19548 | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴)) | ||
Theorem | staffn 19549 | The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ ( ∗ Fn 𝐵 → ∙ = ∗ ) | ||
Theorem | issrng 19550 | The predicate "is a star ring." (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring ↔ ( ∗ ∈ (𝑅 RingHom 𝑂) ∧ ∗ = ◡ ∗ )) | ||
Theorem | srngrhm 19551 | The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂)) | ||
Theorem | srngring 19552 | A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring) | ||
Theorem | srngcnv 19553 | The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ ) | ||
Theorem | srngf1o 19554 | The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*rf‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ :𝐵–1-1-onto→𝐵) | ||
Theorem | srngcl 19555 | The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵) | ||
Theorem | srngnvl 19556 | The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋) | ||
Theorem | srngadd 19557 | The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌))) | ||
Theorem | srngmul 19558 | The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 · 𝑌)) = (( ∗ ‘𝑌) · ( ∗ ‘𝑋))) | ||
Theorem | srng1 19559 | The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *𝑟 to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd 19561.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 ) | ||
Theorem | srng0 19560 | The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 ) | ||
Theorem | issrngd 19561* | Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝜑 → 𝐾 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → ∗ = (*𝑟‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗ ‘𝑥))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘( ∗ ‘𝑥)) = 𝑥) ⇒ ⊢ (𝜑 → 𝑅 ∈ *-Ring) | ||
Theorem | idsrngd 19562* | A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥) ⇒ ⊢ (𝜑 → 𝑅 ∈ *-Ring) | ||
Syntax | clmod 19563 | Extend class notation with class of all left modules. |
class LMod | ||
Syntax | cscaf 19564 | The functionalization of the scalar multiplication operation. |
class ·sf | ||
Definition | df-lmod 19565* | Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.) |
⊢ LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))} | ||
Definition | df-scaf 19566* | Define the functionalization of the ·𝑠 operator. This restricts the value of ·𝑠 to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦))) | ||
Theorem | islmod 19567* | The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))) | ||
Theorem | lmodlema 19568 | Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑅 · 𝑌) ∈ 𝑉 ∧ (𝑅 · (𝑌 + 𝑋)) = ((𝑅 · 𝑌) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑌) = ((𝑄 · 𝑌) + (𝑅 · 𝑌))) ∧ (((𝑄 × 𝑅) · 𝑌) = (𝑄 · (𝑅 · 𝑌)) ∧ ( 1 · 𝑌) = 𝑌))) | ||
Theorem | islmodd 19569* | Properties that determine a left module. See note in isgrpd2 18061 regarding the 𝜑 on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.) |
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) & ⊢ (𝜑 → + = (+g‘𝑊)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) & ⊢ (𝜑 → ⨣ = (+g‘𝐹)) & ⊢ (𝜑 → × = (.r‘𝐹)) & ⊢ (𝜑 → 1 = (1r‘𝐹)) & ⊢ (𝜑 → 𝐹 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉) → (𝑥 · 𝑦) ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ⨣ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 × 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 1 · 𝑥) = 𝑥) ⇒ ⊢ (𝜑 → 𝑊 ∈ LMod) | ||
Theorem | lmodgrp 19570 | A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | ||
Theorem | lmodring 19571 | The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) | ||
Theorem | lmodfgrp 19572 | The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) | ||
Theorem | lmodbn0 19573 | The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝐵 ≠ ∅) | ||
Theorem | lmodacl 19574 | Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
Theorem | lmodmcl 19575 | Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
Theorem | lmodsn0 19576 | The set of scalars in a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ LMod → 𝐵 ≠ ∅) | ||
Theorem | lmodvacl 19577 | Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) | ||
Theorem | lmodass 19578 | Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | lmodlcan 19579 | Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lmodvscl 19580 | Closure of scalar product for a left module. (hvmulcl 28717 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉) | ||
Theorem | scaffval 19581* | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ (𝑥 · 𝑦)) | ||
Theorem | scafval 19582 | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = (𝑋 · 𝑌)) | ||
Theorem | scafeq 19583 | If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ( · Fn (𝐾 × 𝐵) → ∙ = · ) | ||
Theorem | scaffn 19584 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) ⇒ ⊢ ∙ Fn (𝐾 × 𝐵) | ||
Theorem | lmodscaf 19585 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → ∙ :(𝐾 × 𝐵)⟶𝐵) | ||
Theorem | lmodvsdi 19586 | Distributive law for scalar product (left-distributivity). (ax-hvdistr1 28712 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) | ||
Theorem | lmodvsdir 19587 | Distributive law for scalar product (right-distributivity). (ax-hvdistr1 28712 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
Theorem | lmodvsass 19588 | Associative law for scalar product. (ax-hvmulass 28711 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
Theorem | lmod0cl 19589 | The ring zero in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾) | ||
Theorem | lmod1cl 19590 | The ring unit in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ (𝑊 ∈ LMod → 1 ∈ 𝐾) | ||
Theorem | lmodvs1 19591 | Scalar product with ring unit. (ax-hvmulid 28710 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) | ||
Theorem | lmod0vcl 19592 | The zero vector is a vector. (ax-hv0cl 28707 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉) | ||
Theorem | lmod0vlid 19593 | Left identity law for the zero vector. (hvaddid2 28727 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | lmod0vrid 19594 | Right identity law for the zero vector. (ax-hvaddid 28708 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | lmod0vid 19595 | Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋)) | ||
Theorem | lmod0vs 19596 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 28714 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) | ||
Theorem | lmodvs0 19597 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 28728 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 ) | ||
Theorem | lmodvsmmulgdi 19598 | Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ 𝐸 = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋)) | ||
Theorem | lmodfopnelem1 19599 | Lemma 1 for lmodfopne 19601. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾) | ||
Theorem | lmodfopnelem2 19600 | Lemma 2 for lmodfopne 19601. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |