![]() |
Metamath
Proof Explorer Theorem List (p. 199 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmodvsinv 19801 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | lmodvsinv2 19802 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | islmhm2 19803* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 19697. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐸 = (Base‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧))))) | ||
Theorem | islmhmd 19804* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐽 = (Scalar‘𝑇) & ⊢ 𝑁 = (Base‘𝐾) & ⊢ (𝜑 → 𝑆 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐽 = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | 0lmhm 19805 | The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 0 = (0g‘𝑁) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝑇 = (Scalar‘𝑁) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇) → (𝐵 × { 0 }) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | idlmhm 19806 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → ( I ↾ 𝐵) ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | invlmhm 19807 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐼 = (invg‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐼 ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | lmhmco 19808 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘ 𝐺) ∈ (𝑀 LMHom 𝑂)) | ||
Theorem | lmhmplusg 19809 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ + = (+g‘𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | lmhmvsca 19810 | The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑁) & ⊢ 𝐽 = (Scalar‘𝑁) & ⊢ 𝐾 = (Base‘𝐽) ⇒ ⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | lmhmf1o 19811 | A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆))) | ||
Theorem | lmhmima 19812 | The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌) | ||
Theorem | lmhmpreima 19813 | The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) | ||
Theorem | lmhmlsp 19814 | Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐾 = (LSpan‘𝑆) & ⊢ 𝐿 = (LSpan‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈))) | ||
Theorem | lmhmrnlss 19815 | The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) | ||
Theorem | lmhmkerlss 19816 | The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈) | ||
Theorem | reslmhm 19817 | Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) & ⊢ 𝑅 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇)) | ||
Theorem | reslmhm2 19818 | Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) & ⊢ 𝐿 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑈) ∧ 𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | reslmhm2b 19819 | Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) & ⊢ 𝐿 = (LSubSp‘𝑇) ⇒ ⊢ ((𝑇 ∈ LMod ∧ 𝑋 ∈ 𝐿 ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ 𝐹 ∈ (𝑆 LMHom 𝑈))) | ||
Theorem | lmhmeql 19820 | The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈) | ||
Theorem | lspextmo 19821* | A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐾 = (LSpan‘𝑆) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ (𝐾‘𝑋) = 𝐵) → ∃*𝑔 ∈ (𝑆 LMHom 𝑇)(𝑔 ↾ 𝑋) = 𝐹) | ||
Theorem | pwsdiaglmhm 19822* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 LMHom 𝑌)) | ||
Theorem | pwssplit0 19823* | Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶) | ||
Theorem | pwssplit1 19824* | Splitting for structure powers, part 1: restriction is an onto function. The only actual monoid law we need here is that the base set is nonempty. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵–onto→𝐶) | ||
Theorem | pwssplit2 19825* | Splitting for structure powers, part 2: restriction is a group homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 GrpHom 𝑍)) | ||
Theorem | pwssplit3 19826* | Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 LMHom 𝑍)) | ||
Theorem | islmim 19827 | An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)) | ||
Theorem | lmimf1o 19828 | An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | lmimlmhm 19829 | An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 LMHom 𝑆)) | ||
Theorem | lmimgim 19830 | An isomorphism of modules is an isomorphism of groups. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 GrpIso 𝑆)) | ||
Theorem | islmim2 19831 | An isomorphism of left modules is a homomorphism whose converse is a homomorphism. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) ↔ (𝐹 ∈ (𝑅 LMHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 LMHom 𝑅))) | ||
Theorem | lmimcnv 19832 | The converse of a bijective module homomorphism is a bijective module homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑆 LMIso 𝑇) → ◡𝐹 ∈ (𝑇 LMIso 𝑆)) | ||
Theorem | brlmic 19833 | The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 ↔ (𝑅 LMIso 𝑆) ≠ ∅) | ||
Theorem | brlmici 19834 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝑅 ≃𝑚 𝑆) | ||
Theorem | lmiclcl 19835 | Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑅 ∈ LMod) | ||
Theorem | lmicrcl 19836 | Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ∈ LMod) | ||
Theorem | lmicsym 19837 | Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅) | ||
Theorem | lmhmpropd 19838* | Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐽)) & ⊢ (𝜑 → 𝐺 = (Scalar‘𝐾)) & ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿)) & ⊢ (𝜑 → 𝐺 = (Scalar‘𝑀)) & ⊢ 𝑃 = (Base‘𝐹) & ⊢ 𝑄 = (Base‘𝐺) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐽)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝐶)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 LMHom 𝐾) = (𝐿 LMHom 𝑀)) | ||
Syntax | clbs 19839 | Extend class notation with the set of bases for a vector space. |
class LBasis | ||
Definition | df-lbs 19840* | Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) | ||
Theorem | islbs 19841* | The predicate "𝐵 is a basis for the left module or vector space 𝑊". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) | ||
Theorem | lbsss 19842 | A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉) | ||
Theorem | lbsel 19843 | An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → 𝐸 ∈ 𝑉) | ||
Theorem | lbssp 19844 | The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉) | ||
Theorem | lbsind 19845 | A basis is linearly independent; that is, every element has a span which trivially intersects the span of the remainder of the basis. (Contributed by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ¬ (𝐴 · 𝐸) ∈ (𝑁‘(𝐵 ∖ {𝐸}))) | ||
Theorem | lbsind2 19846 | A basis is linearly independent; that is, every element is not in the span of the remainder of the basis. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 1 = (1r‘𝐹) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → ¬ 𝐸 ∈ (𝑁‘(𝐵 ∖ {𝐸}))) | ||
Theorem | lbspss 19847 | No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 1 = (1r‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵) → (𝑁‘𝐶) ≠ 𝑉) | ||
Theorem | lsmcl 19848 | The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) ∈ 𝑆) | ||
Theorem | lsmspsn 19849* | Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈 ∈ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ↔ ∃𝑗 ∈ 𝐾 ∃𝑘 ∈ 𝐾 𝑈 = ((𝑗 · 𝑋) + (𝑘 · 𝑌)))) | ||
Theorem | lsmelval2 19850* | Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | ||
Theorem | lsmsp 19851 | Subspace sum in terms of span. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑁‘(𝑇 ∪ 𝑈))) | ||
Theorem | lsmsp2 19852 | Subspace sum of spans of subsets is the span of their union. (spanuni 29327 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉) → ((𝑁‘𝑇) ⊕ (𝑁‘𝑈)) = (𝑁‘(𝑇 ∪ 𝑈))) | ||
Theorem | lsmssspx 19853 | Subspace sum (in its extended domain) is a subset of the span of the union of its arguments. (Contributed by NM, 6-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑇 ⊆ 𝑉) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝑇 ⊕ 𝑈) ⊆ (𝑁‘(𝑇 ∪ 𝑈))) | ||
Theorem | lsmpr 19854 | The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌}))) | ||
Theorem | lsppreli 19855 | A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) + (𝐵 · 𝑌)) ∈ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lsmelpr 19856 | Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})))) | ||
Theorem | lsppr0 19857 | The span of a vector paired with zero equals the span of the singleton of the vector. (Contributed by NM, 29-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 0 }) = (𝑁‘{𝑋})) | ||
Theorem | lsppr 19858* | Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑣 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))}) | ||
Theorem | lspprel 19859* | Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑍 = ((𝑘 · 𝑋) + (𝑙 · 𝑌)))) | ||
Theorem | lspprabs 19860 | Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspvadd 19861 | The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ⊆ (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspsntri 19862 | Triangle-type inequality for span of a singleton. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 + 𝑌)}) ⊆ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌}))) | ||
Theorem | lspsntrim 19863 | Triangle-type inequality for span of a singleton of vector difference. (Contributed by NM, 25-Apr-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑁‘{(𝑋 − 𝑌)}) ⊆ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌}))) | ||
Theorem | lbspropd 19864* | If two structures have the same components (properties), they have the same set of bases. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐿 ∈ 𝑌) ⇒ ⊢ (𝜑 → (LBasis‘𝐾) = (LBasis‘𝐿)) | ||
Theorem | pj1lmhm 19865 | The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝐿) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom 𝑊)) | ||
Theorem | pj1lmhm2 19866 | The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ 𝐿) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝑊 ↾s (𝑇 ⊕ 𝑈)) LMHom (𝑊 ↾s 𝑇))) | ||
Syntax | clvec 19867 | Extend class notation with class of all left vector spaces. |
class LVec | ||
Definition | df-lvec 19868 | Define the class of all left vector spaces. A left vector space over a division ring is an Abelian group (vectors) together with a division ring (scalars) and a left scalar product connecting them. Some authors call this a "left module over a division ring", reserving "vector space" for those where the division ring is commutative, i.e., is a field. (Contributed by NM, 11-Nov-2013.) |
⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing} | ||
Theorem | islvec 19869 | The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) | ||
Theorem | lvecdrng 19870 | The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) | ||
Theorem | lveclmod 19871 | A left vector space is a left module. (Contributed by NM, 9-Dec-2013.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | ||
Theorem | lsslvec 19872 | A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LVec) | ||
Theorem | lvecvs0or 19873 | If a scalar product is zero, one of its factors must be zero. (hvmul0or 28808 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = 0 ↔ (𝐴 = 𝑂 ∨ 𝑋 = 0 ))) | ||
Theorem | lvecvsn0 19874 | A scalar product is nonzero iff both of its factors are nonzero. (Contributed by NM, 3-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) ≠ 0 ↔ (𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 ))) | ||
Theorem | lssvs0or 19875 | If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) ∈ 𝑈 ↔ (𝐴 = 0 ∨ 𝑋 ∈ 𝑈))) | ||
Theorem | lvecvscan 19876 | Cancellation law for scalar multiplication. (hvmulcan 28855 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐴 · 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lvecvscan2 19877 | Cancellation law for scalar multiplication. (hvmulcan2 28856 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = (𝐵 · 𝑋) ↔ 𝐴 = 𝐵)) | ||
Theorem | lvecinv 19878 | Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝐼 = (invr‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ∖ { 0 })) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 = (𝐴 · 𝑌) ↔ 𝑌 = ((𝐼‘𝐴) · 𝑋))) | ||
Theorem | lspsnvs 19879 | A nonzero scalar product does not change the span of a singleton. (spansncol 29351 analog.) (Contributed by NM, 23-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 0 = (0g‘𝐹) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ≠ 0 ) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{(𝑅 · 𝑋)}) = (𝑁‘{𝑋})) | ||
Theorem | lspsneleq 19880 | Membership relation that implies equality of spans. (spansneleq 29353 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑋})) | ||
Theorem | lspsncmp 19881 | Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) | ||
Theorem | lspsnne1 19882 | Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) | ||
Theorem | lspsnne2 19883 | Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | ||
Theorem | lspsnnecom 19884 | Swap two vectors with different spans. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋})) | ||
Theorem | lspabs2 19885 | Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) | ||
Theorem | lspabs3 19886 | Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{(𝑋 + 𝑌)})) | ||
Theorem | lspsneq 19887* | Equal spans of singletons must have proportional vectors. See lspsnss2 19770 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑘 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsneu 19888* | Nonzero vectors with equal singleton spans have a unique proportionality constant. (Contributed by NM, 31-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑂 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃!𝑘 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑘 · 𝑌))) | ||
Theorem | lspsnel4 19889 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn4 29356 analog.) (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋})) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈)) | ||
Theorem | lspdisj 19890 | The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 }) | ||
Theorem | lspdisjb 19891 | A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 })) | ||
Theorem | lspdisj2 19892 | Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ (𝑁‘{𝑌})) = { 0 }) | ||
Theorem | lspfixed 19893* | Show membership in the span of the sum of two vectors, one of which (𝑌) is fixed in advance. (Contributed by NM, 27-May-2015.) (Revised by AV, 12-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) | ||
Theorem | lspexch 19894 | Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 19895 versus lspexchn2 19896); look for lspexch 19894 and prcom 4628 in same proof. TODO: would a hypothesis of ¬ 𝑋 ∈ (𝑁‘{𝑍}) instead of (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}) be better overall? This would be shorter and also satisfy the 𝑋 ≠ 0 condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the ≠ pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})) & ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑍})) | ||
Theorem | lspexchn1 19895 | Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 19894 to see if this will shorten proofs. (Contributed by NM, 20-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑍})) | ||
Theorem | lspexchn2 19896 | Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch 19894 to see if this will shorten proofs. (Contributed by NM, 24-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍})) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌})) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋})) | ||
Theorem | lspindpi 19897 | Partial independence property. (Contributed by NM, 23-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))) | ||
Theorem | lspindp1 19898 | Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑌}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑍, 𝑌}))) | ||
Theorem | lspindp2l 19899 | Alternate way to say 3 vectors are mutually independent (rotate left). (Contributed by NM, 10-May-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))) | ||
Theorem | lspindp2 19900 | Alternate way to say 3 vectors are mutually independent (rotate right). (Contributed by NM, 12-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}) ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑋}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |