![]() |
Metamath
Proof Explorer Theorem List (p. 453 of 457) | < 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-28785) |
![]() (28786-30308) |
![]() (30309-45683) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-lininds 45201* | 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 45202 | 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 45203* | Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.) |
⊢ linDepS = {〈𝑠, 𝑚〉 ∣ ¬ 𝑠 linIndS 𝑚} | ||
Theorem | linindsv 45204 | The classes of the module and its linearly independent subsets are sets. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → (𝑆 ∈ V ∧ 𝑀 ∈ V)) | ||
Theorem | islininds 45205* | 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 45206* | 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 45207* | 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 45208* | 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 45209* | 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 45210 | A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019.) |
⊢ (𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 (Base‘𝑀)) | ||
Theorem | lindepsnlininds 45211 | A linearly dependent subset is not a linearly independent subset. (Contributed by AV, 26-Apr-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀)) | ||
Theorem | islindeps 45212* | 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 45213* | 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 45214* | 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 45215* | 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 45216* | Implication 1 for lindslininds 45223. (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 45217* | Lemma 1 for lindslinindsimp2 45222. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝑌 ∈ 𝐵) | ||
Theorem | lindslinindimp2lem2 45218* | Lemma 2 for lindslinindsimp2 45222. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥}))) | ||
Theorem | lindslinindimp2lem3 45219* | Lemma 3 for lindslinindsimp2 45222. (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 45220* | Lemma 4 for lindslinindsimp2 45222. (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 45221* | Lemma 5 for lindslinindsimp2 45222. (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 45222* | Implication 2 for lindslininds 45223. (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 45223 | Equivalence of definitions df-linds 20557 and df-lininds 45201 for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 linIndS 𝑀 ↔ 𝑆 ∈ (LIndS‘𝑀))) | ||
Theorem | linds0 45224 | 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 45225 | 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 45226 | 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 45227 | 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 19700), 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 45228 | 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 45229* | Lemma for snlindsntor 45230. (Contributed by AV, 15-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) | ||
Theorem | snlindsntor 45230* | 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 45231 | Lemma for ldepspr 45232. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍)) | ||
Theorem | ldepspr 45232 | 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 45233 | Lemma 3 for lincresunit3 45240. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐴 ∈ 𝑈) → (((𝑁‘𝐴) · 𝑋) = ((𝑁‘𝐴) · 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lincresunitlem1 45234 | 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 45235 | 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 45236* | 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 45237* | 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 45238* | Lemma 1 for lincresunit3 45240. (Contributed by AV, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠 ‘𝑀)𝑧)) | ||
Theorem | lincresunit3lem2 45239* | Lemma 2 for lincresunit3 45240. (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 45240* | 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 45241* | 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 45242* | 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 45243* | 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 45244* | Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 45242 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 45245 | 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 45246* | Lemma 1 for lmod1 45251. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)𝐼) ∈ {𝐼}) | ||
Theorem | lmod1lem2 45247* | Lemma 2 for lmod1 45251. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem3 45248* | Lemma 3 for lmod1 45251. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = ((𝑞( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem4 45249* | Lemma 4 for lmod1 45251. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = (𝑞( ·𝑠 ‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem5 45250* | Lemma 5 for lmod1 45251. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((1r‘(Scalar‘𝑀))( ·𝑠 ‘𝑀)𝐼) = 𝐼) | ||
Theorem | lmod1 45251* | 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 45252 | 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 45253 | 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 45254 | Left modules exist. (Contributed by AV, 29-Apr-2019.) |
⊢ LMod ≠ ∅ | ||
Theorem | zlmodzxzequa 45255 | 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 45256 | 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 45257 | 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 45258 | 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 45259 | Lemma 1 for zlmodzxzldep 45263. (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 45260 | Lemma 2 for zlmodzxzldep 45263. (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 45261 | Lemma 3 for zlmodzxzldep 45263. (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 45262* | Lemma 4 for zlmodzxzldep 45263. (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 45263 | { 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 45264 | Lemma 1 for ldepsnlinc 45267. (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 45265 | Lemma 2 for ldepsnlinc 45267. (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 45266 | 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 19931) 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 45253. (Contributed by AV, 29-Apr-2019.) |
⊢ LVec ⊊ LMod | ||
Theorem | ldepsnlinc 45267* | The reverse implication of islindeps2 45242 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 45255 and zlmodzxznm 45256. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) | ||
Theorem | ldepslinc 45268* | For (left) vector spaces, isldepslvec2 45244 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 45267 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 45269 | 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 45270 | 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 45271 | 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 45272 | 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 45273 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | ltsubsubb 45274 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | ltsubadd2b 45275 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | divsub1dir 45276 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵)) | ||
Theorem | expnegico01 45277 | An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0) → (𝐵↑𝑁) ∈ (0[,)1)) | ||
Theorem | elfzolborelfzop1 45278 | An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) | ||
Theorem | pw2m1lepw2m1 45279 | 2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.) |
⊢ (𝐼 ∈ ℕ → (2↑(𝐼 − 1)) ≤ ((2↑𝐼) − 1)) | ||
Theorem | zgtp1leeq 45280 | If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 − 1) < 𝐼 ∧ 𝐼 ≤ 𝐴) → 𝐼 = 𝐴)) | ||
Theorem | flsubz 45281 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁)) | ||
Theorem | fldivmod 45282 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵)) | ||
Theorem | mod0mul 45283* | If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) = 0 → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁))) | ||
Theorem | modn0mul 45284* | If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦))) | ||
Theorem | m1modmmod 45285 | An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1)) | ||
Theorem | difmodm1lt 45286 | The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd 𝐴 and 𝑁 = 2, since ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) would be (1 − 0) = 1 which is not less than (𝑁 − 1) = 1. (Contributed by AV, 6-Jun-2012.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1)) | ||
Theorem | nn0onn0ex 45287* | For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = ((2 · 𝑚) + 1)) | ||
Theorem | nn0enn0ex 45288* | For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = (2 · 𝑚)) | ||
Theorem | nnennex 45289* | For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ) → ∃𝑚 ∈ ℕ 𝑁 = (2 · 𝑚)) | ||
Theorem | nneop 45290 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ)) | ||
Theorem | nneom 45291 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0eo 45292 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0)) | ||
Theorem | nnpw2even 45293 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ) | ||
Theorem | zefldiv2 45294 | The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = (𝑁 / 2)) | ||
Theorem | zofldiv2 45295 | The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2)) | ||
Theorem | nn0ofldiv2 45296 | The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) (Proof shortened by AV, 7-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2)) | ||
Theorem | flnn0div2ge 45297 | The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2))) | ||
Theorem | flnn0ohalf 45298 | The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = (⌊‘((𝑁 − 1) / 2))) | ||
Theorem | logcxp0 45299 | Logarithm of a complex power. Generalization of logcxp 25344. (Contributed by AV, 22-May-2020.) |
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | regt1loggt0 45300 | The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |