Home | Metamath
Proof Explorer Theorem List (p. 187 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-subrg 18601* |
Define a subring of a ring as a set of elements that is a ring in its
own right and contains the multiplicative identity.
The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is component-wise) contains the false identity 〈1, 0〉 which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ SubRing = (𝑤 ∈ Ring ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ((𝑤 ↾s 𝑠) ∈ Ring ∧ (1r‘𝑤) ∈ 𝑠)}) | ||
Definition | df-rgspn 18602* | The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | issubrg 18603 | The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) | ||
Theorem | subrgss 18604 | A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) | ||
Theorem | subrgid 18605 | Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgring 18606 | A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) | ||
Theorem | subrgcrng 18607 | A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → 𝑆 ∈ CRing) | ||
Theorem | subrgrcl 18608 | Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | ||
Theorem | subrgsubg 18609 | A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) | ||
Theorem | subrg0 18610 | A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 0 = (0g‘𝑆)) | ||
Theorem | subrg1cl 18611 | A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴) | ||
Theorem | subrgbas 18612 | Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) | ||
Theorem | subrg1 18613 | A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 = (1r‘𝑆)) | ||
Theorem | subrgacl 18614 | A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 + 𝑌) ∈ 𝐴) | ||
Theorem | subrgmcl 18615 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 · 𝑌) ∈ 𝐴) | ||
Theorem | subrgsubm 18616 | A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubMnd‘𝑀)) | ||
Theorem | subrgdvds 18617 | If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∥ = (∥r‘𝑅) & ⊢ 𝐸 = (∥r‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ ) | ||
Theorem | subrguss 18618 | A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈) | ||
Theorem | subrginv 18619 | A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐽 = (invr‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) | ||
Theorem | subrgdv 18620 | A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ / = (/r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝐸 = (/r‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌)) | ||
Theorem | subrgunit 18621 | An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ (𝐼‘𝑋) ∈ 𝐴))) | ||
Theorem | subrgugrp 18622 | The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑉 = (Unit‘𝑆) & ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ∈ (SubGrp‘𝐺)) | ||
Theorem | issubrg2 18623* | Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))) | ||
Theorem | opprsubrg 18624 | Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (SubRing‘𝑅) = (SubRing‘𝑂) | ||
Theorem | subrgint 18625 | The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubRing‘𝑅)) | ||
Theorem | subrgin 18626 | The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑅)) → (𝐴 ∩ 𝐵) ∈ (SubRing‘𝑅)) | ||
Theorem | subrgmre 18627 | The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (SubRing‘𝑅) ∈ (Moore‘𝐵)) | ||
Theorem | issubdrg 18628* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐴 ∈ (SubRing‘𝑅)) → (𝑆 ∈ DivRing ↔ ∀𝑥 ∈ (𝐴 ∖ { 0 })(𝐼‘𝑥) ∈ 𝐴)) | ||
Theorem | subsubrg 18629 | A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | subsubrg2 18630 | The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubRing‘𝑅) → (SubRing‘𝑆) = ((SubRing‘𝑅) ∩ 𝒫 𝐴)) | ||
Theorem | issubrg3 18631 | A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ 𝑆 ∈ (SubMnd‘𝑀)))) | ||
Theorem | resrhm 18632 | Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝑋 ∈ (SubRing‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 RingHom 𝑇)) | ||
Theorem | rhmeql 18633 | The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑆 RingHom 𝑇) ∧ 𝐺 ∈ (𝑆 RingHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubRing‘𝑆)) | ||
Theorem | rhmima 18634 | The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRing‘𝑁)) | ||
Theorem | cntzsubr 18635 | Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubRing‘𝑅)) | ||
Theorem | pwsdiagrhm 18636* | Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 RingHom 𝑌)) | ||
Theorem | subrgpropd 18637* | If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (SubRing‘𝐾) = (SubRing‘𝐿)) | ||
Theorem | rhmpropd 18638* | Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐽)𝑦) = (𝑥(.r‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀)) | ||
Syntax | cabv 18639 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 18640* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 13824 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) | ||
Theorem | abvfval 18641* | Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐴 = {𝑓 ∈ ((0[,)+∞) ↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) | ||
Theorem | isabv 18642* | 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 18643* | 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 18644 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring) | ||
Theorem | abvfge0 18645 | 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 18646 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → 𝐹:𝐵⟶ℝ) | ||
Theorem | abvcl 18647 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ ℝ) | ||
Theorem | abvge0 18648 | The absolute value of a number is greater or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝐹‘𝑋)) | ||
Theorem | abveq0 18649 | 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 18650 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐹‘𝑋) ≠ 0) | ||
Theorem | abvgt0 18651 | 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 18652 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) · (𝐹‘𝑌))) | ||
Theorem | abvtri 18653 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abv0 18654 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → (𝐹‘ 0 ) = 0) | ||
Theorem | abv1z 18655 | 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 18656 | 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 18657 | 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 18658 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 − 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) | ||
Theorem | abvrec 18659 | The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 )) → (𝐹‘(𝐼‘𝑋)) = (1 / (𝐹‘𝑋))) | ||
Theorem | abvdiv 18660 | The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌))) | ||
Theorem | abvdom 18661 | 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 18662 | 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 18663* | 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 18664* | 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 18661 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 18665* | 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 18666 | Extend class notation with the functionalization of the *-ring involution. |
class *rf | ||
Syntax | csr 18667 | Extend class notation with class of all *-rings. |
class *-Ring | ||
Definition | df-staf 18668* | 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 18669* | 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 18670* | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) | ||
Theorem | stafval 18671 | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴)) | ||
Theorem | staffn 18672 | 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 18673 | 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 18674 | The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂)) | ||
Theorem | srngring 18675 | A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring) | ||
Theorem | srngcnv 18676 | The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ ) | ||
Theorem | srngf1o 18677 | 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 18678 | The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵) | ||
Theorem | srngnvl 18679 | The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋) | ||
Theorem | srngadd 18680 | The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌))) | ||
Theorem | srngmul 18681 | 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 18682 | 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 18684.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 ) | ||
Theorem | srng0 18683 | The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 ) | ||
Theorem | issrngd 18684* | 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 18685* | 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 18686 | Extend class notation with class of all left modules. |
class LMod | ||
Syntax | cscaf 18687 | The functionalization of the scalar multiplication operation. |
class ·sf | ||
Definition | df-lmod 18688* | 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 18689* | 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 18690* | 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 18691 | 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 18692* | Properties that determine a left module. See note in isgrpd2 17265 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 18693 | A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | ||
Theorem | lmodring 18694 | 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 18695 | 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 18696 | 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 18697 | 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 18698 | 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 18699 | 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 18700 | Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |