![]() |
Metamath
Proof Explorer Theorem List (p. 471 of 478) | < 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-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lincvalpr 47001 | The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝐹 = {〈𝑉, 𝑋〉, 〈𝑊, 𝑌〉} ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊))) | ||
Theorem | lincval1 47002 | The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = {〈𝑉, (0g‘𝑆)〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀)) | ||
Theorem | lcosn0 47003 | Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = {〈𝑉, (0g‘𝑆)〉} ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵) → (𝐹 ∈ (𝑅 ↑m {𝑉}) ∧ 𝐹 finSupp (0g‘𝑆) ∧ (𝐹( linC ‘𝑀){𝑉}) = (0g‘𝑀))) | ||
Theorem | lincvalsc0 47004* | The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) | ||
Theorem | lcoc0 47005* | Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) & ⊢ 𝑅 = (Base‘𝑆) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ (𝑅 ↑m 𝑉) ∧ 𝐹 finSupp 0 ∧ (𝐹( linC ‘𝑀)𝑉) = 𝑍)) | ||
Theorem | linc0scn0 47006* | If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑍, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) | ||
Theorem | lincdifsn 47007 | A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑉) = ((𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) + ((𝐹‘𝑋) · 𝑋))) | ||
Theorem | linc1 47008* | A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑋, 1 , 0 )) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹( linC ‘𝑀)𝑉) = 𝑋) | ||
Theorem | lincellss 47009 | A linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ((𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝐹 finSupp (0g‘(Scalar‘𝑀))) → (𝐹( linC ‘𝑀)𝑉) ∈ 𝑆)) | ||
Theorem | lco0 47010 | The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) = {(0g‘𝑀)}) | ||
Theorem | lcoel0 47011 | The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (0g‘𝑀) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincsum 47012 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ + = (+g‘𝑀) & ⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) & ⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ ✚ = (+g‘𝑆) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉)) | ||
Theorem | lincscm 47013* | A linear combinations multiplied with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 9-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ ∙ = ( ·𝑠 ‘𝑀) & ⊢ · = (.r‘(Scalar‘𝑀)) & ⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑆 · (𝐴‘𝑥))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp (0g‘(Scalar‘𝑀))) → (𝑆 ∙ 𝑋) = (𝐹( linC ‘𝑀)𝑉)) | ||
Theorem | lincsumcl 47014 | The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincscmcl 47015 | The multiplication of a linear combination with a scalar is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 11-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincsumscmcl 47016 | The sum of a linear combination and a multiplication of a linear combination with a scalar is a linear combination. (Contributed by AV, 11-Apr-2019.) |
⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝑅 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (𝑀 LinCo 𝑉) ∧ 𝐵 ∈ (𝑀 LinCo 𝑉))) → ((𝐶 · 𝐷) + 𝐵) ∈ (𝑀 LinCo 𝑉)) | ||
Theorem | lincolss 47017 | According to the statement in [Lang] p. 129, the set (LSubSp‘𝑀) of all linear combinations of a set of vectors V is a submodule (generated by V) of the module M. The elements of V are called generators of (LSubSp‘𝑀). (Contributed by AV, 12-Apr-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo 𝑉) ∈ (LSubSp‘𝑀)) | ||
Theorem | ellcoellss 47018* | Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ∀𝑥 ∈ (𝑀 LinCo 𝑉)𝑥 ∈ 𝑆) | ||
Theorem | lcoss 47019 | A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑉 ⊆ (𝑀 LinCo 𝑉)) | ||
Theorem | lspsslco 47020 | Lemma for lspeqlco 47022. (Contributed by AV, 17-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((LSpan‘𝑀)‘𝑉) ⊆ (𝑀 LinCo 𝑉)) | ||
Theorem | lcosslsp 47021 | Lemma for lspeqlco 47022. (Contributed by AV, 20-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) ⊆ ((LSpan‘𝑀)‘𝑉)) | ||
Theorem | lspeqlco 47022 | Equivalence of a span of a set of vectors of a left module defined as the intersection of all linear subspaces which each contain every vector in that set (see df-lsp 20571) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = ((LSpan‘𝑀)‘𝑉)) | ||
According to the definition in [Lang] p. 129: "A subset S of a module M is said
to be linearly independent (over [the ring] A) if whenever we have a
linear combination ∑x ∈S axx which is equal to
0, then ax=0 for all x∈S." This definition does not care for
the finiteness of the set S (because the definition of a linear combination
in [Lang] p.129 does already assure that only a finite number of coefficients
can be 0 in the sum). Our definition df-lininds 47025 does also neither claim that
the subset must be finite, nor that almost all coefficients within the linear
combination are 0. If this is required, it must be explicitly stated as
precondition in the corresponding theorems. | ||
Syntax | clininds 47023 | Extend class notation with the relation between a module and its linearly independent subsets. |
class linIndS | ||
Syntax | clindeps 47024 | Extend class notation with the relation between a module and its linearly dependent subsets. |
class linDepS | ||
Definition | df-lininds 47025* | Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ linIndS = {〈𝑠, 𝑚〉 ∣ (𝑠 ∈ 𝒫 (Base‘𝑚) ∧ ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑠)((𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))} | ||
Theorem | rellininds 47026 | The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019.) |
⊢ Rel linIndS | ||
Definition | df-lindeps 47027* | Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.) |
⊢ linDepS = {〈𝑠, 𝑚〉 ∣ ¬ 𝑠 linIndS 𝑚} | ||
Theorem | linindsv 47028 | The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ V ∧ 𝑀 ∈ V)) | ||
Theorem | islininds 47029* | The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) | ||
Theorem | linindsi 47030* | The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) | ||
Theorem | linindslinci 47031* | The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 linIndS 𝑀 ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ 𝐹 finSupp 0 ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍)) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) = 0 ) | ||
Theorem | islinindfis 47032* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) | ||
Theorem | islinindfiss 47033* | The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ Fin ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linIndS 𝑀 ↔ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) | ||
Theorem | linindscl 47034 | A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 (Base‘𝑀)) | ||
Theorem | lindepsnlininds 47035 | A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀)) | ||
Theorem | islindeps 47036* | The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ))) | ||
Theorem | lincext1 47037* | Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 29-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋})))) → 𝐹 ∈ (𝐸 ↑m 𝑆)) | ||
Theorem | lincext2 47038* | Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 ) | ||
Theorem | lincext3 47039* | Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠 ‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → (𝐹( linC ‘𝑀)𝑆) = 𝑍) | ||
Theorem | lindslinindsimp1 47040* | Implication 1 for lindslininds 47047. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))))) | ||
Theorem | lindslinindimp2lem1 47041* | Lemma 1 for lindslinindsimp2 47046. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝑌 ∈ 𝐵) | ||
Theorem | lindslinindimp2lem2 47042* | Lemma 2 for lindslinindsimp2 47046. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥}))) | ||
Theorem | lindslinindimp2lem3 47043* | Lemma 3 for lindslinindsimp2 47046. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 )) → 𝐺 finSupp 0 ) | ||
Theorem | lindslinindimp2lem4 47044* | Lemma 4 for lindslinindsimp2 47046. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)) | ||
Theorem | lindslinindsimp2lem5 47045* | Lemma 5 for lindslinindsimp2 47046. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) | ||
Theorem | lindslinindsimp2 47046* | Implication 2 for lindslininds 47047. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) ⇒ ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) | ||
Theorem | lindslininds 47047 | Equivalence of definitions df-linds 21346 and df-lininds 47025 for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 linIndS 𝑀 ↔ 𝑆 ∈ (LIndS‘𝑀))) | ||
Theorem | linds0 47048 | The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ (𝑀 ∈ 𝑉 → ∅ linIndS 𝑀) | ||
Theorem | el0ldep 47049 | A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ (((𝑀 ∈ LMod ∧ 1 < (♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝑆) → 𝑆 linDepS 𝑀) | ||
Theorem | el0ldepsnzr 47050 | A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
⊢ (((𝑀 ∈ LMod ∧ (Scalar‘𝑀) ∈ NzRing) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝑆) → 𝑆 linDepS 𝑀) | ||
Theorem | lindsrng01 47051 | Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 20473), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ ((♯‘𝐸) = 0 ∨ (♯‘𝐸) = 1) ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑆 linIndS 𝑀) | ||
Theorem | lindszr 47052 | Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019.) |
⊢ ((𝑀 ∈ LMod ∧ ¬ (Scalar‘𝑀) ∈ NzRing ∧ 𝑆 ∈ 𝒫 (Base‘𝑀)) → 𝑆 linIndS 𝑀) | ||
Theorem | snlindsntorlem 47053* | Lemma for snlindsntor 47054. (Contributed by AV, 15-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) | ||
Theorem | snlindsntor 47054* | A singleton is linearly independent iff it does not contain a torsion element. According to Wikipedia ("Torsion (algebra)", 15-Apr-2019, https://en.wikipedia.org/wiki/Torsion_(algebra)): "An element m of a module M over a ring R is called a torsion element of the module if there exists a regular element r of the ring (an element that is neither a left nor a right zero divisor) that annihilates m, i.e., (𝑟 · 𝑚) = 0. In an integral domain (a commutative ring without zero divisors), every nonzero element is regular, so a torsion element of a module over an integral domain is one annihilated by a nonzero element of the integral domain." Analogously, the definition in [Lang] p. 147 states that "An element x of [a module] E [over a ring R] is called a torsion element if there exists 𝑎 ∈ 𝑅, 𝑎 ≠ 0, such that 𝑎 · 𝑥 = 0. This definition includes the zero element of the module. Some authors, however, exclude the zero element from the definition of torsion elements. (Contributed by AV, 14-Apr-2019.) (Revised by AV, 27-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀)) | ||
Theorem | ldepsprlem 47055 | Lemma for ldepspr 47056. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍)) | ||
Theorem | ldepspr 47056 | If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 27-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀)) | ||
Theorem | lincresunit3lem3 47057 | Lemma 3 for lincresunit3 47064. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐴 ∈ 𝑈) → (((𝑁‘𝐴) · 𝑋) = ((𝑁‘𝐴) · 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lincresunitlem1 47058 | Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → (𝐼‘(𝑁‘(𝐹‘𝑋))) ∈ 𝐸) | ||
Theorem | lincresunitlem2 47059 | Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ ((((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) ∧ 𝑌 ∈ 𝑆) → ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑌)) ∈ 𝐸) | ||
Theorem | lincresunit1 47060* | Property 1 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈)) → 𝐺 ∈ (𝐸 ↑m (𝑆 ∖ {𝑋}))) | ||
Theorem | lincresunit2 47061* | Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → 𝐺 finSupp 0 ) | ||
Theorem | lincresunit3lem1 47062* | Lemma 1 for lincresunit3 47064. (Contributed by AV, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠 ‘𝑀)𝑧)) | ||
Theorem | lincresunit3lem2 47063* | Lemma 2 for lincresunit3 47064. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 )) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)(𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)))) = ((𝐹 ↾ (𝑆 ∖ {𝑋}))( linC ‘𝑀)(𝑆 ∖ {𝑋}))) | ||
Theorem | lincresunit3 47064* | Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋) | ||
Theorem | lincreslvec3 47065* | Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ≠ 0 ∧ 𝐹 finSupp 0 ) ∧ (𝐹( linC ‘𝑀)𝑆) = 𝑍) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = 𝑋) | ||
Theorem | islindeps2 47066* | Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → 𝑆 linDepS 𝑀)) | ||
Theorem | islininds2 47067* | Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (𝑆 linIndS 𝑀 → ∀𝑠 ∈ 𝑆 ∀𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑓 finSupp 0 ∨ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) ≠ 𝑠))) | ||
Theorem | isldepslvec2 47068* | Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 47066 holds, so that both definitions are equivalent (see theorem 1.6 in [Roman] p. 46 and the note in [Roman] p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑m (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ 𝑆 linDepS 𝑀)) | ||
Theorem | lindssnlvec 47069 | A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 28-Apr-2019.) |
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ (Base‘𝑀) ∧ 𝑆 ≠ (0g‘𝑀)) → {𝑆} linIndS 𝑀) | ||
Theorem | lmod1lem1 47070* | Lemma 1 for lmod1 47075. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)𝐼) ∈ {𝐼}) | ||
Theorem | lmod1lem2 47071* | Lemma 2 for lmod1 47075. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem3 47072* | Lemma 3 for lmod1 47075. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = ((𝑞( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem4 47073* | Lemma 4 for lmod1 47075. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = (𝑞( ·𝑠 ‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem5 47074* | Lemma 5 for lmod1 47075. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((1r‘(Scalar‘𝑀))( ·𝑠 ‘𝑀)𝐼) = 𝐼) | ||
Theorem | lmod1 47075* | The (smallest) structure representing a zero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑀 ∈ LMod) | ||
Theorem | lmod1zr 47076 | The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑅 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} & ⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod) | ||
Theorem | lmod1zrnlvec 47077 | There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑅 = {〈(Base‘ndx), {𝑍}〉, 〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉, 〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} & ⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∉ LVec) | ||
Theorem | lmodn0 47078 | Left modules exist. (Contributed by AV, 29-Apr-2019.) |
⊢ LMod ≠ ∅ | ||
Theorem | zlmodzxzequa 47079 | Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 0 = {〈0, 0〉, 〈1, 0〉} & ⊢ ∙ = ( ·𝑠 ‘𝑍) & ⊢ − = (-g‘𝑍) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ ((2 ∙ 𝐴) − (3 ∙ 𝐵)) = 0 | ||
Theorem | zlmodzxznm 47080 | Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 112). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 0 = {〈0, 0〉, 〈1, 0〉} & ⊢ ∙ = ( ·𝑠 ‘𝑍) & ⊢ − = (-g‘𝑍) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴) | ||
Theorem | zlmodzxzldeplem 47081 | A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
Theorem | zlmodzxzequap 47082 | Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} & ⊢ 0 = {〈0, 0〉, 〈1, 0〉} & ⊢ + = (+g‘𝑍) & ⊢ ∙ = ( ·𝑠 ‘𝑍) ⇒ ⊢ ((2 ∙ 𝐴) + (-3 ∙ 𝐵)) = 0 | ||
Theorem | zlmodzxzldeplem1 47083 | Lemma 1 for zlmodzxzldep 47087. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} & ⊢ 𝐹 = {〈𝐴, 2〉, 〈𝐵, -3〉} ⇒ ⊢ 𝐹 ∈ (ℤ ↑m {𝐴, 𝐵}) | ||
Theorem | zlmodzxzldeplem2 47084 | Lemma 2 for zlmodzxzldep 47087. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} & ⊢ 𝐹 = {〈𝐴, 2〉, 〈𝐵, -3〉} ⇒ ⊢ 𝐹 finSupp 0 | ||
Theorem | zlmodzxzldeplem3 47085 | Lemma 3 for zlmodzxzldep 47087. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} & ⊢ 𝐹 = {〈𝐴, 2〉, 〈𝐵, -3〉} ⇒ ⊢ (𝐹( linC ‘𝑍){𝐴, 𝐵}) = (0g‘𝑍) | ||
Theorem | zlmodzxzldeplem4 47086* | Lemma 4 for zlmodzxzldep 47087. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} & ⊢ 𝐹 = {〈𝐴, 2〉, 〈𝐵, -3〉} ⇒ ⊢ ∃𝑦 ∈ {𝐴, 𝐵} (𝐹‘𝑦) ≠ 0 | ||
Theorem | zlmodzxzldep 47087 | { A , B } is a linearly dependent set within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ {𝐴, 𝐵} linDepS 𝑍 | ||
Theorem | ldepsnlinclem1 47088 | Lemma 1 for ldepsnlinc 47091. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐵}) → (𝐹( linC ‘𝑍){𝐵}) ≠ 𝐴) | ||
Theorem | ldepsnlinclem2 47089 | Lemma 2 for ldepsnlinc 47091. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑍 = (ℤring freeLMod {0, 1}) & ⊢ 𝐴 = {〈0, 3〉, 〈1, 6〉} & ⊢ 𝐵 = {〈0, 2〉, 〈1, 4〉} ⇒ ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐴}) → (𝐹( linC ‘𝑍){𝐴}) ≠ 𝐵) | ||
Theorem | lvecpsslmod 47090 | The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 20705) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 47077. (Contributed by AV, 29-Apr-2019.) |
⊢ LVec ⊊ LMod | ||
Theorem | ldepsnlinc 47091* | The reverse implication of islindeps2 47066 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 47079 and zlmodzxznm 47080. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) | ||
Theorem | ldepslinc 47092* | For (left) vector spaces, isldepslvec2 47068 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 47091 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ (∀𝑚 ∈ LVec ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)) ∧ ¬ ∀𝑚 ∈ LMod ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣))) | ||
Theorem | suppdm 47093 | If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.) |
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑍 ∉ ran 𝐹) → (𝐹 supp 𝑍) = dom 𝐹) | ||
Theorem | eluz2cnn0n1 47094 | An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.) |
⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ (ℂ ∖ {0, 1})) | ||
Theorem | divge1b 47095 | The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 1 ≤ (𝐵 / 𝐴))) | ||
Theorem | divgt1b 47096 | The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 1 < (𝐵 / 𝐴))) | ||
Theorem | ltsubaddb 47097 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | ltsubsubb 47098 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | ltsubadd2b 47099 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | divsub1dir 47100 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |