Home | Metamath
Proof Explorer Theorem List (p. 189 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 | ||
Theorem | lspsnsubg 18801 | The span of a singleton is an additive subgroup (frequently used special case of lspcl 18797). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) | ||
Theorem | 00lsp 18802 | fvco4i 6186 lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ ∅ = (LSpan‘∅) | ||
Theorem | lspid 18803 | The span of a subspace is itself. (spanid 27590 analog.) (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈) | ||
Theorem | lspssv 18804 | 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 18805 | Span preserves subset ordering. (spanss 27591 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈)) | ||
Theorem | lspssid 18806 | A set of vectors is a subset of its span. (spanss2 27588 analog.) (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 ⊆ (𝑁‘𝑈)) | ||
Theorem | lspidm 18807 | 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 18808 | 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 18809 | 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 18810 | Moore closure generalizes module span. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ 𝐾 = (LSpan‘𝑊) & ⊢ 𝐹 = (mrCls‘𝑈) ⇒ ⊢ (𝑊 ∈ LMod → 𝐾 = 𝐹) | ||
Theorem | lspsnss 18811 | The span of the singleton of a subspace member is included in the subspace. (spansnss 27814 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → (𝑁‘{𝑋}) ⊆ 𝑈) | ||
Theorem | lspsnel3 18812 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 27815 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑈) | ||
Theorem | lspprss 18813 | 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 18814 | A vector belongs to the span of its singleton. (spansnid 27806 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) | ||
Theorem | lspsnel6 18815 | 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 18816 | 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 18817 | 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 18818 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspprid2 18819 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspprvacl 18820 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lssats2 18821* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 (𝑁‘{𝑥})) | ||
Theorem | lspsneli 18822 | A scalar product with a vector belongs to the span of its singleton. (spansnmul 27807 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 · 𝑋) ∈ (𝑁‘{𝑋})) | ||
Theorem | lspsn 18823* | 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 18824* | Member of span of the singleton of a vector. (elspansn 27809 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑈 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ 𝐾 𝑈 = (𝑘 · 𝑋))) | ||
Theorem | lspsnvsi 18825 | 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 18826* | Comparable spans of singletons must have proportional vectors. See lspsneq 18943 for equal span version. (Contributed by NM, 7-Jun-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ 𝐾 𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsnneg 18827 | 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 18828 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{(𝑋 − 𝑌)}) = (𝑁‘{(𝑌 − 𝑋)})) | ||
Theorem | lspsn0 18829 | Span of the singleton of the zero vector. (spansn0 27784 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑁‘{ 0 }) = { 0 }) | ||
Theorem | lsp0 18830 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑁‘∅) = { 0 }) | ||
Theorem | lspuni0 18831 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → ∪ (𝑁‘∅) = 0 ) | ||
Theorem | lspun0 18832 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘(𝑋 ∪ { 0 })) = (𝑁‘𝑋)) | ||
Theorem | lspsneq0 18833 | 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 18834 | 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 18835 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) | ||
Theorem | lsslsp 18836 | 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 18837 | 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 18838* | 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 18839* | 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.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐿 ∈ V) ⇒ ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿)) | ||
Syntax | clmhm 18840 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 18841 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 18842 | The class of the left module isomorphism relation. |
class ≃𝑚 | ||
Definition | df-lmhm 18843* | 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 18844* | 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 18845 | 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 ∖ 1𝑜)) | ||
Theorem | reldmlmhm 18846 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ Rel dom LMHom | ||
Theorem | lmimfn 18847 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ LMIso Fn (LMod × LMod) | ||
Theorem | islmhm 18848* | 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 18849* | Property of a module homomorphism, similar to ismhm 17160. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))))) | ||
Theorem | lmhmlem 18850 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾))) | ||
Theorem | lmhmsca 18851 | 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 18852 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | lmhmlmod2 18853 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | ||
Theorem | lmhmlmod1 18854 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | ||
Theorem | lmhmf 18855 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | lmhmlin 18856 | A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌))) | ||
Theorem | lmodvsinv 18857 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | lmodvsinv2 18858 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | islmhm2 18859* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 18754. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐸 = (Base‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧))))) | ||
Theorem | islmhmd 18860* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐽 = (Scalar‘𝑇) & ⊢ 𝑁 = (Base‘𝐾) & ⊢ (𝜑 → 𝑆 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐽 = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | 0lmhm 18861 | The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 0 = (0g‘𝑁) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑇 = (Scalar‘𝑁) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇) → (𝐵 × { 0 }) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | idlmhm 18862 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → ( I ↾ 𝐵) ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | invlmhm 18863 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐼 = (invg‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐼 ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | lmhmco 18864 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘ 𝐺) ∈ (𝑀 LMHom 𝑂)) | ||
Theorem | lmhmplusg 18865 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ + = (+g‘𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | lmhmvsca 18866 | The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑁) & ⊢ 𝐽 = (Scalar‘𝑁) & ⊢ 𝐾 = (Base‘𝐽) ⇒ ⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘𝑓 · 𝐹) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | lmhmf1o 18867 | A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆))) | ||
Theorem | lmhmima 18868 | The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌) | ||
Theorem | lmhmpreima 18869 | The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) | ||
Theorem | lmhmlsp 18870 | Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐾 = (LSpan‘𝑆) & ⊢ 𝐿 = (LSpan‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈))) | ||
Theorem | lmhmrnlss 18871 | The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) | ||
Theorem | lmhmkerlss 18872 | The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈) | ||
Theorem | reslmhm 18873 | Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) & ⊢ 𝑅 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇)) | ||
Theorem | reslmhm2 18874 | Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) & ⊢ 𝐿 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑈) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | reslmhm2b 18875 | Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) & ⊢ 𝐿 = (LSubSp‘𝑇) ⇒ ⊢ ((𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ 𝐹 ∈ (𝑆 LMHom 𝑈))) | ||
Theorem | lmhmeql 18876 | The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈) | ||
Theorem | lspextmo 18877* | A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐾 = (LSpan‘𝑆) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ (𝐾‘𝑋) = 𝐵) → ∃*𝑔 ∈ (𝑆 LMHom 𝑇)(𝑔 ↾ 𝑋) = 𝐹) | ||
Theorem | pwsdiaglmhm 18878* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 LMHom 𝑌)) | ||
Theorem | pwssplit0 18879* | Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶) | ||
Theorem | pwssplit1 18880* | Splitting for structure powers, part 1: restriction is an onto function. The only actual monoid law we need here is that the base set is nonempty. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵–onto→𝐶) | ||
Theorem | pwssplit2 18881* | Splitting for structure powers, part 2: restriction is a group homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 GrpHom 𝑍)) | ||
Theorem | pwssplit3 18882* | Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 LMHom 𝑍)) | ||
Theorem | islmim 18883 | An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)) | ||
Theorem | lmimf1o 18884 | An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | lmimlmhm 18885 | An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 LMHom 𝑆)) | ||
Theorem | lmimgim 18886 | An isomorphism of modules is an isomorphism of groups. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆)) | ||
Theorem | islmim2 18887 | An isomorphism of left modules is a homomorphism whose converse is a homomorphism. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 LMHom 𝑅))) | ||
Theorem | lmimcnv 18888 | The converse of a bijective module homomorphism is a bijective module homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑆 LMIso 𝑇) → ◡𝐹 ∈ (𝑇 LMIso 𝑆)) | ||
Theorem | brlmic 18889 | The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 ↔ (𝑅 LMIso 𝑆) ≠ ∅) | ||
Theorem | brlmici 18890 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝑅 ≃𝑚 𝑆) | ||
Theorem | lmiclcl 18891 | Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑅 ∈ LMod) | ||
Theorem | lmicrcl 18892 | Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ∈ LMod) | ||
Theorem | lmicsym 18893 | Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅) | ||
Theorem | lmhmpropd 18894* | Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐽)) & ⊢ (𝜑 → 𝐺 = (Scalar‘𝐾)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿)) & ⊢ (𝜑 → 𝐺 = (Scalar‘𝑀)) & ⊢ 𝑃 = (Base‘𝐹) & ⊢ 𝑄 = (Base‘𝐺) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐽)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝐶)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 LMHom 𝐾) = (𝐿 LMHom 𝑀)) | ||
Syntax | clbs 18895 | Extend class notation with the set of bases for a vector space. |
class LBasis | ||
Definition | df-lbs 18896* | Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) | ||
Theorem | islbs 18897* | The predicate "𝐵 is a basis for the left module or vector space 𝑊". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) | ||
Theorem | lbsss 18898 | A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉) | ||
Theorem | lbsel 18899 | An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → 𝐸 ∈ 𝑉) | ||
Theorem | lbssp 18900 | The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |