![]() |
Metamath
Proof Explorer Theorem List (p. 197 of 454) | < 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: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | abvdiv 19601 | The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 )) → (𝐹‘(𝑋 / 𝑌)) = ((𝐹‘𝑋) / (𝐹‘𝑌))) | ||
Theorem | abvdom 19602 | 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 19603 | 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 19604* | 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 19605* | 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 19602 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 19606* | 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 19607 | Extend class notation with the functionalization of the *-ring involution. |
class *rf | ||
Syntax | csr 19608 | Extend class notation with class of all *-rings. |
class *-Ring | ||
Definition | df-staf 19609* | 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 19610* | 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 19611* | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ ∙ = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) | ||
Theorem | stafval 19612 | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ∗ = (*𝑟‘𝑅) & ⊢ ∙ = (*rf‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝐵 → ( ∙ ‘𝐴) = ( ∗ ‘𝐴)) | ||
Theorem | staffn 19613 | 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 19614 | 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 19615 | The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ ∈ (𝑅 RingHom 𝑂)) | ||
Theorem | srngring 19616 | A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ (𝑅 ∈ *-Ring → 𝑅 ∈ Ring) | ||
Theorem | srngcnv 19617 | The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*rf‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ∗ = ◡ ∗ ) | ||
Theorem | srngf1o 19618 | 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 19619 | The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘𝑋) ∈ 𝐵) | ||
Theorem | srngnvl 19620 | The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵) → ( ∗ ‘( ∗ ‘𝑋)) = 𝑋) | ||
Theorem | srngadd 19621 | The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ∗ ‘(𝑋 + 𝑌)) = (( ∗ ‘𝑋) + ( ∗ ‘𝑌))) | ||
Theorem | srngmul 19622 | 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 19623 | 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 19625.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 ) | ||
Theorem | srng0 19624 | The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ ∗ = (*𝑟‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 ) | ||
Theorem | issrngd 19625* | 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 19626* | 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 19627 | Extend class notation with class of all left modules. |
class LMod | ||
Syntax | cscaf 19628 | The functionalization of the scalar multiplication operation. |
class ·sf | ||
Definition | df-lmod 19629* | 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 19630* | 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 19631* | 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 19632 | 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 19633* | Properties that determine a left module. See note in isgrpd2 18115 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 19634 | A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | ||
Theorem | lmodring 19635 | 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 19636 | 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 19637 | 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 19638 | 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 19639 | 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 19640 | 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 19641 | 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 19642 | Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | lmodlcan 19643 | Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lmodvscl 19644 | Closure of scalar product for a left module. (hvmulcl 28796 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉) | ||
Theorem | scaffval 19645* | 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 19646 | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = (𝑋 · 𝑌)) | ||
Theorem | scafeq 19647 | 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 19648 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) ⇒ ⊢ ∙ Fn (𝐾 × 𝐵) | ||
Theorem | lmodscaf 19649 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ∙ = ( ·sf ‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → ∙ :(𝐾 × 𝐵)⟶𝐵) | ||
Theorem | lmodvsdi 19650 | Distributive law for scalar product (left-distributivity). (ax-hvdistr1 28791 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) | ||
Theorem | lmodvsdir 19651 | Distributive law for scalar product (right-distributivity). (ax-hvdistr1 28791 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
Theorem | lmodvsass 19652 | Associative law for scalar product. (ax-hvmulass 28790 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ × = (.r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
Theorem | lmod0cl 19653 | 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 19654 | 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 19655 | Scalar product with ring unit. (ax-hvmulid 28789 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) | ||
Theorem | lmod0vcl 19656 | The zero vector is a vector. (ax-hv0cl 28786 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉) | ||
Theorem | lmod0vlid 19657 | Left identity law for the zero vector. (hvaddid2 28806 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | lmod0vrid 19658 | Right identity law for the zero vector. (ax-hvaddid 28787 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | lmod0vid 19659 | 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 19660 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 28793 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑂 · 𝑋) = 0 ) | ||
Theorem | lmodvs0 19661 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 28807 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾) → (𝑋 · 0 ) = 0 ) | ||
Theorem | lmodvsmmulgdi 19662 | 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 19663 | Lemma 1 for lmodfopne 19665. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾) | ||
Theorem | lmodfopnelem2 19664 | Lemma 2 for lmodfopne 19665. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉)) | ||
Theorem | lmodfopne 19665 | The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 1 ≠ 0 ) → + ≠ · ) | ||
Theorem | lcomf 19666 | A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐾) & ⊢ (𝜑 → 𝐻:𝐼⟶𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐺 ∘f · 𝐻):𝐼⟶𝐵) | ||
Theorem | lcomfsupp 19667 | A linear-combination sum is finitely supported if the coefficients are. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by AV, 15-Jul-2019.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐾) & ⊢ (𝜑 → 𝐻:𝐼⟶𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (0g‘𝐹) & ⊢ (𝜑 → 𝐺 finSupp 𝑌) ⇒ ⊢ (𝜑 → (𝐺 ∘f · 𝐻) finSupp 0 ) | ||
Theorem | lmodvnegcl 19668 | Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ 𝑉) | ||
Theorem | lmodvnegid 19669 | Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 ) | ||
Theorem | lmodvneg1 19670 | Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 1 = (1r‘𝐹) & ⊢ 𝑀 = (invg‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑀‘ 1 ) · 𝑋) = (𝑁‘𝑋)) | ||
Theorem | lmodvsneg 19671 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = ((𝑀‘𝑅) · 𝑋)) | ||
Theorem | lmodvsubcl 19672 | Closure of vector subtraction. (hvsubcl 28800 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) | ||
Theorem | lmodcom 19673 | Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | lmodabl 19674 | A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) | ||
Theorem | lmodcmn 19675 | A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) | ||
Theorem | lmodnegadd 19676 | Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘((𝐴 · 𝑋) + (𝐵 · 𝑌))) = (((𝐼‘𝐴) · 𝑋) + ((𝐼‘𝐵) · 𝑌))) | ||
Theorem | lmod4 19677 | Commutative/associative law for left module vector sum. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝑍 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉)) → ((𝑋 + 𝑌) + (𝑍 + 𝑈)) = ((𝑋 + 𝑍) + (𝑌 + 𝑈))) | ||
Theorem | lmodvsubadd 19678 | Relationship between vector subtraction and addition. (hvsubadd 28860 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | lmodvaddsub4 19679 | Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | lmodvpncan 19680 | Addition/subtraction cancellation law for vectors. (hvpncan 28822 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | lmodvnpcan 19681 | Cancellation law for vector subtraction (npcan 10884 analog). (Contributed by NM, 19-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | lmodvsubval2 19682 | Value of vector subtraction in terms of addition. (hvsubval 28799 analog.) (Contributed by NM, 31-Mar-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝐹) & ⊢ 1 = (1r‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) = (𝐴 + ((𝑁‘ 1 ) · 𝐵))) | ||
Theorem | lmodsubvs 19683 | Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (invg‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 − (𝐴 · 𝑌)) = (𝑋 + ((𝑁‘𝐴) · 𝑌))) | ||
Theorem | lmodsubdi 19684 | Scalar multiplication distributive law for subtraction. (hvsubdistr1 28832 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 · (𝑋 − 𝑌)) = ((𝐴 · 𝑋) − (𝐴 · 𝑌))) | ||
Theorem | lmodsubdir 19685 | Scalar multiplication distributive law for subtraction. (hvsubdistr2 28833 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴𝑆𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋))) | ||
Theorem | lmodsubeq0 19686 | If the difference between two vectors is zero, they are equal. (hvsubeq0 28851 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | lmodsubid 19687 | Subtraction of a vector from itself. (hvsubid 28809 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉) → (𝐴 − 𝐴) = 0 ) | ||
Theorem | lmodvsghm 19688* | Scalar multiplication of the vector space by a fixed scalar is an endomorphism of the additive group of vectors. (Contributed by Mario Carneiro, 5-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)) ∈ (𝑊 GrpHom 𝑊)) | ||
Theorem | lmodprop2d 19689* | If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 19690 also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(.r‘𝐹)𝑦) = (𝑥(.r‘𝐺)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod)) | ||
Theorem | lmodpropd 19690* | If two structures have the same components (properties), one is a left module iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 27-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿)) & ⊢ 𝑃 = (Base‘𝐹) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ LMod ↔ 𝐿 ∈ LMod)) | ||
Theorem | gsumvsmul 19691* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 19353, since every ring is a left module over itself. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) (Revised by AV, 10-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑌) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (𝑋 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑌)))) | ||
Theorem | mptscmfsupp0 19692* | A mapping to a scalar product is finitely supported if the mapping to the scalar is finitely supported. (Contributed by AV, 5-Oct-2019.) |
⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ∈ LMod) & ⊢ (𝜑 → 𝑅 = (Scalar‘𝑄)) & ⊢ 𝐾 = (Base‘𝑄) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑆 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑊 ∈ 𝐾) & ⊢ 0 = (0g‘𝑄) & ⊢ 𝑍 = (0g‘𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ 𝑆) finSupp 𝑍) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ (𝑆 ∗ 𝑊)) finSupp 0 ) | ||
Theorem | mptscmfsuppd 19693* | A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe 20925. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 8-Aug-2019.) (Proof shortened by AV, 18-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑆 = (Scalar‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑃 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐴:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 finSupp (0g‘𝑆)) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) · 𝑍)) finSupp (0g‘𝑃)) | ||
Theorem | rmodislmodlem 19694* | Lemma for rmodislmod 19695. This is the part of the proof of rmodislmod 19695 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.) |
⊢ 𝑉 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) & ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)) & ⊢ 𝐿 = (𝑅 sSet 〈( ·𝑠 ‘ndx), ∗ 〉) ⇒ ⊢ ((𝐹 ∈ CRing ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 × 𝑏) ∗ 𝑐) = (𝑎 ∗ (𝑏 ∗ 𝑐))) | ||
Theorem | rmodislmod 19695* | The right module 𝑅 induces a left module 𝐿 by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to the definition df-lmod 19629 of a left module, see also islmod 19631. (Contributed by AV, 3-Dec-2021.) |
⊢ 𝑉 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) & ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)) & ⊢ 𝐿 = (𝑅 sSet 〈( ·𝑠 ‘ndx), ∗ 〉) ⇒ ⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod) | ||
Syntax | clss 19696 | Extend class notation with linear subspaces of a left module or left vector space. |
class LSubSp | ||
Definition | df-lss 19697* | Define the set of linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) |
⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠}) | ||
Theorem | lssset 19698* | The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 15-Jul-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠}) | ||
Theorem | islss 19699* | The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) | ||
Theorem | islssd 19700* | Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑊)) & ⊢ (𝜑 → + = (+g‘𝑊)) & ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊)) & ⊢ (𝜑 → 𝑆 = (LSubSp‘𝑊)) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑈 ≠ ∅) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |