Home | Metamath
Proof Explorer Theorem List (p. 334 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 | lsatlss 33301 | The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆) | ||
Theorem | lsatlssel 33302 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | lsatssv 33303 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑄 ⊆ 𝑉) | ||
Theorem | lsatn0 33304 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 28588 analog.) (Contributed by NM, 25-Aug-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑈 ≠ { 0 }) | ||
Theorem | lsatspn0 33305 | The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ↔ 𝑋 ≠ 0 )) | ||
Theorem | lsator0sp 33306 | The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ∨ (𝑁‘{𝑋}) = { 0 })) | ||
Theorem | lsatssn0 33307 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑈 ≠ { 0 }) | ||
Theorem | lsatcmp 33308 | If two atoms are comparable, they are equal. (atsseq 28590 analog.) TODO: can lspsncmp 18937 shorten this? (Contributed by NM, 25-Aug-2014.) |
⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
Theorem | lsatcmp2 33309 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 33308. TODO: can lspsncmp 18937 shorten this? (Contributed by NM, 3-Feb-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝐴) & ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 })) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) | ||
Theorem | lsatel 33310 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → 𝑈 = (𝑁‘{𝑋})) | ||
Theorem | lsatelbN 33311 | A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑈 = (𝑁‘{𝑋}))) | ||
Theorem | lsat2el 33312 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑃 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑄) ⇒ ⊢ (𝜑 → 𝑃 = 𝑄) | ||
Theorem | lsmsat 33313* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 34109 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑇 ≠ { 0 }) & ⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈))) | ||
Theorem | lsatfixedN 33314* | Show equality with the span of the sum of two vectors, one of which (𝑋) is fixed in advance. Compare lspfixed 18949. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑄 ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → 𝑄 ⊆ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑌}) ∖ { 0 })𝑄 = (𝑁‘{(𝑋 + 𝑧)})) | ||
Theorem | lsmsatcv 33315 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 27895 analog.) Explicit atom version of lsmcv 18962. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇 ⊕ 𝑄)) → 𝑈 = (𝑇 ⊕ 𝑄)) | ||
Theorem | lssatomic 33316* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 28601 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ≠ { 0 }) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈) | ||
Theorem | lssats 33317* | The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. Hypothesis (shatomistici 28604 analog.) (Contributed by NM, 9-Apr-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) | ||
Theorem | lpssat 33318* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 28606 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ⊊ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) | ||
Theorem | lrelat 33319* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 28607 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ⊊ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊊ (𝑇 ⊕ 𝑞) ∧ (𝑇 ⊕ 𝑞) ⊆ 𝑈)) | ||
Theorem | lssatle 33320* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 28614 analog.) (Contributed by NM, 29-Oct-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈))) | ||
Theorem | lssat 33321* | Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. (chpssati 28606 analog.) (Contributed by NM, 9-Apr-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑉 ∈ 𝑆) ∧ 𝑈 ⊊ 𝑉) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ 𝑈)) | ||
Theorem | islshpat 33322* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 33285. (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ 𝐴 (𝑈 ⊕ 𝑞) = 𝑉))) | ||
Syntax | clcv 33323 | Extend class notation with the covering relation for a left module or left vector space. |
class ⋖L | ||
Definition | df-lcv 33324* | Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation 𝐴( ⋖L ‘𝑊)𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See lcvbr 33326 for binary relation. (df-cv 28522 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ ⋖L = (𝑤 ∈ V ↦ {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) | ||
Theorem | lcvfbr 33325* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐶 = {〈𝑡, 𝑢〉 ∣ ((𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}) | ||
Theorem | lcvbr 33326* | The covers relation for a left vector space (or a left module). (cvbr 28525 analog.) (Contributed by NM, 9-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ¬ ∃𝑠 ∈ 𝑆 (𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈)))) | ||
Theorem | lcvbr2 33327* | The covers relation for a left vector space (or a left module). (cvbr2 28526 analog.) (Contributed by NM, 9-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈)))) | ||
Theorem | lcvbr3 33328* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑇𝐶𝑈 ↔ (𝑇 ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 ((𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈) → (𝑠 = 𝑇 ∨ 𝑠 = 𝑈))))) | ||
Theorem | lcvpss 33329 | The covers relation implies proper subset. (cvpss 28528 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇𝐶𝑈) ⇒ ⊢ (𝜑 → 𝑇 ⊊ 𝑈) | ||
Theorem | lcvnbtwn 33330 | The covers relation implies no in-betweenness. (cvnbtwn 28529 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅𝐶𝑇) ⇒ ⊢ (𝜑 → ¬ (𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇)) | ||
Theorem | lcvntr 33331 | The covers relation is not transitive. (cvntr 28535 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅𝐶𝑇) & ⊢ (𝜑 → 𝑇𝐶𝑈) ⇒ ⊢ (𝜑 → ¬ 𝑅𝐶𝑈) | ||
Theorem | lcvnbtwn2 33332 | The covers relation implies no in-betweenness. (cvnbtwn2 28530 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅𝐶𝑇) & ⊢ (𝜑 → 𝑅 ⊊ 𝑈) & ⊢ (𝜑 → 𝑈 ⊆ 𝑇) ⇒ ⊢ (𝜑 → 𝑈 = 𝑇) | ||
Theorem | lcvnbtwn3 33333 | The covers relation implies no in-betweenness. (cvnbtwn3 28531 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅𝐶𝑇) & ⊢ (𝜑 → 𝑅 ⊆ 𝑈) & ⊢ (𝜑 → 𝑈 ⊊ 𝑇) ⇒ ⊢ (𝜑 → 𝑈 = 𝑅) | ||
Theorem | lsmcv2 33334 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 28536 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ (𝑁‘{𝑋}) ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑈𝐶(𝑈 ⊕ (𝑁‘{𝑋}))) | ||
Theorem | lcvat 33335* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 28609 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇𝐶𝑈) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑇 ⊕ 𝑞) = 𝑈) | ||
Theorem | lsatcv0 33336 | An atom covers the zero subspace. (atcv0 28585 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → { 0 }𝐶𝑄) | ||
Theorem | lsatcveq0 33337 | A subspace covered by an atom must be the zero subspace. (atcveq0 28591 analog.) (Contributed by NM, 7-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑈𝐶𝑄 ↔ 𝑈 = { 0 })) | ||
Theorem | lsat0cv 33338 | A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ { 0 }𝐶𝑈)) | ||
Theorem | lcvexchlem1 33339 | Lemma for lcvexch 33344. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑇 ⊊ (𝑇 ⊕ 𝑈) ↔ (𝑇 ∩ 𝑈) ⊊ 𝑈)) | ||
Theorem | lcvexchlem2 33340 | Lemma for lcvexch 33344. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) ⊆ 𝑅) & ⊢ (𝜑 → 𝑅 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ∩ 𝑈) = 𝑅) | ||
Theorem | lcvexchlem3 33341 | Lemma for lcvexch 33344. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ⊆ 𝑅) & ⊢ (𝜑 → 𝑅 ⊆ (𝑇 ⊕ 𝑈)) ⇒ ⊢ (𝜑 → ((𝑅 ∩ 𝑈) ⊕ 𝑇) = 𝑅) | ||
Theorem | lcvexchlem4 33342 | Lemma for lcvexch 33344. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈)) ⇒ ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈) | ||
Theorem | lcvexchlem5 33343 | Lemma for lcvexch 33344. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (𝑇 ∩ 𝑈)𝐶𝑈) ⇒ ⊢ (𝜑 → 𝑇𝐶(𝑇 ⊕ 𝑈)) | ||
Theorem | lcvexch 33344 | Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 28612 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝑇 ∩ 𝑈)𝐶𝑈 ↔ 𝑇𝐶(𝑇 ⊕ 𝑈))) | ||
Theorem | lcvp 33345 | Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28618 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑈 ∩ 𝑄) = { 0 } ↔ 𝑈𝐶(𝑈 ⊕ 𝑄))) | ||
Theorem | lcv1 33346 | Covering property of a subspace plus an atom. (chcv1 28598 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄))) | ||
Theorem | lcv2 33347 | Covering property of a subspace plus an atom. (chcv2 28599 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑈 ⊊ (𝑈 ⊕ 𝑄) ↔ 𝑈𝐶(𝑈 ⊕ 𝑄))) | ||
Theorem | lsatexch 33348 | The atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. (atexch 28624 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ⊆ (𝑈 ⊕ 𝑅)) & ⊢ (𝜑 → (𝑈 ∩ 𝑄) = { 0 }) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (𝑈 ⊕ 𝑄)) | ||
Theorem | lsatnle 33349 | The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 28619 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ (𝑈 ∩ 𝑄) = { 0 })) | ||
Theorem | lsatnem0 33350 | The meet of distinct atoms is the zero subspace. (atnemeq0 28620 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑄 ≠ 𝑅 ↔ (𝑄 ∩ 𝑅) = { 0 })) | ||
Theorem | lsatexch1 33351 | The atom exch1ange property. (hlatexch1 33699 analog.) (Contributed by NM, 14-Jan-2015.) |
⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ⊆ (𝑆 ⊕ 𝑅)) & ⊢ (𝜑 → 𝑄 ≠ 𝑆) ⇒ ⊢ (𝜑 → 𝑅 ⊆ (𝑆 ⊕ 𝑄)) | ||
Theorem | lsatcv0eq 33352 | If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 28622 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) ⇒ ⊢ (𝜑 → ({ 0 }𝐶(𝑄 ⊕ 𝑅) ↔ 𝑄 = 𝑅)) | ||
Theorem | lsatcv1 33353 | Two atoms covering the zero subspace are equal. (atcv1 28623 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑈𝐶(𝑄 ⊕ 𝑅)) ⇒ ⊢ (𝜑 → (𝑈 = { 0 } ↔ 𝑄 = 𝑅)) | ||
Theorem | lsatcvatlem 33354 | Lemma for lsatcvat 33355. (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≠ { 0 }) & ⊢ (𝜑 → 𝑈 ⊊ (𝑄 ⊕ 𝑅)) & ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐴) | ||
Theorem | lsatcvat 33355 | A nonzero subspace less than the sum of two atoms is an atom. (atcvati 28629 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≠ { 0 }) & ⊢ (𝜑 → 𝑈 ⊊ (𝑄 ⊕ 𝑅)) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐴) | ||
Theorem | lsatcvat2 33356 | A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 28630 analog.) (Contributed by NM, 10-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ≠ 𝑅) & ⊢ (𝜑 → 𝑈𝐶(𝑄 ⊕ 𝑅)) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐴) | ||
Theorem | lsatcvat3 33357 | A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28639 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ≠ 𝑅) & ⊢ (𝜑 → ¬ 𝑅 ⊆ 𝑈) & ⊢ (𝜑 → 𝑄 ⊆ (𝑈 ⊕ 𝑅)) ⇒ ⊢ (𝜑 → (𝑈 ∩ (𝑄 ⊕ 𝑅)) ∈ 𝐴) | ||
Theorem | islshpcv 33358 | Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))) | ||
Theorem | l1cvpat 33359 | A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 33779 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑈𝐶𝑉) & ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → (𝑈 ⊕ 𝑄) = 𝑉) | ||
Theorem | l1cvat 33360 | Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 33780 analog.) (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ 𝐶 = ( ⋖L ‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ≠ 𝑅) & ⊢ (𝜑 → 𝑈𝐶𝑉) & ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ((𝑄 ⊕ 𝑅) ∩ 𝑈) ∈ 𝐴) | ||
Theorem | lshpat 33361 | Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 34347 analog.) TODO: This changes 𝑈𝐶𝑉 in l1cvpat 33359 and l1cvat 33360 to 𝑈 ∈ 𝐻, which in turn change 𝑈 ∈ 𝐻 in islshpcv 33358 to 𝑈𝐶𝑉, with a couple of conversions of span to atom. Seems convoluted. Would a direct proof be better? (Contributed by NM, 11-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑄 ∈ 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝐴) & ⊢ (𝜑 → 𝑄 ≠ 𝑅) & ⊢ (𝜑 → ¬ 𝑄 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ((𝑄 ⊕ 𝑅) ∩ 𝑈) ∈ 𝐴) | ||
Syntax | clfn 33362 | Extend class notation with all linear functionals of a left module or left vector space. |
class LFnl | ||
Definition | df-lfl 33363* | Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014.) |
⊢ LFnl = (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑𝑚 (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))}) | ||
Theorem | lflset 33364* | The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ⨣ = (+g‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐹 = {𝑓 ∈ (𝐾 ↑𝑚 𝑉) ∣ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑓‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝑓‘𝑥)) ⨣ (𝑓‘𝑦))}) | ||
Theorem | islfl 33365* | The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ⨣ = (+g‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝐺 ∈ 𝐹 ↔ (𝐺:𝑉⟶𝐾 ∧ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))))) | ||
Theorem | lfli 33366 | Property of a linear functional. (lnfnli 28283 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ⨣ = (+g‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌))) | ||
Theorem | islfld 33367* | Properties that determine a linear functional. TODO: use this in place of islfl 33365 when it shortens the proof. (Contributed by NM, 19-Oct-2014.) |
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) & ⊢ (𝜑 → + = (+g‘𝑊)) & ⊢ (𝜑 → 𝐷 = (Scalar‘𝑊)) & ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐷)) & ⊢ (𝜑 → ⨣ = (+g‘𝐷)) & ⊢ (𝜑 → × = (.r‘𝐷)) & ⊢ (𝜑 → 𝐹 = (LFnl‘𝑊)) & ⊢ (𝜑 → 𝐺:𝑉⟶𝐾) & ⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐹) | ||
Theorem | lflf 33368 | A linear functional is a function from vectors to scalars. (lnfnfi 28284 analog.) (Contributed by NM, 15-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝐾) | ||
Theorem | lflcl 33369 | A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → (𝐺‘𝑋) ∈ 𝐾) | ||
Theorem | lfl0 33370 | A linear functional is zero at the zero vector. (lnfn0i 28285 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑍 = (0g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘𝑍) = 0 ) | ||
Theorem | lfladd 33371 | Property of a linear functional. (lnfnaddi 28286 analog.) (Contributed by NM, 18-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ ⨣ = (+g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘(𝑋 + 𝑌)) = ((𝐺‘𝑋) ⨣ (𝐺‘𝑌))) | ||
Theorem | lflsub 33372 | Property of a linear functional. (lnfnaddi 28286 analog.) (Contributed by NM, 18-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝑀 = (-g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘(𝑋 − 𝑌)) = ((𝐺‘𝑋)𝑀(𝐺‘𝑌))) | ||
Theorem | lflmul 33373 | Property of a linear functional. (lnfnmuli 28287 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝐺‘(𝑅 · 𝑋)) = (𝑅 × (𝐺‘𝑋))) | ||
Theorem | lfl0f 33374 | The zero function is a functional. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑉 × { 0 }) ∈ 𝐹) | ||
Theorem | lfl1 33375* | A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 1 = (1r‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → ∃𝑥 ∈ 𝑉 (𝐺‘𝑥) = 1 ) | ||
Theorem | lfladdcl 33376 | Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 + 𝐻) ∈ 𝐹) | ||
Theorem | lfladdcom 33377 | Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 + 𝐻) = (𝐻 ∘𝑓 + 𝐺)) | ||
Theorem | lfladdass 33378 | Associativity of functional addition. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝐼 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐺 ∘𝑓 + 𝐻) ∘𝑓 + 𝐼) = (𝐺 ∘𝑓 + (𝐻 ∘𝑓 + 𝐼))) | ||
Theorem | lfladd0l 33379 | Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑉 × { 0 }) ∘𝑓 + 𝐺) = 𝐺) | ||
Theorem | lflnegcl 33380* | Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 33451, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥))) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝐹) | ||
Theorem | lflnegl 33381* | A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 33451, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥))) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ + = (+g‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝜑 → (𝑁 ∘𝑓 + 𝐺) = (𝑉 × { 0 })) | ||
Theorem | lflvscl 33382 | Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014.) (Revised by Mario Carneiro, 22-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × {𝑅})) ∈ 𝐹) | ||
Theorem | lflvsdi1 33383 | Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐺 ∘𝑓 + 𝐻) ∘𝑓 · (𝑉 × {𝑋})) = ((𝐺 ∘𝑓 · (𝑉 × {𝑋})) ∘𝑓 + (𝐻 ∘𝑓 · (𝑉 × {𝑋})))) | ||
Theorem | lflvsdi2 33384 | Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · ((𝑉 × {𝑋}) ∘𝑓 + (𝑉 × {𝑌}))) = ((𝐺 ∘𝑓 · (𝑉 × {𝑋})) ∘𝑓 + (𝐺 ∘𝑓 · (𝑉 × {𝑌})))) | ||
Theorem | lflvsdi2a 33385 | Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × {(𝑋 + 𝑌)})) = ((𝐺 ∘𝑓 · (𝑉 × {𝑋})) ∘𝑓 + (𝐺 ∘𝑓 · (𝑉 × {𝑌})))) | ||
Theorem | lflvsass 33386 | Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × {(𝑋 · 𝑌)})) = ((𝐺 ∘𝑓 · (𝑉 × {𝑋})) ∘𝑓 · (𝑉 × {𝑌}))) | ||
Theorem | lfl0sc 33387 | The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of (𝑉 × { 0 }) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × { 0 })) = (𝑉 × { 0 })) | ||
Theorem | lflsc0N 33388 | The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑉 × { 0 }) ∘𝑓 · (𝑉 × {𝑋})) = (𝑉 × { 0 })) | ||
Theorem | lfl1sc 33389 | The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 1 = (1r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × { 1 })) = 𝐺) | ||
Syntax | clk 33390 | Extend class notation with the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. |
class LKer | ||
Definition | df-lkr 33391* | Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.) |
⊢ LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))}))) | ||
Theorem | lkrfval 33392* | The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐾 = (𝑓 ∈ 𝐹 ↦ (◡𝑓 “ { 0 }))) | ||
Theorem | lkrval 33393 | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = (◡𝐺 “ { 0 })) | ||
Theorem | ellkr 33394 | Membership in the kernel of a functional. (elnlfn 28171 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹) → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝑋 ∈ 𝑉 ∧ (𝐺‘𝑋) = 0 ))) | ||
Theorem | lkrval2 33395* | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ 𝑉 ∣ (𝐺‘𝑥) = 0 }) | ||
Theorem | ellkr2 33396 | Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝐺‘𝑋) = 0 )) | ||
Theorem | lkrcl 33397 | A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → 𝑋 ∈ 𝑉) | ||
Theorem | lkrf0 33398 | The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → (𝐺‘𝑋) = 0 ) | ||
Theorem | lkr0f 33399 | The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × { 0 }))) | ||
Theorem | lkrlss 33400 | The kernel of a linear functional is a subspace. (nlelshi 28303 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |