![]() |
Metamath
Proof Explorer Theorem List (p. 207 of 477) | < 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-30136) |
![]() (30137-31659) |
![]() (31660-47692) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lspsneq0b 20601 | Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 = 0 ↔ 𝑌 = 0 )) | ||
Theorem | lmodindp1 20602 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≠ 0 ) | ||
Theorem | lsslsp 20603 | Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap 𝑀‘𝐺 and 𝑁‘𝐺 since we are computing a property of 𝑁‘𝐺? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015. |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑀 = (LSpan‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑋) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈) → (𝑀‘𝐺) = (𝑁‘𝐺)) | ||
Theorem | lss0v 20604 | The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑍 = (0g‘𝑋) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) → 𝑍 = 0 ) | ||
Theorem | lsspropd 20605* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) ⇒ ⊢ (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿)) | ||
Theorem | lsppropd 20606* | If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) & ⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐿 ∈ 𝑌) ⇒ ⊢ (𝜑 → (LSpan‘𝐾) = (LSpan‘𝐿)) | ||
Syntax | clmhm 20607 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 20608 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 20609 | The class of the left module isomorphism relation. |
class ≃𝑚 | ||
Definition | df-lmhm 20610* | A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))}) | ||
Definition | df-lmim 20611* | An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ LMIso = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}) | ||
Definition | df-lmic 20612 | Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ≃𝑚 = (◡ LMIso “ (V ∖ 1o)) | ||
Theorem | reldmlmhm 20613 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ Rel dom LMHom | ||
Theorem | lmimfn 20614 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ LMIso Fn (LMod × LMod) | ||
Theorem | islmhm 20615* | Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))))) | ||
Theorem | islmhm3 20616* | Property of a module homomorphism, similar to ismhm 18660. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐸 (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))))) | ||
Theorem | lmhmlem 20617 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾))) | ||
Theorem | lmhmsca 20618 | A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾) | ||
Theorem | lmghm 20619 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | lmhmlmod2 20620 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | ||
Theorem | lmhmlmod1 20621 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | ||
Theorem | lmhmf 20622 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | lmhmlin 20623 | A homomorphism of left modules is 𝐾-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐸 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (𝐹‘(𝑋 · 𝑌)) = (𝑋 × (𝐹‘𝑌))) | ||
Theorem | lmodvsinv 20624 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝑀 = (invg‘𝐹) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑅) · 𝑋) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | lmodvsinv2 20625 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (invg‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵) → (𝑅 · (𝑁‘𝑋)) = (𝑁‘(𝑅 · 𝑋))) | ||
Theorem | islmhm2 20626* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20520. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐿 = (Scalar‘𝑇) & ⊢ 𝐸 = (Base‘𝐾) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) ⇒ ⊢ ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) → (𝐹 ∈ (𝑆 LMHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐿 = 𝐾 ∧ ∀𝑥 ∈ 𝐸 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝐹‘((𝑥 · 𝑦) + 𝑧)) = ((𝑥 × (𝐹‘𝑦)) ⨣ (𝐹‘𝑧))))) | ||
Theorem | islmhmd 20627* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑆) & ⊢ × = ( ·𝑠 ‘𝑇) & ⊢ 𝐾 = (Scalar‘𝑆) & ⊢ 𝐽 = (Scalar‘𝑇) & ⊢ 𝑁 = (Base‘𝐾) & ⊢ (𝜑 → 𝑆 ∈ LMod) & ⊢ (𝜑 → 𝑇 ∈ LMod) & ⊢ (𝜑 → 𝐽 = 𝐾) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 · 𝑦)) = (𝑥 × (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | 0lmhm 20628 | 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 20629 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → ( I ↾ 𝐵) ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | invlmhm 20630 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐼 = (invg‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐼 ∈ (𝑀 LMHom 𝑀)) | ||
Theorem | lmhmco 20631 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘ 𝐺) ∈ (𝑀 LMHom 𝑂)) | ||
Theorem | lmhmplusg 20632 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ + = (+g‘𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | lmhmvsca 20633 | 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 20634 | 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 20635 | The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌) | ||
Theorem | lmhmpreima 20636 | The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (LSubSp‘𝑆) & ⊢ 𝑌 = (LSubSp‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) | ||
Theorem | lmhmlsp 20637 | Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐾 = (LSpan‘𝑆) & ⊢ 𝐿 = (LSpan‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ⊆ 𝑉) → (𝐹 “ (𝐾‘𝑈)) = (𝐿‘(𝐹 “ 𝑈))) | ||
Theorem | lmhmrnlss 20638 | The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) | ||
Theorem | lmhmkerlss 20639 | The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈) | ||
Theorem | reslmhm 20640 | Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) & ⊢ 𝑅 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇)) | ||
Theorem | reslmhm2 20641 | 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 20642 | 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 20643 | The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈) | ||
Theorem | lspextmo 20644* | 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 20645* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 LMHom 𝑌)) | ||
Theorem | pwssplit0 20646* | Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝑈) & ⊢ 𝑍 = (𝑊 ↑s 𝑉) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) ⇒ ⊢ ((𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶) | ||
Theorem | pwssplit1 20647* | 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 20648* | 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 20649* | 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 20650 | 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 20651 | An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | lmimlmhm 20652 | An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝐹 ∈ (𝑅 LMHom 𝑆)) | ||
Theorem | lmimgim 20653 | 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 20654 | 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 20655 | 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 20656 | The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 ↔ (𝑅 LMIso 𝑆) ≠ ∅) | ||
Theorem | brlmici 20657 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 LMIso 𝑆) → 𝑅 ≃𝑚 𝑆) | ||
Theorem | lmiclcl 20658 | Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑅 ∈ LMod) | ||
Theorem | lmicrcl 20659 | Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ∈ LMod) | ||
Theorem | lmicsym 20660 | Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → 𝑆 ≃𝑚 𝑅) | ||
Theorem | lmhmpropd 20661* | 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 20662 | Extend class notation with the set of bases for a vector space. |
class LBasis | ||
Definition | df-lbs 20663* | 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 20664* | 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 20665 | A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉) | ||
Theorem | lbsel 20666 | An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) ⇒ ⊢ ((𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵) → 𝐸 ∈ 𝑉) | ||
Theorem | lbssp 20667 | The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝐵 ∈ 𝐽 → (𝑁‘𝐵) = 𝑉) | ||
Theorem | lbsind 20668 | 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 20669 | 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 20670 | 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 20671 | 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 20672* | Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈 ∈ ((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ↔ ∃𝑗 ∈ 𝐾 ∃𝑘 ∈ 𝐾 𝑈 = ((𝑗 · 𝑋) + (𝑘 · 𝑌)))) | ||
Theorem | lsmelval2 20673* | 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 20674 | 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 20675 | Subspace sum of spans of subsets is the span of their union. (spanuni 30762 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ 𝑈 ⊆ 𝑉) → ((𝑁‘𝑇) ⊕ (𝑁‘𝑈)) = (𝑁‘(𝑇 ∪ 𝑈))) | ||
Theorem | lsmssspx 20676 | 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 20677 | 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 20678 | 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 20679 | 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 20680 | 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 20681* | Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = {𝑣 ∣ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑣 = ((𝑘 · 𝑋) + (𝑙 · 𝑌))}) | ||
Theorem | lspprel 20682* | Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ∃𝑘 ∈ 𝐾 ∃𝑙 ∈ 𝐾 𝑍 = ((𝑘 · 𝑋) + (𝑙 · 𝑌)))) | ||
Theorem | lspprabs 20683 | Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘{𝑋, (𝑋 + 𝑌)}) = (𝑁‘{𝑋, 𝑌})) | ||
Theorem | lspvadd 20684 | 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 20685 | 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 20686 | 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 20687* | 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 20688 | 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 20689 | 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 20690 | Extend class notation with class of all left vector spaces. |
class LVec | ||
Definition | df-lvec 20691 | 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 20692 | The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) | ||
Theorem | lvecdrng 20693 | The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) | ||
Theorem | lveclmod 20694 | A left vector space is a left module. (Contributed by NM, 9-Dec-2013.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | ||
Theorem | lveclmodd 20695 | A vector space is a left module. (Contributed by SN, 16-May-2024.) |
⊢ (𝜑 → 𝑊 ∈ LVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ LMod) | ||
Theorem | lsslvec 20696 | A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LVec) | ||
Theorem | lmhmlvec 20697 | The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
Theorem | lvecvs0or 20698 | If a scalar product is zero, one of its factors must be zero. (hvmul0or 30243 analog.) (Contributed by NM, 2-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑂 = (0g‘𝐹) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 · 𝑋) = 0 ↔ (𝐴 = 𝑂 ∨ 𝑋 = 0 ))) | ||
Theorem | lvecvsn0 20699 | 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 20700 | 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 ∨ 𝑋 ∈ 𝑈))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |