Home | Metamath
Proof Explorer Theorem List (p. 205 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsspropd 20401* | 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 20402* | 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 20403 | Extend class notation with the generator of left module hom-sets. |
class LMHom | ||
Syntax | clmim 20404 | The class of left module isomorphism sets. |
class LMIso | ||
Syntax | clmic 20405 | The class of the left module isomorphism relation. |
class βπ | ||
Definition | df-lmhm 20406* | 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 20407* | 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 20408 | 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 20409 | Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom LMHom | ||
Theorem | lmimfn 20410 | Lemma for module isomorphisms. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ LMIso Fn (LMod Γ LMod) | ||
Theorem | islmhm 20411* | 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 20412* | Property of a module homomorphism, similar to ismhm 18538. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) | ||
Theorem | lmhmlem 20413 | Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) β β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ πΏ = πΎ))) | ||
Theorem | lmhmsca 20414 | 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 20415 | A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) | ||
Theorem | lmhmlmod2 20416 | A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmlmod1 20417 | A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β π β LMod) | ||
Theorem | lmhmf 20418 | A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π LMHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | lmhmlin 20419 | A homomorphism of left modules is πΎ-linear. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & β’ πΈ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((πΉ β (π LMHom π) β§ π β π΅ β§ π β πΈ) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | lmodvsinv 20420 | Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ π = (invgβπΉ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β ((πβπ ) Β· π) = (πβ(π Β· π))) | ||
Theorem | lmodvsinv2 20421 | Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (invgβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π΅) β (π Β· (πβπ)) = (πβ(π Β· π))) | ||
Theorem | islmhm2 20422* | A one-equation proof of linearity of a left module homomorphism, similar to df-lss 20316. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΎ = (Scalarβπ) & β’ πΏ = (Scalarβπ) & β’ πΈ = (BaseβπΎ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) β β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))))) | ||
Theorem | islmhmd 20423* | Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ Γ = ( Β·π βπ) & β’ πΎ = (Scalarβπ) & β’ π½ = (Scalarβπ) & β’ π = (BaseβπΎ) & β’ (π β π β LMod) & β’ (π β π β LMod) & β’ (π β π½ = πΎ) & β’ (π β πΉ β (π GrpHom π)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) β β’ (π β πΉ β (π LMHom π)) | ||
Theorem | 0lmhm 20424 | 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 20425 | The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β LMod β ( I βΎ π΅) β (π LMHom π)) | ||
Theorem | invlmhm 20426 | The negative function on a module is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ πΌ = (invgβπ) β β’ (π β LMod β πΌ β (π LMHom π)) | ||
Theorem | lmhmco 20427 | The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ β πΊ) β (π LMHom π)) | ||
Theorem | lmhmplusg 20428 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ + = (+gβπ) β β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ βf + πΊ) β (π LMHom π)) | ||
Theorem | lmhmvsca 20429 | 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 20430 | 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 20431 | The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β π) | ||
Theorem | lmhmpreima 20432 | The inverse image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (β‘πΉ β π) β π) | ||
Theorem | lmhmlsp 20433 | Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (Baseβπ) & β’ πΎ = (LSpanβπ) & β’ πΏ = (LSpanβπ) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β (πΎβπ)) = (πΏβ(πΉ β π))) | ||
Theorem | lmhmrnlss 20434 | The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (πΉ β (π LMHom π) β ran πΉ β (LSubSpβπ)) | ||
Theorem | lmhmkerlss 20435 | The kernel of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ πΎ = (β‘πΉ β { 0 }) & β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) β β’ (πΉ β (π LMHom π) β πΎ β π) | ||
Theorem | reslmhm 20436 | Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ βΎ π) β (π LMHom π)) | ||
Theorem | reslmhm2 20437 | 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 20438 | 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 20439 | The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (LSubSpβπ) β β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β dom (πΉ β© πΊ) β π) | ||
Theorem | lspextmo 20440* | 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 20441* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β LMod β§ πΌ β π) β πΉ β (π LMHom π)) | ||
Theorem | pwssplit0 20442* | Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs π) & β’ π = (π βs π) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΉ = (π₯ β π΅ β¦ (π₯ βΎ π)) β β’ ((π β π β§ π β π β§ π β π) β πΉ:π΅βΆπΆ) | ||
Theorem | pwssplit1 20443* | 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 20444* | 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 20445* | 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 20446 | 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 20447 | An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π LMIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | lmimlmhm 20448 | An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ (πΉ β (π LMIso π) β πΉ β (π LMHom π)) | ||
Theorem | lmimgim 20449 | 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 20450 | 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 20451 | 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 20452 | The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π LMIso π) β β ) | ||
Theorem | brlmici 20453 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ β (π LMIso π) β π βπ π) | ||
Theorem | lmiclcl 20454 | Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β π β LMod) | ||
Theorem | lmicrcl 20455 | Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (π βπ π β π β LMod) | ||
Theorem | lmicsym 20456 | Module isomorphism is symmetric. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ (π βπ π β π βπ π ) | ||
Theorem | lmhmpropd 20457* | 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 20458 | Extend class notation with the set of bases for a vector space. |
class LBasis | ||
Definition | df-lbs 20459* | 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 20460* | 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 20461 | A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) β β’ (π΅ β π½ β π΅ β π) | ||
Theorem | lbsel 20462 | An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) β β’ ((π΅ β π½ β§ πΈ β π΅) β πΈ β π) | ||
Theorem | lbssp 20463 | The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) β β’ (π΅ β π½ β (πβπ΅) = π) | ||
Theorem | lbsind 20464 | 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 20465 | 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 20466 | 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 20467 | 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 20468* | Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β ((πβ{π}) β (πβ{π})) β βπ β πΎ βπ β πΎ π = ((π Β· π) + (π Β· π)))) | ||
Theorem | lsmelval2 20469* | 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 20470 | 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 20471 | Subspace sum of spans of subsets is the span of their union. (spanuni 30272 analog.) (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) β β’ ((π β LMod β§ π β π β§ π β π) β ((πβπ) β (πβπ)) = (πβ(π βͺ π))) | ||
Theorem | lsmssspx 20472 | 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 20473 | 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 20474 | 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 20475 | 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 20476 | 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 20477* | Span of a pair of vectors. (Contributed by NM, 22-Aug-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, π}) = {π£ β£ βπ β πΎ βπ β πΎ π£ = ((π Β· π) + (π Β· π))}) | ||
Theorem | lspprel 20478* | Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (πβ{π, π}) β βπ β πΎ βπ β πΎ π = ((π Β· π) + (π Β· π)))) | ||
Theorem | lspprabs 20479 | Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π, (π + π)}) = (πβ{π, π})) | ||
Theorem | lspvadd 20480 | 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 20481 | 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 20482 | 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 20483* | 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 20484 | 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 20485 | 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 20486 | Extend class notation with class of all left vector spaces. |
class LVec | ||
Definition | df-lvec 20487 | 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 20488 | The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.) |
β’ πΉ = (Scalarβπ) β β’ (π β LVec β (π β LMod β§ πΉ β DivRing)) | ||
Theorem | lvecdrng 20489 | The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.) |
β’ πΉ = (Scalarβπ) β β’ (π β LVec β πΉ β DivRing) | ||
Theorem | lveclmod 20490 | A left vector space is a left module. (Contributed by NM, 9-Dec-2013.) |
β’ (π β LVec β π β LMod) | ||
Theorem | lsslvec 20491 | A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β LVec β§ π β π) β π β LVec) | ||
Theorem | lvecvs0or 20492 | If a scalar product is zero, one of its factors must be zero. (hvmul0or 29753 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π΄ β πΎ) & β’ (π β π β π) β β’ (π β ((π΄ Β· π) = 0 β (π΄ = π β¨ π = 0 ))) | ||
Theorem | lvecvsn0 20493 | 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 20494 | 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 20495 | Cancellation law for scalar multiplication. (hvmulcan 29800 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) & β’ (π β π β LVec) & β’ (π β π΄ β πΎ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β 0 ) β β’ (π β ((π΄ Β· π) = (π΄ Β· π) β π = π)) | ||
Theorem | lvecvscan2 20496 | Cancellation law for scalar multiplication. (hvmulcan2 29801 analog.) (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β ((π΄ Β· π) = (π΅ Β· π) β π΄ = π΅)) | ||
Theorem | lvecinv 20497 | Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) & β’ πΌ = (invrβπΉ) & β’ (π β π β LVec) & β’ (π β π΄ β (πΎ β { 0 })) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π = (π΄ Β· π) β π = ((πΌβπ΄) Β· π))) | ||
Theorem | lspsnvs 20498 | A nonzero scalar product does not change the span of a singleton. (spansncol 30296 analog.) (Contributed by NM, 23-Apr-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) & β’ π = (LSpanβπ) β β’ ((π β LVec β§ (π β πΎ β§ π β 0 ) β§ π β π) β (πβ{(π Β· π)}) = (πβ{π})) | ||
Theorem | lspsneleq 20499 | Membership relation that implies equality of spans. (spansneleq 30298 analog.) (Contributed by NM, 4-Jul-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β (πβ{π})) & β’ (π β π β 0 ) β β’ (π β (πβ{π}) = (πβ{π})) | ||
Theorem | lspsncmp 20500 | Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β (πβ{π}) = (πβ{π}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |