![]() |
Metamath
Proof Explorer Theorem List (p. 205 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lssn0 20401 | A subspace is not empty. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑈 ≠ ∅) | ||
Theorem | 00lss 20402 | The empty structure has no subspaces (for use with fvco4i 6942). (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ ∅ = (LSubSp‘∅) | ||
Theorem | lsscl 20403 | Closure property of a subspace. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 8-Jan-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑈 ∈ 𝑆 ∧ (𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → ((𝑍 · 𝑋) + 𝑌) ∈ 𝑈) | ||
Theorem | lssvsubcl 20404 | 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 20405 | 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 20597. Can it be used along with lspsnne1 20578, lspsnne2 20579 to shorten this proof? (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝑋 + 𝑌) ∈ 𝑈) | ||
Theorem | lssvancl2 20406 | 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 20407 | 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 20408 | 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 20409 | The zero subspace is included in every subspace. (sh0le 30382 analog.) (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ 𝑋) | ||
Theorem | lssle0 20410 | No subspace is smaller than the zero subspace. (shle0 30384 analog.) (Contributed by NM, 20-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑆) → (𝑋 ⊆ { 0 } ↔ 𝑋 = { 0 })) | ||
Theorem | lssne0 20411* | A nonzero subspace has a nonzero vector. (shne0i 30390 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 8-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑋 ∈ 𝑆 → (𝑋 ≠ { 0 } ↔ ∃𝑦 ∈ 𝑋 𝑦 ≠ 0 )) | ||
Theorem | lssvneln0 20412 | 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 20413 | 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 20414* | Conclude subspace ordering from nonzero vector membership. (ssrdv 3950 analog.) (Contributed by NM, 17-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ⊆ 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑉 ∖ { 0 })) → (𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ 𝑈) | ||
Theorem | lssvacl 20415 | 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 20416 | 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 20417 | Closure of negative vectors in a subspace. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈) | ||
Theorem | lsssubg 20418 | All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) | ||
Theorem | lsssssubg 20419 | All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊)) | ||
Theorem | islss3 20420 | 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 20421 | A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) | ||
Theorem | lsslss 20422 | The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑇 = (LSubSp‘𝑋) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑉 ∈ 𝑇 ↔ (𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈))) | ||
Theorem | islss4 20423* | 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 20424* | 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 20425 | 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 20426 | 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 20427 | 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 20428 | Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵)) | ||
Theorem | prdsvscacl 20429* | 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 20430* | 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 20431 | A structure power of a left module is a left module. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ LMod) | ||
Syntax | clspn 20432 | Extend class notation with span of a set of vectors. |
class LSpan | ||
Definition | df-lsp 20433* | 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 20434* | The span function for a left vector space (or a left module). (df-span 30251 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝑁 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡})) | ||
Theorem | lspf 20435 | 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 20436* | The span of a set of vectors (in a left module). (spanval 30275 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ 𝑆 ∣ 𝑈 ⊆ 𝑡}) | ||
Theorem | lspcl 20437 | The span of a set of vectors is a subspace. (spancl 30278 analog.) (Contributed by NM, 9-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) ∈ 𝑆) | ||
Theorem | lspsncl 20438 | The span of a singleton is a subspace (frequently used special case of lspcl 20437). (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) | ||
Theorem | lspprcl 20439 | The span of a pair is a subspace (frequently used special case of lspcl 20437). (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ 𝑆) | ||
Theorem | lsptpcl 20440 | The span of an unordered triple is a subspace (frequently used special case of lspcl 20437). (Contributed by NM, 22-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌, 𝑍}) ∈ 𝑆) | ||
Theorem | lspsnsubg 20441 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 20437). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) | ||
Theorem | 00lsp 20442 | fvco4i 6942 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ∅ = (LSpan‘∅) | ||
Theorem | lspid 20443 | The span of a subspace is itself. (spanid 30289 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈) | ||
Theorem | lspssv 20444 | 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 20445 | Span preserves subset ordering. (spanss 30290 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈)) | ||
Theorem | lspssid 20446 | A set of vectors is a subset of its span. (spanss2 30287 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝑁‘𝑈)) | ||
Theorem | lspidm 20447 | 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 20448 | 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 20449 | 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 20450 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹) | ||
Theorem | lspsnss 20451 | The span of the singleton of a subspace member is included in the subspace. (spansnss 30513 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈) | ||
Theorem | lspsnel3 20452 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 30514 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑈) | ||
Theorem | lspprss 20453 | 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 20454 | A vector belongs to the span of its singleton. (spansnid 30505 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) | ||
Theorem | lspsnel6 20455 | 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 20456 | 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 20457 | 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 20458 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspprid2 20459 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspprvacl 20460 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lssats2 20461* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 (𝑁‘{𝑥})) | ||
Theorem | lspsneli 20462 | A scalar product with a vector belongs to the span of its singleton. (spansnmul 30506 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 · 𝑋) ∈ (𝑁‘{𝑋})) | ||
Theorem | lspsn 20463* | Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) | ||
Theorem | lspsnel 20464* | Member of span of the singleton of a vector. (elspansn 30508 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑈 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ 𝐾 𝑈 = (𝑘 · 𝑋))) | ||
Theorem | lspsnvsi 20465 | Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) ⊆ (𝑁‘{𝑋})) | ||
Theorem | lspsnss2 20466* | Comparable spans of singletons must have proportional vectors. See lspsneq 20583 for equal span version. (Contributed by NM, 7-Jun-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ 𝐾 𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsnneg 20467 | Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑀 = (invg‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑀‘𝑋)}) = (𝑁‘{𝑋})) | ||
Theorem | lspsnsub 20468 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) = (𝑁‘{(𝑌 − 𝑋)})) | ||
Theorem | lspsn0 20469 | Span of the singleton of the zero vector. (spansn0 30483 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑁‘{ 0 }) = { 0 }) | ||
Theorem | lsp0 20470 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0 }) | ||
Theorem | lspuni0 20471 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 ) | ||
Theorem | lspun0 20472 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋)) | ||
Theorem | lspsneq0 20473 | Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑁‘{𝑋}) = { 0 } ↔ 𝑋 = 0 )) | ||
Theorem | lspsneq0b 20474 | Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 = 0 ↔ 𝑌 = 0 )) | ||
Theorem | lmodindp1 20475 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) | ||
Theorem | lsslsp 20476 | Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap 𝑀‘𝐺 and 𝑁‘𝐺 since we are computing a property of 𝑁‘𝐺? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015. |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑀 = (LSpan‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑋) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑀‘𝐺) = (𝑁‘𝐺)) | ||
Theorem | lss0v 20477 | The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑍 = (0g‘𝑋) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) → 𝑍 = 0 ) | ||
Theorem | lsspropd 20478* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) ⇒ ⊢ (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿)) | ||
Theorem | lsppropd 20479* | If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐿 ∈ 𝑌) ⇒ ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿)) | ||
Syntax | clmhm 20480 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 20481 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 20482 | The class of the left module isomorphism relation. |
class ≃𝑚 | ||
Definition | df-lmhm 20483* | A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))}) | ||
Definition | df-lmim 20484* | An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ LMIso = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}) | ||
Definition | df-lmic 20485 | Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ≃𝑚 = (◡ LMIso “ (V ∖ 1o)) | ||
Theorem | reldmlmhm 20486 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ Rel dom LMHom | ||
Theorem | lmimfn 20487 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ LMIso Fn (LMod × LMod) | ||
Theorem | islmhm 20488* | Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))))) | ||
Theorem | islmhm3 20489* | Property of a module homomorphism, similar to ismhm 18603. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))))) | ||
Theorem | lmhmlem 20490 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾))) | ||
Theorem | lmhmsca 20491 | A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾) | ||
Theorem | lmghm 20492 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | lmhmlmod2 20493 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | ||
Theorem | lmhmlmod1 20494 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | ||
Theorem | lmhmf 20495 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | lmhmlin 20496 | A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌))) | ||
Theorem | lmodvsinv 20497 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | lmodvsinv2 20498 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | islmhm2 20499* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20393. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐸 = (Base‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧))))) | ||
Theorem | islmhmd 20500* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐽 = (Scalar‘𝑇) & ⊢ 𝑁 = (Base‘𝐾) & ⊢ (𝜑 → 𝑆 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐽 = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |