Home | Metamath
Proof Explorer Theorem List (p. 197 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmodfopnelem1 19601 | Lemma 1 for lmodfopne 19603. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾) | ||
Theorem | lmodfopnelem2 19602 | Lemma 2 for lmodfopne 19603. (Contributed by AV, 2-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝑊 ∈ LMod ∧ + = · ) → ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉)) | ||
Theorem | lmodfopne 19603 | 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 19604 | A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺:𝐼⟶𝐾) & ⊢ (𝜑 → 𝐻:𝐼⟶𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐺 ∘f · 𝐻):𝐼⟶𝐵) | ||
Theorem | lcomfsupp 19605 | 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 19606 | Closure of vector negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) ∈ 𝑉) | ||
Theorem | lmodvnegid 19607 | 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 19608 | 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 19609 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑁‘(𝑅 · 𝑋)) = ((𝑀‘𝑅) · 𝑋)) | ||
Theorem | lmodvsubcl 19610 | Closure of vector subtraction. (hvsubcl 28722 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) | ||
Theorem | lmodcom 19611 | Left module vector sum is commutative. (Contributed by Gérard Lang, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | lmodabl 19612 | 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 19613 | A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015.) |
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) | ||
Theorem | lmodnegadd 19614 | Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘((𝐴 · 𝑋) + (𝐵 · 𝑌))) = (((𝐼‘𝐴) · 𝑋) + ((𝐼‘𝐵) · 𝑌))) | ||
Theorem | lmod4 19615 | 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 19616 | Relationship between vector subtraction and addition. (hvsubadd 28782 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | lmodvaddsub4 19617 | Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | lmodvpncan 19618 | Addition/subtraction cancellation law for vectors. (hvpncan 28744 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | lmodvnpcan 19619 | 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 19620 | Value of vector subtraction in terms of addition. (hvsubval 28721 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 19621 | Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (invg‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 − (𝐴 · 𝑌)) = (𝑋 + ((𝑁‘𝐴) · 𝑌))) | ||
Theorem | lmodsubdi 19622 | Scalar multiplication distributive law for subtraction. (hvsubdistr1 28754 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 · (𝑋 − 𝑌)) = ((𝐴 · 𝑋) − (𝐴 · 𝑌))) | ||
Theorem | lmodsubdir 19623 | Scalar multiplication distributive law for subtraction. (hvsubdistr2 28755 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴𝑆𝐵) · 𝑋) = ((𝐴 · 𝑋) − (𝐵 · 𝑋))) | ||
Theorem | lmodsubeq0 19624 | If the difference between two vectors is zero, they are equal. (hvsubeq0 28773 analog.) (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | lmodsubid 19625 | Subtraction of a vector from itself. (hvsubid 28731 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉) → (𝐴 − 𝐴) = 0 ) | ||
Theorem | lmodvsghm 19626* | 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 19627* | If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd 19628 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 19628* | 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 19629* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc2 19288, 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 19630* | 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 19631* | A function mapping to a scalar product in which one factor is finitely supported is finitely supported. Formerly part of proof for ply1coe 20394. (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 19632* | Lemma for rmodislmod 19633. This is the part of the proof of rmodislmod 19633 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 19633* | 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 19567 of a left module, see also islmod 19569. (Contributed by AV, 3-Dec-2021.) |
⊢ 𝑉 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ⨣ = (+g‘𝐹) & ⊢ × = (.r‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 ⨣ 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) & ⊢ ∗ = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 · 𝑠)) & ⊢ 𝐿 = (𝑅 sSet 〈( ·𝑠 ‘ndx), ∗ 〉) ⇒ ⊢ (𝐹 ∈ CRing → 𝐿 ∈ LMod) | ||
Syntax | clss 19634 | Extend class notation with linear subspaces of a left module or left vector space. |
class LSubSp | ||
Definition | df-lss 19635* | 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 19636* | 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 19637* | 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 19638* | 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‘𝑊)) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑈 ≠ ∅) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | lssss 19639 | A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) | ||
Theorem | lssel 19640 | A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑉) | ||
Theorem | lss1 19641 | The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝑆) | ||
Theorem | lssuni 19642 | The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → ∪ 𝑆 = 𝑉) | ||
Theorem | lssn0 19643 | A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑈 ≠ ∅) | ||
Theorem | 00lss 19644 | The empty structure has no subspaces (for use with fvco4i 6756). (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ∅ = (LSubSp‘∅) | ||
Theorem | lsscl 19645 | Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑈 ∈ 𝑆 ∧ (𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → ((𝑍 · 𝑋) + 𝑌) ∈ 𝑈) | ||
Theorem | lssvsubcl 19646 | Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) ∈ 𝑈) | ||
Theorem | lssvancl1 19647 | Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. TODO: notice similarity to lspindp3 19839. Can it be used along with lspsnne1 19820, lspsnne2 19821 to shorten this proof? (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝑋 + 𝑌) ∈ 𝑈) | ||
Theorem | lssvancl2 19648 | Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝑌 + 𝑋) ∈ 𝑈) | ||
Theorem | lss0cl 19649 | The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 0 ∈ 𝑈) | ||
Theorem | lsssn0 19650 | The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → { 0 } ∈ 𝑆) | ||
Theorem | lss0ss 19651 | The zero subspace is included in every subspace. (sh0le 29145 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ 𝑋) | ||
Theorem | lssle0 19652 | No subspace is smaller than the zero subspace. (shle0 29147 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 })) | ||
Theorem | lssne0 19653* | A nonzero subspace has a nonzero vector. (shne0i 29153 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝑆 → (𝑋 ≠ { 0 } ↔ ∃𝑦 ∈ 𝑋 𝑦 ≠ 0 )) | ||
Theorem | lssvneln0 19654 | A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 19-Jul-2022.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑋 ≠ 0 ) | ||
Theorem | lssneln0 19655 | A vector 𝑋 which doesn't belong to a subspace 𝑈 is nonzero. (Contributed by NM, 14-May-2015.) (Revised by AV, 17-Jul-2022.) (Proof shortened by AV, 19-Jul-2022.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | ||
Theorem | lssssr 19656* | Conclude subspace ordering from nonzero vector membership. (ssrdv 3972 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ⊆ 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ 𝑈) | ||
Theorem | lssvacl 19657 | Closure of vector addition in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ + = (+g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈) | ||
Theorem | lssvscl 19658 | Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈)) → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | lssvnegcl 19659 | Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈) | ||
Theorem | lsssubg 19660 | All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) | ||
Theorem | lsssssubg 19661 | All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊)) | ||
Theorem | islss3 19662 | A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod))) | ||
Theorem | lsslmod 19663 | A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) | ||
Theorem | lsslss 19664 | The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑇 = (LSubSp‘𝑋) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈))) | ||
Theorem | islss4 19665* | A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ∈ (SubGrp‘𝑊) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝑈 (𝑎 · 𝑏) ∈ 𝑈))) | ||
Theorem | lss1d 19666* | One-dimensional subspace (or zero-dimensional if 𝑋 is the zero vector). (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆) | ||
Theorem | lssintcl 19667 | The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑆) | ||
Theorem | lssincl 19668 | The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ∩ 𝑈) ∈ 𝑆) | ||
Theorem | lssmre 19669 | The subspaces of a module comprise a Moore system on the vectors of the module. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (Moore‘𝐵)) | ||
Theorem | lssacs 19670 | Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵)) | ||
Theorem | prdsvscacl 19671* | Pointwise scalar multiplication is closed in products of modules. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶LMod) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (Scalar‘(𝑅‘𝑥)) = 𝑆) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) | ||
Theorem | prdslmodd 19672* | The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶LMod) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) ⇒ ⊢ (𝜑 → 𝑌 ∈ LMod) | ||
Theorem | pwslmod 19673 | The product of a family of left modules is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ LMod) | ||
Syntax | clspn 19674 | Extend class notation with span of a set of vectors. |
class LSpan | ||
Definition | df-lsp 19675* | Define span of a set of vectors of a left module or left vector space. (Contributed by NM, 8-Dec-2013.) |
⊢ LSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (LSubSp‘𝑤) ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | lspfval 19676* | The span function for a left vector space (or a left module). (df-span 29014 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | lspf 19677 | The span operator on a left module maps subsets to subsets. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑁:𝒫 𝑉⟶𝑆) | ||
Theorem | lspval 19678* | The span of a set of vectors (in a left module). (spanval 29038 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ 𝑆 ∣ 𝑈 ⊆ 𝑡}) | ||
Theorem | lspcl 19679 | The span of a set of vectors is a subspace. (spancl 29041 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ∈ 𝑆) | ||
Theorem | lspsncl 19680 | The span of a singleton is a subspace (frequently used special case of lspcl 19679). (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) | ||
Theorem | lspprcl 19681 | The span of a pair is a subspace (frequently used special case of lspcl 19679). (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆) | ||
Theorem | lsptpcl 19682 | The span of an unordered triple is a subspace (frequently used special case of lspcl 19679). (Contributed by NM, 22-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌, 𝑍}) ∈ 𝑆) | ||
Theorem | lspsnsubg 19683 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 19679). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) | ||
Theorem | 00lsp 19684 | fvco4i 6756 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ∅ = (LSpan‘∅) | ||
Theorem | lspid 19685 | The span of a subspace is itself. (spanid 29052 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈) | ||
Theorem | lspssv 19686 | A span is a set of vectors. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ⊆ 𝑉) | ||
Theorem | lspss 19687 | Span preserves subset ordering. (spanss 29053 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈)) | ||
Theorem | lspssid 19688 | A set of vectors is a subset of its span. (spanss2 29050 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝑁‘𝑈)) | ||
Theorem | lspidm 19689 | The span of a set of vectors is idempotent. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈)) | ||
Theorem | lspun 19690 | The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉) → (𝑁‘(𝑇 ∪ 𝑈)) = (𝑁‘((𝑁‘𝑇) ∪ (𝑁‘𝑈)))) | ||
Theorem | lspssp 19691 | If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ 𝑈) | ||
Theorem | mrclsp 19692 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹) | ||
Theorem | lspsnss 19693 | The span of the singleton of a subspace member is included in the subspace. (spansnss 29276 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈) | ||
Theorem | lspsnel3 19694 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 29277 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑈) | ||
Theorem | lspprss 19695 | The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈) | ||
Theorem | lspsnid 19696 | A vector belongs to the span of its singleton. (spansnid 29268 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) | ||
Theorem | lspsnel6 19697 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ 𝑈))) | ||
Theorem | lspsnel5 19698 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑁‘{𝑋}) ⊆ 𝑈)) | ||
Theorem | lspsnel5a 19699 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑈) | ||
Theorem | lspprid1 19700 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |