Home | Metamath
Proof Explorer Theorem List (p. 199 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 | lspsntrim 19801 | Triangle-type inequality for span of a singleton of vector difference. (Contributed by NM, 25-Apr-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑌)}) ⊆ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌}))) | ||
Theorem | lbspropd 19802* | If two structures have the same components (properties), they have the same set of bases. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐿 ∈ V) ⇒ ⊢ (𝜑 → (LBasis‘𝐾) = (LBasis‘𝐿)) | ||
Theorem | pj1lmhm 19803 | The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝐿) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom 𝑊)) | ||
Theorem | pj1lmhm2 19804 | The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝐿) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom (𝑊 ↾s 𝑇))) | ||
Syntax | clvec 19805 | Extend class notation with class of all left vector spaces. |
class LVec | ||
Definition | df-lvec 19806 | Define the class of all left vector spaces. A left vector space over a division ring is an Abelian group (vectors) together with a division ring (scalars) and a left scalar product connecting them. Some authors call this a "left module over a division ring", reserving "vector space" for those where the division ring is commutative, i.e., is a field. (Contributed by NM, 11-Nov-2013.) |
⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing} | ||
Theorem | islvec 19807 | The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) | ||
Theorem | lvecdrng 19808 | The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) | ||
Theorem | lveclmod 19809 | A left vector space is a left module. (Contributed by NM, 9-Dec-2013.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | ||
Theorem | lsslvec 19810 | A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LVec) | ||
Theorem | lvecvs0or 19811 | If a scalar product is zero, one of its factors must be zero. (hvmul0or 28730 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = 0 ↔ (𝐴 = 𝑂 ∨ 𝑋 = 0 ))) | ||
Theorem | lvecvsn0 19812 | A scalar product is nonzero iff both of its factors are nonzero. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) ≠ 0 ↔ (𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 ))) | ||
Theorem | lssvs0or 19813 | If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) ∈ 𝑈 ↔ (𝐴 = 0 ∨ 𝑋 ∈ 𝑈))) | ||
Theorem | lvecvscan 19814 | Cancellation law for scalar multiplication. (hvmulcan 28777 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐴 · 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lvecvscan2 19815 | Cancellation law for scalar multiplication. (hvmulcan2 28778 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐵 · 𝑋) ↔ 𝐴 = 𝐵)) | ||
Theorem | lvecinv 19816 | Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝐼 = (invr‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 = (𝐴 · 𝑌) ↔ 𝑌 = ((𝐼‘𝐴) · 𝑋))) | ||
Theorem | lspsnvs 19817 | A nonzero scalar product does not change the span of a singleton. (spansncol 29273 analog.) (Contributed by NM, 23-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) = (𝑁‘{𝑋})) | ||
Theorem | lspsneleq 19818 | Membership relation that implies equality of spans. (spansneleq 29275 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑋})) | ||
Theorem | lspsncmp 19819 | Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) | ||
Theorem | lspsnne1 19820 | Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) | ||
Theorem | lspsnne2 19821 | Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | ||
Theorem | lspsnnecom 19822 | Swap two vectors with different spans. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋})) | ||
Theorem | lspabs2 19823 | Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) | ||
Theorem | lspabs3 19824 | Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)})) | ||
Theorem | lspsneq 19825* | Equal spans of singletons must have proportional vectors. See lspsnss2 19708 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsneu 19826* | Nonzero vectors with equal singleton spans have a unique proportionality constant. (Contributed by NM, 31-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑂 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃!𝑘 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsnel4 19827 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 29278 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈)) | ||
Theorem | lspdisj 19828 | The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 }) | ||
Theorem | lspdisjb 19829 | A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 })) | ||
Theorem | lspdisj2 19830 | Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌})) = { 0 }) | ||
Theorem | lspfixed 19831* | Show membership in the span of the sum of two vectors, one of which (𝑌) is fixed in advance. (Contributed by NM, 27-May-2015.) (Revised by AV, 12-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) | ||
Theorem | lspexch 19832 | Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 19833 versus lspexchn2 19834); look for lspexch 19832 and prcom 4662 in same proof. TODO: would a hypothesis of ¬ 𝑋 ∈ (𝑁‘{𝑍}) instead of (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) be better overall? This would be shorter and also satisfy the 𝑋 ≠ 0 condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the ≠ pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑍})) | ||
Theorem | lspexchn1 19833 | Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 19832 to see if this will shorten proofs. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍})) | ||
Theorem | lspexchn2 19834 | Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 19832 to see if this will shorten proofs. (Contributed by NM, 24-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋})) | ||
Theorem | lspindpi 19835 | Partial independence property. (Contributed by NM, 23-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))) | ||
Theorem | lspindp1 19836 | Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌}))) | ||
Theorem | lspindp2l 19837 | Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))) | ||
Theorem | lspindp2 19838 | Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋}))) | ||
Theorem | lspindp3 19839 | Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑋 + 𝑌)})) | ||
Theorem | lspindp4 19840 | (Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑋 + 𝑌)})) | ||
Theorem | lvecindp 19841 | Compute the 𝑋 coefficient in a sum with an independent vector 𝑋 (first conjunct), which can then be removed to continue with the remaining vectors summed in expressions 𝑌 and 𝑍 (second conjunct). Typically, 𝑈 is the span of the remaining vectors. (Contributed by NM, 5-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 19-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝑌) = ((𝐵 · 𝑋) + 𝑍)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝑌 = 𝑍)) | ||
Theorem | lvecindp2 19842 | Sums of independent vectors must have equal coefficients. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) & ⊢ (𝜑 → 𝐷 ∈ 𝐾) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = ((𝐶 · 𝑋) + (𝐷 · 𝑌))) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | lspsnsubn0 19843 | Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ≠ 0 ) | ||
Theorem | lsmcv 19844 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 29357 analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ (𝑁‘{𝑋}))) → 𝑈 = (𝑇 ⊕ (𝑁‘{𝑋}))) | ||
Theorem | lspsolvlem 19845* | Lemma for lspsolv 19846. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)} & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌}))) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) | ||
Theorem | lspsolv 19846 | If 𝑋 is in the span of 𝐴 ∪ {𝑌} but not 𝐴, then 𝑌 is in the span of 𝐴 ∪ {𝑋}. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑌 ∈ (𝑁‘(𝐴 ∪ {𝑋}))) | ||
Theorem | lssacsex 19847* | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 19670 by lspsolv 19846. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = (LSubSp‘𝑊) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝑋 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝐴 ∈ (ACS‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))) | ||
Theorem | lspsnat 19848 | There is no subspace strictly between the zero subspace and the span of a vector (i.e. a 1-dimensional subspace is an atom). (h1datomi 29286 analog.) (Contributed by NM, 20-Apr-2014.) (Proof shortened by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑉) ∧ 𝑈 ⊆ (𝑁‘{𝑋})) → (𝑈 = (𝑁‘{𝑋}) ∨ 𝑈 = { 0 })) | ||
Theorem | lspsncv0 19849* | The span of a singleton covers the zero subspace, using Definition 3.2.18 of [PtakPulmannova] p. 68 for "covers".) (Contributed by NM, 12-Aug-2014.) (Revised by AV, 13-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝑆 ({ 0 } ⊊ 𝑦 ∧ 𝑦 ⊊ (𝑁‘{𝑋}))) | ||
Theorem | lsppratlem1 19850 | Lemma for lspprat 19856. Let 𝑥 ∈ (𝑈 ∖ {0}) (if there is no such 𝑥 then 𝑈 is the zero subspace), and let 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥})) (assuming the conclusion is false). The goal is to write 𝑋, 𝑌 in terms of 𝑥, 𝑦, which would normally be done by solving the system of linear equations. The span equivalent of this process is lspsolv 19846 (hence the name), which we use extensively below. In this lemma, we show that since 𝑥 ∈ (𝑁‘{𝑋, 𝑌}), either 𝑥 ∈ (𝑁‘{𝑌}) or 𝑋 ∈ (𝑁‘{𝑥, 𝑌}). (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑁‘{𝑌}) ∨ 𝑋 ∈ (𝑁‘{𝑥, 𝑌}))) | ||
Theorem | lsppratlem2 19851 | Lemma for lspprat 19856. Show that if 𝑋 and 𝑌 are both in (𝑁‘{𝑥, 𝑦}) (which will be our goal for each of the two cases above), then (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈, contradicting the hypothesis for 𝑈. (Contributed by NM, 29-Aug-2014.) (Revised by Mario Carneiro, 5-Sep-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑦})) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑥, 𝑦})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈) | ||
Theorem | lsppratlem3 19852 | Lemma for lspprat 19856. In the first case of lsppratlem1 19850, since 𝑥 ∉ (𝑁‘∅), also 𝑌 ∈ (𝑁‘{𝑥}), and since 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑋, 𝑥}) and 𝑦 ∉ (𝑁‘{𝑥}), we have 𝑋 ∈ (𝑁‘{𝑥, 𝑦}) as desired. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) & ⊢ (𝜑 → 𝑥 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) | ||
Theorem | lsppratlem4 19853 | Lemma for lspprat 19856. In the second case of lsppratlem1 19850, 𝑦 ∈ (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌}) and 𝑦 ∉ (𝑁‘{𝑥}) implies 𝑌 ∈ (𝑁‘{𝑥, 𝑦}) and thus 𝑋 ∈ (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦}) as well. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌})) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) | ||
Theorem | lsppratlem5 19854 | Lemma for lspprat 19856. Combine the two cases and show a contradiction to 𝑈 ⊊ (𝑁‘{𝑋, 𝑌}) under the assumptions on 𝑥 and 𝑦. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) & ⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ 𝑈) | ||
Theorem | lsppratlem6 19855 | Lemma for lspprat 19856. Negating the assumption on 𝑦, we arrive close to the desired conclusion. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑈 ∖ { 0 }) → 𝑈 = (𝑁‘{𝑥}))) | ||
Theorem | lspprat 19856* | A proper subspace of the span of a pair of vectors is the span of a singleton (an atom) or the zero subspace (if 𝑧 is zero). Proof suggested by Mario Carneiro, 28-Aug-2014. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 𝑈 = (𝑁‘{𝑧})) | ||
Theorem | islbs2 19857* | An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) | ||
Theorem | islbs3 19858* | An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑠(𝑠 ⊊ 𝐵 → (𝑁‘𝑠) ⊊ 𝑉)))) | ||
Theorem | lbsacsbs 19859 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 19857. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = (LSubSp‘𝑊) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝐼 ∧ (𝑁‘𝑆) = 𝑋))) | ||
Theorem | lvecdim 19860 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 19847 and lbsacsbs 19859 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 17783. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑇 ∈ 𝐽) → 𝑆 ≈ 𝑇) | ||
Theorem | lbsextlem1 19861* | Lemma for lbsext 19866. The set 𝑆 is the set of all linearly independent sets containing 𝐶; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐶 ⊆ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) & ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⇒ ⊢ (𝜑 → 𝑆 ≠ ∅) | ||
Theorem | lbsextlem2 19862* | Lemma for lbsext 19866. Since 𝐴 is a chain (actually, we only need it to be closed under binary union), the union 𝑇 of the spans of each individual element of 𝐴 is a subspace, and it contains all of ∪ 𝐴 (except for our target vector 𝑥- we are trying to make 𝑥 a linear combination of all the other vectors in some set from 𝐴). (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐶 ⊆ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) & ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} & ⊢ 𝑃 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝐴) & ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⇒ ⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇)) | ||
Theorem | lbsextlem3 19863* | Lemma for lbsext 19866. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐶 ⊆ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) & ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} & ⊢ 𝑃 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝐴) & ⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | lbsextlem4 19864* | Lemma for lbsext 19866. lbsextlem3 19863 satisfies the conditions for the application of Zorn's lemma zorn 9918 (thus invoking AC), and so there is a maximal linearly independent set extending 𝐶. Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐶 ⊆ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) & ⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} & ⊢ (𝜑 → 𝒫 𝑉 ∈ dom card) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠) | ||
Theorem | lbsextg 19865* | For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (((𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card) ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠) | ||
Theorem | lbsext 19866* | For any linearly independent subset 𝐶 of 𝑉, there is a basis containing the vectors in 𝐶. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐶 ⊆ 𝑉 ∧ ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠) | ||
Theorem | lbsexg 19867 | Every vector space has a basis. This theorem is an AC equivalent; this is the forward implication. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((CHOICE ∧ 𝑊 ∈ LVec) → 𝐽 ≠ ∅) | ||
Theorem | lbsex 19868 | Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐽 ≠ ∅) | ||
Theorem | lvecprop2d 19869* | If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd 19870 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‘𝐺)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec)) | ||
Theorem | lvecpropd 19870* | If two structures have the same components (properties), one is a left vector space iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿)) & ⊢ 𝑃 = (Base‘𝐹) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec)) | ||
Syntax | csra 19871 | Extend class notation with the subring algebra generator. |
class subringAlg | ||
Syntax | crglmod 19872 | Extend class notation with the left module induced by a ring over itself. |
class ringLMod | ||
Syntax | clidl 19873 | Ring left-ideal function. |
class LIdeal | ||
Syntax | crsp 19874 | Ring span function. |
class RSpan | ||
Definition | df-sra 19875* | Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ subringAlg = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) sSet 〈( ·𝑠 ‘ndx), (.r‘𝑤)〉) sSet 〈(·𝑖‘ndx), (.r‘𝑤)〉))) | ||
Definition | df-rgmod 19876 | Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ ringLMod = (𝑤 ∈ V ↦ ((subringAlg ‘𝑤)‘(Base‘𝑤))) | ||
Definition | df-lidl 19877 | Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ LIdeal = (LSubSp ∘ ringLMod) | ||
Definition | df-rsp 19878 | Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ RSpan = (LSpan ∘ ringLMod) | ||
Theorem | sraval 19879 | Lemma for srabase 19881 through sravsca 19885. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈( ·𝑠 ‘ndx), (.r‘𝑊)〉) sSet 〈(·𝑖‘ndx), (.r‘𝑊)〉)) | ||
Theorem | sralem 19880 | Lemma for srabase 19881 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ (𝑁 < 5 ∨ 8 < 𝑁) ⇒ ⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴)) | ||
Theorem | srabase 19881 | Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (Base‘𝑊) = (Base‘𝐴)) | ||
Theorem | sraaddg 19882 | Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (+g‘𝑊) = (+g‘𝐴)) | ||
Theorem | sramulr 19883 | Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = (.r‘𝐴)) | ||
Theorem | srasca 19884 | The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) | ||
Theorem | sravsca 19885 | The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = ( ·𝑠 ‘𝐴)) | ||
Theorem | sraip 19886 | The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (.r‘𝑊) = (·𝑖‘𝐴)) | ||
Theorem | sratset 19887 | Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴)) | ||
Theorem | sratopn 19888 | Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (TopOpen‘𝑊) = (TopOpen‘𝐴)) | ||
Theorem | srads 19889 | Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → (dist‘𝑊) = (dist‘𝐴)) | ||
Theorem | sralmod 19890 | The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆) ⇒ ⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝐴 ∈ LMod) | ||
Theorem | sralmod0 19891 | The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 0 = (0g‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 0 = (0g‘𝐴)) | ||
Theorem | issubrngd2 19892* | Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷)) & ⊢ (𝜑 → 0 = (0g‘𝐼)) & ⊢ (𝜑 → + = (+g‘𝐼)) & ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼)) & ⊢ (𝜑 → 0 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷) & ⊢ (𝜑 → 1 = (1r‘𝐼)) & ⊢ (𝜑 → · = (.r‘𝐼)) & ⊢ (𝜑 → 1 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 · 𝑦) ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ∈ Ring) ⇒ ⊢ (𝜑 → 𝐷 ∈ (SubRing‘𝐼)) | ||
Theorem | rlmfn 19893 | ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.) |
⊢ ringLMod Fn V | ||
Theorem | rlmval 19894 | Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (ringLMod‘𝑊) = ((subringAlg ‘𝑊)‘(Base‘𝑊)) | ||
Theorem | lidlval 19895 | Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊)) | ||
Theorem | rspval 19896 | Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
⊢ (RSpan‘𝑊) = (LSpan‘(ringLMod‘𝑊)) | ||
Theorem | rlmval2 19897 | Value of the ring module extended. (Contributed by AV, 2-Dec-2018.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝑊 ∈ 𝑋 → (ringLMod‘𝑊) = (((𝑊 sSet 〈(Scalar‘ndx), 𝑊〉) sSet 〈( ·𝑠 ‘ndx), (.r‘𝑊)〉) sSet 〈(·𝑖‘ndx), (.r‘𝑊)〉)) | ||
Theorem | rlmbas 19898 | Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (Base‘𝑅) = (Base‘(ringLMod‘𝑅)) | ||
Theorem | rlmplusg 19899 | Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
⊢ (+g‘𝑅) = (+g‘(ringLMod‘𝑅)) | ||
Theorem | rlm0 19900 | Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ (0g‘𝑅) = (0g‘(ringLMod‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |