![]() |
Metamath
Proof Explorer Theorem List (p. 207 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lspsnss 20601 | The span of the singleton of a subspace member is included in the subspace. (spansnss 30824 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 4-Sep-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (πβ{π}) β π) | ||
Theorem | lspsnel3 20602 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (elspansn3 30825 analog.) (Contributed by NM, 4-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) β β’ (π β π β π) | ||
Theorem | lspprss 20603 | The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) β π) | ||
Theorem | lspsnid 20604 | A vector belongs to the span of its singleton. (spansnid 30816 analog.) (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β π β (πβ{π})) | ||
Theorem | lspsnel6 20605 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) (Revised by Mario Carneiro, 8-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (π β π β (π β π β§ (πβ{π}) β π))) | ||
Theorem | lspsnel5 20606 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β (πβ{π}) β π)) | ||
Theorem | lspsnel5a 20607 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π}) β π) | ||
Theorem | lspprid1 20608 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprid2 20609 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprvacl 20610 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π + π) β (πβ{π, π})) | ||
Theorem | lssats2 20611* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β π = βͺ π₯ β π (πβ{π₯})) | ||
Theorem | lspsneli 20612 | A scalar product with a vector belongs to the span of its singleton. (spansnmul 30817 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) β β’ (π β (π΄ Β· π) β (πβ{π})) | ||
Theorem | lspsn 20613* | Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) = {π£ β£ βπ β πΎ π£ = (π Β· π)}) | ||
Theorem | lspsnel 20614* | Member of span of the singleton of a vector. (elspansn 30819 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnvsi 20615 | Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β πΎ β§ π β π) β (πβ{(π Β· π)}) β (πβ{π})) | ||
Theorem | lspsnss2 20616* | Comparable spans of singletons must have proportional vectors. See lspsneq 20735 for equal span version. (Contributed by NM, 7-Jun-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnneg 20617 | Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) | ||
Theorem | lspsnsub 20618 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) | ||
Theorem | lspsn0 20619 | Span of the singleton of the zero vector. (spansn0 30794 analog.) (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πβ{ 0 }) = { 0 }) | ||
Theorem | lsp0 20620 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πββ ) = { 0 }) | ||
Theorem | lspuni0 20621 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ ) = 0 ) | ||
Theorem | lspun0 20622 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) | ||
Theorem | lspsneq0 20623 | Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) | ||
Theorem | lspsneq0b 20624 | 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 20625 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) | ||
Theorem | lsslsp 20626 | 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 20627 | 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 20628* | 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 20629* | 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 20630 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 20631 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 20632 | The class of the left module isomorphism relation. |
class βπ | ||
Definition | df-lmhm 20633* | 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 20634* | 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 20635 | 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 20636 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom LMHom | ||
Theorem | lmimfn 20637 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ LMIso Fn (LMod Γ LMod) | ||
Theorem | islmhm 20638* | 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 20639* | Property of a module homomorphism, similar to ismhm 18673. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) | ||
Theorem | lmhmlem 20640 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) β β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ πΏ = πΎ))) | ||
Theorem | lmhmsca 20641 | 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 20642 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) | ||
Theorem | lmhmlmod2 20643 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmlmod1 20644 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmf 20645 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π LMHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | lmhmlin 20646 | A homomorphism of left modules is πΎ-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((πΉ β (π LMHom π) β§ π β π΅ β§ π β πΈ) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | lmodvsinv 20647 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ π = (invgβπΉ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β ((πβπ ) Β· π) = (πβ(π Β· π))) | ||
Theorem | lmodvsinv2 20648 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β (π Β· (πβπ)) = (πβ(π Β· π))) | ||
Theorem | islmhm2 20649* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20543. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ πΈ = (BaseβπΎ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))))) | ||
Theorem | islmhmd 20650* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) & β’ πΎ = (Scalarβπ) & β’ π½ = (Scalarβπ) & β’ π = (BaseβπΎ) & β’ (π β π β LMod) & β’ (π β π β LMod) & β’ (π β π½ = πΎ) & β’ (π β πΉ β (π GrpHom π)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) β β’ (π β πΉ β (π LMHom π)) | ||
Theorem | 0lmhm 20651 | 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 20652 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β LMod β ( I βΎ π΅) β (π LMHom π)) | ||
Theorem | invlmhm 20653 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ πΌ = (invgβπ) β β’ (π β LMod β πΌ β (π LMHom π)) | ||
Theorem | lmhmco 20654 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ β πΊ) β (π LMHom π)) | ||
Theorem | lmhmplusg 20655 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ + = (+gβπ) β β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ βf + πΊ) β (π LMHom π)) | ||
Theorem | lmhmvsca 20656 | 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 20657 | 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 20658 | The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β π) | ||
Theorem | lmhmpreima 20659 | The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (β‘πΉ β π) β π) | ||
Theorem | lmhmlsp 20660 | Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (Baseβπ) & β’ πΎ = (LSpanβπ) & β’ πΏ = (LSpanβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β (πΎβπ)) = (πΏβ(πΉ β π))) | ||
Theorem | lmhmrnlss 20661 | The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β ran πΉ β (LSubSpβπ)) | ||
Theorem | lmhmkerlss 20662 | The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (β‘πΉ β { 0 }) & β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (πΉ β (π LMHom π) β πΎ β π) | ||
Theorem | reslmhm 20663 | Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ βΎ π) β (π LMHom π)) | ||
Theorem | reslmhm2 20664 | 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 20665 | 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 20666 | The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β dom (πΉ β© πΊ) β π) | ||
Theorem | lspextmo 20667* | 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 20668* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β LMod β§ πΌ β π) β πΉ β (π LMHom π)) | ||
Theorem | pwssplit0 20669* | Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs π) & β’ π = (π βs π) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΉ = (π₯ β π΅ β¦ (π₯ βΎ π)) β β’ ((π β π β§ π β π β§ π β π) β πΉ:π΅βΆπΆ) | ||
Theorem | pwssplit1 20670* | 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 20671* | 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 20672* | 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 20673 | 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 20674 | An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π LMIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | lmimlmhm 20675 | An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ (πΉ β (π LMIso π) β πΉ β (π LMHom π)) | ||
Theorem | lmimgim 20676 | 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 20677 | 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 20678 | 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 20679 | The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π LMIso π) β β ) | ||
Theorem | brlmici 20680 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ β (π LMIso π) β π βπ π) | ||
Theorem | lmiclcl 20681 | Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β π β LMod) | ||
Theorem | lmicrcl 20682 | Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (π βπ π β π β LMod) | ||
Theorem | lmicsym 20683 | Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ (π βπ π β π βπ π ) | ||
Theorem | lmhmpropd 20684* | 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 20685 | Extend class notation with the set of bases for a vector space. |
class LBasis | ||
Definition | df-lbs 20686* | 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 20687* | 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 20688 | A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) β β’ (π΅ β π½ β π΅ β π) | ||
Theorem | lbsel 20689 | An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) β β’ ((π΅ β π½ β§ πΈ β π΅) β πΈ β π) | ||
Theorem | lbssp 20690 | The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) β β’ (π΅ β π½ β (πβπ΅) = π) | ||
Theorem | lbsind 20691 | 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 20692 | 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 20693 | 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 20694 | 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 20695* | Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β ((πβ{π}) β (πβ{π})) β βπ β πΎ βπ β πΎ π = ((π Β· π) + (π Β· π)))) | ||
Theorem | lsmelval2 20696* | 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 20697 | 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 20698 | Subspace sum of spans of subsets is the span of their union. (spanuni 30797 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) β β’ ((π β LMod β§ π β π β§ π β π) β ((πβπ) β (πβπ)) = (πβ(π βͺ π))) | ||
Theorem | lsmssspx 20699 | 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 20700 | 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) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) = ((πβ{π}) β (πβ{π}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |