![]() |
Metamath
Proof Explorer Theorem List (p. 484 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lincext3 48301* | 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 48302* | Implication 1 for lindslininds 48309. (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 48303* | Lemma 1 for lindslinindsimp2 48308. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝑌 ∈ 𝐵) | ||
Theorem | lindslinindimp2lem2 48304* | Lemma 2 for lindslinindsimp2 48308. (Contributed by AV, 25-Apr-2019.) |
⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) & ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥}))) | ||
Theorem | lindslinindimp2lem3 48305* | Lemma 3 for lindslinindsimp2 48308. (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 48306* | Lemma 4 for lindslinindsimp2 48308. (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 48307* | Lemma 5 for lindslinindsimp2 48308. (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 48308* | Implication 2 for lindslininds 48309. (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 48309 | Equivalence of definitions df-linds 21844 and df-lininds 48287 for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019.) (Proof shortened by AV, 30-Jul-2019.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 linIndS 𝑀 ↔ 𝑆 ∈ (LIndS‘𝑀))) | ||
Theorem | linds0 48310 | 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 48311 | 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 48312 | 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 48313 | 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 20888), 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 48314 | 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 48315* | Lemma for snlindsntor 48316. (Contributed by AV, 15-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) | ||
Theorem | snlindsntor 48316* | 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 48317 | Lemma for ldepspr 48318. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝑆 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) ⇒ ⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (( 1 · 𝑋)(+g‘𝑀)((𝑁‘𝐴) · 𝑌)) = 𝑍)) | ||
Theorem | ldepspr 48318 | 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 48319 | Lemma 3 for lincresunit3 48326. (Contributed by AV, 18-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑀) ⇒ ⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐴 ∈ 𝑈) → (((𝑁‘𝐴) · 𝑋) = ((𝑁‘𝐴) · 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lincresunitlem1 48320 | 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 48321 | 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 48322* | 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 48323* | 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 48324* | Lemma 1 for lincresunit3 48326. (Contributed by AV, 17-May-2019.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑅 = (Scalar‘𝑀) & ⊢ 𝐸 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (𝑠 ∈ (𝑆 ∖ {𝑋}) ↦ ((𝐼‘(𝑁‘(𝐹‘𝑋))) · (𝐹‘𝑠))) ⇒ ⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑m 𝑆) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ 𝑧 ∈ (𝑆 ∖ {𝑋}))) → ((𝑁‘(𝐹‘𝑋))( ·𝑠 ‘𝑀)((𝐺‘𝑧)( ·𝑠 ‘𝑀)𝑧)) = ((𝐹‘𝑧)( ·𝑠 ‘𝑀)𝑧)) | ||
Theorem | lincresunit3lem2 48325* | Lemma 2 for lincresunit3 48326. (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 48326* | 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 48327* | 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 48328* | 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 48329* | 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 48330* | Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 48328 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 48331 | 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 48332* | Lemma 1 for lmod1 48337. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)𝐼) ∈ {𝐼}) | ||
Theorem | lmod1lem2 48333* | Lemma 2 for lmod1 48337. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠 ‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem3 48334* | Lemma 3 for lmod1 48337. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = ((𝑞( ·𝑠 ‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem4 48335* | Lemma 4 for lmod1 48337. (Contributed by AV, 29-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠 ‘𝑀)𝐼) = (𝑞( ·𝑠 ‘𝑀)(𝑟( ·𝑠 ‘𝑀)𝐼))) | ||
Theorem | lmod1lem5 48336* | Lemma 5 for lmod1 48337. (Contributed by AV, 28-Apr-2019.) |
⊢ 𝑀 = ({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx), 𝑅〉} ∪ {〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((1r‘(Scalar‘𝑀))( ·𝑠 ‘𝑀)𝐼) = 𝐼) | ||
Theorem | lmod1 48337* | 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 48338 | 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 48339 | 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 48340 | Left modules exist. (Contributed by AV, 29-Apr-2019.) |
⊢ LMod ≠ ∅ | ||
Theorem | zlmodzxzequa 48341 | 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 48342 | 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 48343 | 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 48344 | 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 48345 | Lemma 1 for zlmodzxzldep 48349. (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 48346 | Lemma 2 for zlmodzxzldep 48349. (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 48347 | Lemma 3 for zlmodzxzldep 48349. (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 48348* | Lemma 4 for zlmodzxzldep 48349. (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 48349 | { 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 48350 | Lemma 1 for ldepsnlinc 48353. (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 48351 | Lemma 2 for ldepsnlinc 48353. (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 48352 | 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 21122) 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 48339. (Contributed by AV, 29-Apr-2019.) |
⊢ LVec ⊊ LMod | ||
Theorem | ldepsnlinc 48353* | The reverse implication of islindeps2 48328 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 combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 48341 and zlmodzxznm 48342. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) | ||
Theorem | ldepslinc 48354* | For (left) vector spaces, isldepslvec2 48330 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 48353 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 48355 | 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 48356 | 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 48357 | 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 48358 | 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 48359 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | ltsubsubb 48360 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | ltsubadd2b 48361 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | divsub1dir 48362 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵)) | ||
Theorem | expnegico01 48363 | 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 48364 | 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 48365 | 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 48366 | 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 48367 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁)) | ||
Theorem | mod0mul 48368* | 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 48369* | 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 48370 | 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 48371 | 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 48372* | 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 48373* | 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 48374* | 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 48375 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ)) | ||
Theorem | nneom 48376 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0eo 48377 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0)) | ||
Theorem | nnpw2even 48378 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ) | ||
Theorem | zefldiv2 48379 | 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 48380 | 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 48381 | 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 48382 | 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 48383 | 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 48384 | Logarithm of a complex power. Generalization of logcxp 26725. (Contributed by AV, 22-May-2020.) |
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | regt1loggt0 48385 | The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵)) | ||
Syntax | cfdiv 48386 | Extend class notation with the division operator of two functions. |
class /f | ||
Definition | df-fdiv 48387* | Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0))) | ||
Theorem | fdivval 48388 | The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘f / 𝐺) ↾ (𝐺 supp 0))) | ||
Theorem | fdivmpt 48389* | The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥)))) | ||
Theorem | fdivmptf 48390 | The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℂ) | ||
Theorem | refdivmptf 48391 | The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) | ||
Theorem | fdivpm 48392 | The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴)) | ||
Theorem | refdivpm 48393 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴)) | ||
Theorem | fdivmptfv 48394 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Theorem | refdivmptfv 48395 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Syntax | cbigo 48396 | Extend class notation with the class of the "big-O" function. |
class Ο | ||
Definition | df-bigo 48397* | Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalization of "big-O of one", see df-o1 15522 and df-lo1 15523. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 48406. (Contributed by AV, 15-May-2020.) |
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}) | ||
Theorem | bigoval 48398* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))}) | ||
Theorem | elbigofrcl 48399 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ)) | ||
Theorem | elbigo 48400* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |