![]() |
Metamath
Proof Explorer Theorem List (p. 218 of 482) | < 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-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uvcvvcl 21701 | A coordinate of a unit vector is either 0 or 1. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π unitVec πΌ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (((π β π β§ πΌ β π β§ π½ β πΌ) β§ πΎ β πΌ) β ((πβπ½)βπΎ) β { 0 , 1 }) | ||
Theorem | uvcvvcl2 21702 | A unit vector coordinate is a ring element. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π unitVec πΌ) & β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β πΎ β πΌ) β β’ (π β ((πβπ½)βπΎ) β π΅) | ||
Theorem | uvcvv1 21703 | The unit vector is one at its designated coordinate. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π unitVec πΌ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ 1 = (1rβπ ) β β’ (π β ((πβπ½)βπ½) = 1 ) | ||
Theorem | uvcvv0 21704 | The unit vector is zero at its designated coordinate. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π unitVec πΌ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β πΎ β πΌ) & β’ (π β π½ β πΎ) & β’ 0 = (0gβπ ) β β’ (π β ((πβπ½)βπΎ) = 0 ) | ||
Theorem | uvcff 21705 | Domain and codomain of the unit vector generator; ring condition required to be sure 1 and 0 are actually in the ring. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by AV, 21-Jul-2019.) |
β’ π = (π unitVec πΌ) & β’ π = (π freeLMod πΌ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΌ β π) β π:πΌβΆπ΅) | ||
Theorem | uvcf1 21706 | In a nonzero ring, each unit vector is different. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
β’ π = (π unitVec πΌ) & β’ π = (π freeLMod πΌ) & β’ π΅ = (Baseβπ) β β’ ((π β NzRing β§ πΌ β π) β π:πΌβ1-1βπ΅) | ||
Theorem | uvcresum 21707 | Any element of a free module can be expressed as a finite linear combination of unit vectors. (Contributed by Stefan O'Rear, 3-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Jul-2015.) |
β’ π = (π unitVec πΌ) & β’ π = (π freeLMod πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β Ring β§ πΌ β π β§ π β π΅) β π = (π Ξ£g (π βf Β· π))) | ||
Theorem | frlmssuvc1 21708* | A scalar multiple of a unit vector included in a support-restriction subspace is included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 24-Jun-2019.) |
β’ πΉ = (π freeLMod πΌ) & β’ π = (π unitVec πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπΉ) & β’ 0 = (0gβπ ) & β’ πΆ = {π₯ β π΅ β£ (π₯ supp 0 ) β π½} & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β πΏ β π½) & β’ (π β π β πΎ) β β’ (π β (π Β· (πβπΏ)) β πΆ) | ||
Theorem | frlmssuvc2 21709* | A nonzero scalar multiple of a unit vector not included in a support-restriction subspace is not included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 24-Jun-2019.) |
β’ πΉ = (π freeLMod πΌ) & β’ π = (π unitVec πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπΉ) & β’ 0 = (0gβπ ) & β’ πΆ = {π₯ β π΅ β£ (π₯ supp 0 ) β π½} & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β πΏ β (πΌ β π½)) & β’ (π β π β (πΎ β { 0 })) β β’ (π β Β¬ (π Β· (πβπΏ)) β πΆ) | ||
Theorem | frlmsslsp 21710* | A subset of a free module obtained by restricting the support set is spanned by the relevant unit vectors. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by AV, 24-Jun-2019.) |
β’ π = (π freeLMod πΌ) & β’ π = (π unitVec πΌ) & β’ πΎ = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ πΆ = {π₯ β π΅ β£ (π₯ supp 0 ) β π½} β β’ ((π β Ring β§ πΌ β π β§ π½ β πΌ) β (πΎβ(π β π½)) = πΆ) | ||
Theorem | frlmlbs 21711 | The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Proof shortened by AV, 21-Jul-2019.) |
β’ πΉ = (π freeLMod πΌ) & β’ π = (π unitVec πΌ) & β’ π½ = (LBasisβπΉ) β β’ ((π β Ring β§ πΌ β π) β ran π β π½) | ||
Theorem | frlmup1 21712* | Any assignment of unit vectors to target vectors can be extended (uniquely) to a homomorphism from a free module to an arbitrary other module on the same base ring. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Proof shortened by AV, 21-Jul-2019.) |
β’ πΉ = (π freeLMod πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΆ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) & β’ (π β π β LMod) & β’ (π β πΌ β π) & β’ (π β π = (Scalarβπ)) & β’ (π β π΄:πΌβΆπΆ) β β’ (π β πΈ β (πΉ LMHom π)) | ||
Theorem | frlmup2 21713* | The evaluation map has the intended behavior on the unit vectors. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Proof shortened by AV, 21-Jul-2019.) |
β’ πΉ = (π freeLMod πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΆ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) & β’ (π β π β LMod) & β’ (π β πΌ β π) & β’ (π β π = (Scalarβπ)) & β’ (π β π΄:πΌβΆπΆ) & β’ (π β π β πΌ) & β’ π = (π unitVec πΌ) β β’ (π β (πΈβ(πβπ)) = (π΄βπ)) | ||
Theorem | frlmup3 21714* | The range of such an evaluation map is the finite linear combinations of the target vectors and also the span of the target vectors. (Contributed by Stefan O'Rear, 6-Feb-2015.) |
β’ πΉ = (π freeLMod πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΆ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) & β’ (π β π β LMod) & β’ (π β πΌ β π) & β’ (π β π = (Scalarβπ)) & β’ (π β π΄:πΌβΆπΆ) & β’ πΎ = (LSpanβπ) β β’ (π β ran πΈ = (πΎβran π΄)) | ||
Theorem | frlmup4 21715* | Universal property of the free module by existential uniqueness. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ π = (Scalarβπ) & β’ πΉ = (π freeLMod πΌ) & β’ π = (π unitVec πΌ) & β’ πΆ = (Baseβπ) β β’ ((π β LMod β§ πΌ β π β§ π΄:πΌβΆπΆ) β β!π β (πΉ LMHom π)(π β π) = π΄) | ||
Theorem | ellspd 21716* | The elements of the span of an indexed collection of basic vectors are those vectors which can be written as finite linear combinations of basic vectors. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by AV, 24-Jun-2019.) (Revised by AV, 11-Apr-2024.) |
β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ:πΌβΆπ΅) & β’ (π β π β LMod) & β’ (π β πΌ β π) β β’ (π β (π β (πβ(πΉ β πΌ)) β βπ β (πΎ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π βf Β· πΉ))))) | ||
Theorem | elfilspd 21717* | Simplified version of ellspd 21716 when the spanning set is finite: all linear combinations are then acceptable. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Proof shortened by AV, 21-Jul-2019.) |
β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ:πΌβΆπ΅) & β’ (π β π β LMod) & β’ (π β πΌ β Fin) β β’ (π β (π β (πβ(πΉ β πΌ)) β βπ β (πΎ βm πΌ)π = (π Ξ£g (π βf Β· πΉ)))) | ||
According to the definition in [Lang] p. 129: "A subset S of a module M is said to be linearly independent (over A) if whenever we have a linear combination βxβSaxx which is equal to 0, then ax = 0 for all x β S", and according to the Definition in [Lang] p. 130: "a familiy {xi}iβI of elements of M is said to be linearly independent (over A) if whenever we have a linear combination βiβIaixi = 0, then ai = 0 for all i β I." These definitions correspond to Definitions df-linds 21721 and df-lindf 21720 respectively, where it is claimed that a nonzero summand can be extracted (βiβ{I\{j}}aixi = -ajxj) and be represented as a linear combination of the remaining elements of the family. | ||
Syntax | clindf 21718 | The class relationship of independent families in a module. |
class LIndF | ||
Syntax | clinds 21719 | The class generator of independent sets in a module. |
class LIndS | ||
Definition | df-lindf 21720* |
An independent family is a family of vectors, no nonzero multiple of
which can be expressed as a linear combination of other elements of the
family. This is almost, but not quite, the same as a function into an
independent set.
This is a defined concept because it matters in many cases whether independence is taken at a set or family level. For instance, a number is transcedental iff its nonzero powers are linearly independent. Is 1 transcedental? It has only one nonzero power. We can almost define family independence as a family of unequal elements with independent range, as islindf3 21740, but taking that as primitive would lead to unpleasant corner case behavior with the zero ring. This is equivalent to the common definition of having no nontrivial representations of zero (islindf4 21752) and only one representation for each element of the range (islindf5 21753). (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ LIndF = {β¨π, π€β© β£ (π:dom πβΆ(Baseβπ€) β§ [(Scalarβπ€) / π ]βπ₯ β dom πβπ β ((Baseβπ ) β {(0gβπ )}) Β¬ (π( Β·π βπ€)(πβπ₯)) β ((LSpanβπ€)β(π β (dom π β {π₯}))))} | ||
Definition | df-linds 21721* | An independent set is a set which is independent as a family. See also islinds3 21748 and islinds4 21749. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ LIndS = (π€ β V β¦ {π β π« (Baseβπ€) β£ ( I βΎ π ) LIndF π€}) | ||
Theorem | rellindf 21722 | The independent-family predicate is a proper relation and can be used with brrelex1i 5728. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ Rel LIndF | ||
Theorem | islinds 21723 | Property of an independent set of vectors in terms of an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β π β (π β (LIndSβπ) β (π β π΅ β§ ( I βΎ π) LIndF π))) | ||
Theorem | linds1 21724 | An independent set of vectors is a set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β (LIndSβπ) β π β π΅) | ||
Theorem | linds2 21725 | An independent set of vectors is independent as a family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β (LIndSβπ) β ( I βΎ π) LIndF π) | ||
Theorem | islindf 21726* | Property of an independent family of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β π β§ πΉ β π) β (πΉ LIndF π β (πΉ:dom πΉβΆπ΅ β§ βπ₯ β dom πΉβπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (dom πΉ β {π₯})))))) | ||
Theorem | islinds2 21727* | Expanded property of an independent set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ (π β π β (πΉ β (LIndSβπ) β (πΉ β π΅ β§ βπ₯ β πΉ βπ β (π β { 0 }) Β¬ (π Β· π₯) β (πΎβ(πΉ β {π₯}))))) | ||
Theorem | islindf2 21728* | Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β π β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ₯ β πΌ βπ β (π β { 0 }) Β¬ (π Β· (πΉβπ₯)) β (πΎβ(πΉ β (πΌ β {π₯}))))) | ||
Theorem | lindff 21729 | Functional property of a linearly independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) β β’ ((πΉ LIndF π β§ π β π) β πΉ:dom πΉβΆπ΅) | ||
Theorem | lindfind 21730 | A linearly independent family is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ πΏ = (Scalarβπ) & β’ 0 = (0gβπΏ) & β’ πΎ = (BaseβπΏ) β β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β Β¬ (π΄ Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ})))) | ||
Theorem | lindsind 21731 | A linearly independent set is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ πΏ = (Scalarβπ) & β’ 0 = (0gβπΏ) & β’ πΎ = (BaseβπΏ) β β’ (((πΉ β (LIndSβπ) β§ πΈ β πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β Β¬ (π΄ Β· πΈ) β (πβ(πΉ β {πΈ}))) | ||
Theorem | lindfind2 21732 | In a linearly independent family in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ πΎ = (LSpanβπ) & β’ πΏ = (Scalarβπ) β β’ (((π β LMod β§ πΏ β NzRing) β§ πΉ LIndF π β§ πΈ β dom πΉ) β Β¬ (πΉβπΈ) β (πΎβ(πΉ β (dom πΉ β {πΈ})))) | ||
Theorem | lindsind2 21733 | In a linearly independent set in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ πΎ = (LSpanβπ) & β’ πΏ = (Scalarβπ) β β’ (((π β LMod β§ πΏ β NzRing) β§ πΉ β (LIndSβπ) β§ πΈ β πΉ) β Β¬ πΈ β (πΎβ(πΉ β {πΈ}))) | ||
Theorem | lindff1 21734 | A linearly independent family over a nonzero ring has no repeated elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΏ = (Scalarβπ) β β’ ((π β LMod β§ πΏ β NzRing β§ πΉ LIndF π) β πΉ:dom πΉβ1-1βπ΅) | ||
Theorem | lindfrn 21735 | The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ ((π β LMod β§ πΉ LIndF π) β ran πΉ β (LIndSβπ)) | ||
Theorem | f1lindf 21736 | Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β πΊ) LIndF π) | ||
Theorem | lindfres 21737 | Any restriction of an independent family is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ ((π β LMod β§ πΉ LIndF π) β (πΉ βΎ π) LIndF π) | ||
Theorem | lindsss 21738 | Any subset of an independent set is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ ((π β LMod β§ πΉ β (LIndSβπ) β§ πΊ β πΉ) β πΊ β (LIndSβπ)) | ||
Theorem | f1linds 21739 | A family constructed from non-repeated elements of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ ((π β LMod β§ π β (LIndSβπ) β§ πΉ:π·β1-1βπ) β πΉ LIndF π) | ||
Theorem | islindf3 21740 | In a nonzero ring, independent families can be equivalently characterized as renamings of independent sets. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ πΏ = (Scalarβπ) β β’ ((π β LMod β§ πΏ β NzRing) β (πΉ LIndF π β (πΉ:dom πΉβ1-1βV β§ ran πΉ β (LIndSβπ)))) | ||
Theorem | lindfmm 21741 | Linear independence of a family is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β (πΊ β πΉ) LIndF π)) | ||
Theorem | lindsmm 21742 | Linear independence of a set is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ β π΅) β (πΉ β (LIndSβπ) β (πΊ β πΉ) β (LIndSβπ))) | ||
Theorem | lindsmm2 21743 | The monomorphic image of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ β (LIndSβπ)) β (πΊ β πΉ) β (LIndSβπ)) | ||
Theorem | lsslindf 21744 | Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LMod β§ π β π β§ ran πΉ β π) β (πΉ LIndF π β πΉ LIndF π)) | ||
Theorem | lsslinds 21745 | Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LMod β§ π β π β§ πΉ β π) β (πΉ β (LIndSβπ) β πΉ β (LIndSβπ))) | ||
Theorem | islbs4 21746 | A basis is an independent spanning set. This could have been used as alternative definition of a basis: LBasis = (π€ β V β¦ {π β π« (Baseβπ€) β£ (((LSpanβπ€) βπ) = (Baseβπ€) β§ π β (LIndSβπ€))}). (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ π½ = (LBasisβπ) & β’ πΎ = (LSpanβπ) β β’ (π β π½ β (π β (LIndSβπ) β§ (πΎβπ) = π΅)) | ||
Theorem | lbslinds 21747 | A basis is independent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π½ = (LBasisβπ) β β’ π½ β (LIndSβπ) | ||
Theorem | islinds3 21748 | A subset is linearly independent iff it is a basis of its span. (Contributed by Stefan O'Rear, 25-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (LSpanβπ) & β’ π = (π βΎs (πΎβπ)) & β’ π½ = (LBasisβπ) β β’ (π β LMod β (π β (LIndSβπ) β π β π½)) | ||
Theorem | islinds4 21749* | A set is independent in a vector space iff it is a subset of some basis. This is an axiom of choice equivalent. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π½ = (LBasisβπ) β β’ (π β LVec β (π β (LIndSβπ) β βπ β π½ π β π)) | ||
Theorem | lmimlbs 21750 | The isomorphic image of a basis is a basis. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π½ = (LBasisβπ) & β’ πΎ = (LBasisβπ) β β’ ((πΉ β (π LMIso π) β§ π΅ β π½) β (πΉ β π΅) β πΎ) | ||
Theorem | lmiclbs 21751 | Having a basis is an isomorphism invariant. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π½ = (LBasisβπ) & β’ πΎ = (LBasisβπ) β β’ (π βπ π β (π½ β β β πΎ β β )) | ||
Theorem | islindf4 21752* | A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ ) & β’ πΏ = (Baseβ(π freeLMod πΌ)) β β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β π₯ = (πΌ Γ {π})))) | ||
Theorem | islindf5 21753* | A family is independent iff the linear combinations homomorphism is injective. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
β’ πΉ = (π freeLMod πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΆ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) & β’ (π β π β LMod) & β’ (π β πΌ β π) & β’ (π β π = (Scalarβπ)) & β’ (π β π΄:πΌβΆπΆ) β β’ (π β (π΄ LIndF π β πΈ:π΅β1-1βπΆ)) | ||
Theorem | indlcim 21754* | An independent, spanning family extends to an isomorphism from a free module. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ πΉ = (π freeLMod πΌ) & β’ π΅ = (BaseβπΉ) & β’ πΆ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) & β’ (π β π β LMod) & β’ (π β πΌ β π) & β’ (π β π = (Scalarβπ)) & β’ (π β π΄:πΌβontoβπ½) & β’ (π β π΄ LIndF π) & β’ (π β (πβπ½) = πΆ) β β’ (π β πΈ β (πΉ LMIso π)) | ||
Theorem | lbslcic 21755 | A module with a basis is isomorphic to a free module with the same cardinality. (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ πΉ = (Scalarβπ) & β’ π½ = (LBasisβπ) β β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β π βπ (πΉ freeLMod πΌ)) | ||
Theorem | lmisfree 21756* | A module has a basis iff it is isomorphic to a free module. In settings where isomorphic objects are not distinguished, it is common to define "free module" as any module with a basis; thus for instance lbsex 21035 might be described as "every vector space is free". (Contributed by Stefan O'Rear, 26-Feb-2015.) |
β’ π½ = (LBasisβπ) & β’ πΉ = (Scalarβπ) β β’ (π β LMod β (π½ β β β βπ π βπ (πΉ freeLMod π))) | ||
Theorem | lvecisfrlm 21757* | Every vector space is isomorphic to a free module. (Contributed by AV, 7-Mar-2019.) |
β’ πΉ = (Scalarβπ) β β’ (π β LVec β βπ π βπ (πΉ freeLMod π)) | ||
Theorem | lmimco 21758 | The composition of two isomorphisms of modules is an isomorphism of modules. (Contributed by AV, 10-Mar-2019.) |
β’ ((πΉ β (π LMIso π) β§ πΊ β (π LMIso π)) β (πΉ β πΊ) β (π LMIso π)) | ||
Theorem | lmictra 21759 | Module isomorphism is transitive. (Contributed by AV, 10-Mar-2019.) |
β’ ((π βπ π β§ π βπ π) β π βπ π) | ||
Theorem | uvcf1o 21760 | In a nonzero ring, the mapping of the index set of a free module onto the unit vectors of the free module is a 1-1 onto function. (Contributed by AV, 10-Mar-2019.) |
β’ π = (π unitVec πΌ) β β’ ((π β NzRing β§ πΌ β π) β π:πΌβ1-1-ontoβran π) | ||
Theorem | uvcendim 21761 | In a nonzero ring, the number of unit vectors of a free module corresponds to the dimension of the free module. (Contributed by AV, 10-Mar-2019.) |
β’ π = (π unitVec πΌ) β β’ ((π β NzRing β§ πΌ β π) β πΌ β ran π) | ||
Theorem | frlmisfrlm 21762 | A free module is isomorphic to a free module over the same (nonzero) ring, with the same cardinality. (Contributed by AV, 10-Mar-2019.) |
β’ ((π β NzRing β§ πΌ β π β§ πΌ β π½) β (π freeLMod πΌ) βπ (π freeLMod π½)) | ||
Theorem | frlmiscvec 21763 | Every free module is isomorphic to the free module of "column vectors" of the same dimension over the same (nonzero) ring. (Contributed by AV, 10-Mar-2019.) |
β’ ((π β NzRing β§ πΌ β π) β (π freeLMod πΌ) βπ (π freeLMod (πΌ Γ {β }))) | ||
Syntax | casa 21764 | Associative algebra. |
class AssAlg | ||
Syntax | casp 21765 | Algebraic span function. |
class AlgSpan | ||
Syntax | cascl 21766 | Class of algebra scalar injection function. |
class algSc | ||
Definition | df-assa 21767* | Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
β’ AssAlg = {π€ β (LMod β© Ring) β£ [(Scalarβπ€) / π]βπ β (Baseβπ)βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)[( Β·π βπ€) / π ][(.rβπ€) / π‘](((ππ π₯)π‘π¦) = (ππ (π₯π‘π¦)) β§ (π₯π‘(ππ π¦)) = (ππ (π₯π‘π¦)))} | ||
Definition | df-asp 21768* | Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ AlgSpan = (π€ β AssAlg β¦ (π β π« (Baseβπ€) β¦ β© {π‘ β ((SubRingβπ€) β© (LSubSpβπ€)) β£ π β π‘})) | ||
Definition | df-ascl 21769* | Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unity element. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ algSc = (π€ β V β¦ (π₯ β (Baseβ(Scalarβπ€)) β¦ (π₯( Β·π βπ€)(1rβπ€)))) | ||
Theorem | isassa 21770* | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ (π β AssAlg β ((π β LMod β§ π β Ring) β§ βπ β π΅ βπ₯ β π βπ¦ β π (((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦)) β§ (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))))) | ||
Theorem | assalem 21771 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β (((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π)) β§ (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π)))) | ||
Theorem | assaass 21772 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β ((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π))) | ||
Theorem | assaassr 21773 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ π β π β§ π β π)) β (π Γ (π΄ Β· π)) = (π΄ Β· (π Γ π))) | ||
Theorem | assalmod 21774 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ (π β AssAlg β π β LMod) | ||
Theorem | assaring 21775 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
β’ (π β AssAlg β π β Ring) | ||
Theorem | assasca 21776 | The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by SN, 2-Mar-2025.) |
β’ πΉ = (Scalarβπ) β β’ (π β AssAlg β πΉ β Ring) | ||
Theorem | assa2ass 21777 | Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) & β’ β = (.rβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) β β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = ((πΆ β π΄) Β· (π Γ π))) | ||
Theorem | isassad 21778* | Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
β’ (π β π = (Baseβπ)) & β’ (π β πΉ = (Scalarβπ)) & β’ (π β π΅ = (BaseβπΉ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β Γ = (.rβπ)) & β’ (π β π β LMod) & β’ (π β π β Ring) & β’ ((π β§ (π β π΅ β§ π₯ β π β§ π¦ β π)) β ((π Β· π₯) Γ π¦) = (π Β· (π₯ Γ π¦))) & β’ ((π β§ (π β π΅ β§ π₯ β π β§ π¦ β π)) β (π₯ Γ (π Β· π¦)) = (π Β· (π₯ Γ π¦))) β β’ (π β π β AssAlg) | ||
Theorem | issubassa3 21779 | A subring that is also a subspace is a subalgebra. The key theorem is islss3 20825. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (π βΎs π΄) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ (π΄ β (SubRingβπ) β§ π΄ β πΏ)) β π β AssAlg) | ||
Theorem | issubassa 21780 | The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π = (π βΎs π΄) & β’ πΏ = (LSubSpβπ) & β’ π = (Baseβπ) & β’ 1 = (1rβπ) β β’ ((π β AssAlg β§ 1 β π΄ β§ π΄ β π) β (π β AssAlg β (π΄ β (SubRingβπ) β§ π΄ β πΏ))) | ||
Theorem | sraassab 21781 | A subring algebra is an associative algebra if and only if the subring is included in the ring's center. (Contributed by SN, 21-Mar-2025.) |
β’ π΄ = ((subringAlg βπ)βπ) & β’ π = (Cntrβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ (π β π β (SubRingβπ)) β β’ (π β (π΄ β AssAlg β π β π)) | ||
Theorem | sraassa 21782 | The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) (Proof shortened by SN, 21-Mar-2025.) |
β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β AssAlg) | ||
Theorem | sraassaOLD 21783 | Obsolete version of sraassa 21782 as of 21-Mar-2025. (Contributed by Mario Carneiro, 6-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β CRing β§ π β (SubRingβπ)) β π΄ β AssAlg) | ||
Theorem | rlmassa 21784 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (π β CRing β (ringLModβπ ) β AssAlg) | ||
Theorem | assapropd 21785* | If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) & β’ (π β πΉ = (ScalarβπΎ)) & β’ (π β πΉ = (ScalarβπΏ)) & β’ π = (BaseβπΉ) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) β β’ (π β (πΎ β AssAlg β πΏ β AssAlg)) | ||
Theorem | aspval 21786* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) | ||
Theorem | asplss 21787 | The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) β πΏ) | ||
Theorem | aspid 21788 | The algebraic span of a subalgebra is itself. (spanid 31131 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β AssAlg β§ π β (SubRingβπ) β§ π β πΏ) β (π΄βπ) = π) | ||
Theorem | aspsubrg 21789 | The algebraic span of a set of vectors is a subring of the algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π) β (π΄βπ) β (SubRingβπ)) | ||
Theorem | aspss 21790 | Span preserves subset ordering. (spanss 31132 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π β§ π β π) β (π΄βπ) β (π΄βπ)) | ||
Theorem | aspssid 21791 | A set of vectors is a subset of its span. (spanss2 31129 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΄ = (AlgSpanβπ) & β’ π = (Baseβπ) β β’ ((π β AssAlg β§ π β π) β π β (π΄βπ)) | ||
Theorem | asclfval 21792* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ π΄ = (π₯ β πΎ β¦ (π₯ Β· 1 )) | ||
Theorem | asclval 21793 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) β β’ (π β πΎ β (π΄βπ) = (π Β· 1 )) | ||
Theorem | asclfn 21794 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ π΄ Fn πΎ | ||
Theorem | asclf 21795 | The algebra scalars function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β Ring) & β’ (π β π β LMod) & β’ πΎ = (BaseβπΉ) & β’ π΅ = (Baseβπ) β β’ (π β π΄:πΎβΆπ΅) | ||
Theorem | asclghm 21796 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β Ring) & β’ (π β π β LMod) β β’ (π β π΄ β (πΉ GrpHom π)) | ||
Theorem | ascl0 21797 | The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β LMod) & β’ (π β π β Ring) β β’ (π β (π΄β(0gβπΉ)) = (0gβπ)) | ||
Theorem | ascl1 21798 | The scalar 1 embedded into a left module corresponds to the 1 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β LMod) & β’ (π β π β Ring) β β’ (π β (π΄β(1rβπΉ)) = (1rβπ)) | ||
Theorem | asclmul1 21799 | Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β AssAlg β§ π β πΎ β§ π β π) β ((π΄βπ ) Γ π) = (π Β· π)) | ||
Theorem | asclmul2 21800 | Right multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β AssAlg β§ π β πΎ β§ π β π) β (π Γ (π΄βπ )) = (π Β· π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |