![]() |
Metamath
Proof Explorer Theorem List (p. 476 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fldcatALTV 47501* | The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldcALTV 47502* | The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatALTVβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubcALTV 47503* | According to df-subc 17789, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17820 and subcss2 17823). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatALTVβπ) βΎcat π½))) | ||
Theorem | opeliun2xp 47504 | Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5740. (Contributed by AV, 30-Mar-2019.) |
β’ (β¨πΆ, π¦β© β βͺ π¦ β π΅ (π΄ Γ {π¦}) β (π¦ β π΅ β§ πΆ β π΄)) | ||
Theorem | eliunxp2 47505* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5835. (Contributed by AV, 30-Mar-2019.) |
β’ (πΆ β βͺ π¦ β π΅ (π΄ Γ {π¦}) β βπ₯βπ¦(πΆ = β¨π₯, π¦β© β§ (π₯ β π΄ β§ π¦ β π΅))) | ||
Theorem | mpomptx2 47506* | Express a two-argument function as a one-argument function, or vice-versa. In this version π΄(π¦) is not assumed to be constant w.r.t π¦, analogous to mpomptx 7527. (Contributed by AV, 30-Mar-2019.) |
β’ (π§ = β¨π₯, π¦β© β πΆ = π·) β β’ (π§ β βͺ π¦ β π΅ (π΄ Γ {π¦}) β¦ πΆ) = (π₯ β π΄, π¦ β π΅ β¦ π·) | ||
Theorem | cbvmpox2 47507* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7508 allows π΄ to be a function of π¦, analogous to cbvmpox 7507. (Contributed by AV, 30-Mar-2019.) |
β’ β²π§π΄ & β’ β²π¦π· & β’ β²π§πΆ & β’ β²π€πΆ & β’ β²π₯πΈ & β’ β²π¦πΈ & β’ (π¦ = π§ β π΄ = π·) & β’ ((π¦ = π§ β§ π₯ = π€) β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π€ β π·, π§ β π΅ β¦ πΈ) | ||
Theorem | dmmpossx2 47508* | The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx 8064. (Contributed by AV, 30-Mar-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ dom πΉ β βͺ π¦ β π΅ (π΄ Γ {π¦}) | ||
Theorem | mpoexxg2 47509* | Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg 8073. (Contributed by AV, 30-Mar-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((π΅ β π β§ βπ¦ β π΅ π΄ β π) β πΉ β V) | ||
Theorem | ovmpordxf 47510* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7565. (Contributed by AV, 30-Mar-2019.) |
β’ (π β πΉ = (π₯ β πΆ, π¦ β π· β¦ π )) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β π = π) & β’ ((π β§ π¦ = π΅) β πΆ = πΏ) & β’ (π β π΄ β πΏ) & β’ (π β π΅ β π·) & β’ (π β π β π) & β’ β²π₯π & β’ β²π¦π & β’ β²π¦π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π¦π β β’ (π β (π΄πΉπ΅) = π) | ||
Theorem | ovmpordx 47511* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7565. (Contributed by AV, 30-Mar-2019.) |
β’ (π β πΉ = (π₯ β πΆ, π¦ β π· β¦ π )) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β π = π) & β’ ((π β§ π¦ = π΅) β πΆ = πΏ) & β’ (π β π΄ β πΏ) & β’ (π β π΅ β π·) & β’ (π β π β π) β β’ (π β (π΄πΉπ΅) = π) | ||
Theorem | ovmpox2 47512* | The value of an operation class abstraction. Variant of ovmpoga 7569 which does not require π· and π₯ to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ ((π₯ = π΄ β§ π¦ = π΅) β π = π) & β’ (π¦ = π΅ β πΆ = πΏ) & β’ πΉ = (π₯ β πΆ, π¦ β π· β¦ π ) β β’ ((π΄ β πΏ β§ π΅ β π· β§ π β π») β (π΄πΉπ΅) = π) | ||
Theorem | fdmdifeqresdif 47513* | The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.) |
β’ πΉ = (π₯ β π· β¦ if(π₯ = π, π, (πΊβπ₯))) β β’ (πΊ:(π· β {π})βΆπ β πΊ = (πΉ βΎ (π· β {π}))) | ||
Theorem | offvalfv 47514* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
β’ (π β π΄ β π) & β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΄) β β’ (π β (πΉ βf π πΊ) = (π₯ β π΄ β¦ ((πΉβπ₯)π (πΊβπ₯)))) | ||
Theorem | ofaddmndmap 47515 | The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β Mnd β§ π β π β§ (π΄ β (π βm π) β§ π΅ β (π βm π))) β (π΄ βf + π΅) β (π βm π)) | ||
Theorem | mapsnop 47516 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
β’ πΉ = {β¨π, πβ©} β β’ ((π β π β§ π β π β§ π β π) β πΉ β (π βm {π})) | ||
Theorem | fprmappr 47517 | A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024.) |
β’ ((π β π β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅) β§ (πΆ β π β§ π· β π)) β {β¨π΄, πΆβ©, β¨π΅, π·β©} β (π βm {π΄, π΅})) | ||
Theorem | mapprop 47518 | An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) (Proof shortened by AV, 2-Jun-2024.) |
β’ πΉ = {β¨π, π΄β©, β¨π, π΅β©} β β’ (((π β π β§ π΄ β π ) β§ (π β π β§ π΅ β π ) β§ (π β π β§ π β π)) β πΉ β (π βm {π, π})) | ||
Theorem | ztprmneprm 47519 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
β’ ((π β β€ β§ π΄ β β β§ π΅ β β) β ((π Β· π΄) = π΅ β π΄ = π΅)) | ||
Theorem | 2t6m3t4e0 47520 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
β’ ((2 Β· 6) β (3 Β· 4)) = 0 | ||
Theorem | ssnn0ssfz 47521* | For any finite subset of β0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 32595. (Contributed by AV, 30-Sep-2019.) |
β’ (π΄ β (π« β0 β© Fin) β βπ β β0 π΄ β (0...π)) | ||
Theorem | nn0sumltlt 47522 | If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019.) |
β’ ((π β β0 β§ π β β0 β§ π β β0) β ((π + π) < π β π < π)) | ||
Theorem | bcpascm1 47523 | Pascal's rule for the binomial coefficient, generalized to all integers πΎ, shifted down by 1. (Contributed by AV, 8-Sep-2019.) |
β’ ((π β β β§ πΎ β β€) β (((π β 1)CπΎ) + ((π β 1)C(πΎ β 1))) = (πCπΎ)) | ||
Theorem | altgsumbc 47524* | The sum of binomial coefficients for a fixed positive π with alternating signs is zero. Notice that this is not valid for π = 0 (since ((-1β0) Β· (0C0)) = (1 Β· 1) = 1). For a proof using Pascal's rule (bcpascm1 47523) instead of the binomial theorem (binom 15803), see altgsumbcALT 47525. (Contributed by AV, 13-Sep-2019.) |
β’ (π β β β Ξ£π β (0...π)((-1βπ) Β· (πCπ)) = 0) | ||
Theorem | altgsumbcALT 47525* | Alternate proof of altgsumbc 47524, using Pascal's rule (bcpascm1 47523) instead of the binomial theorem (binom 15803). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β β Ξ£π β (0...π)((-1βπ) Β· (πCπ)) = 0) | ||
Theorem | zlmodzxzlmod 47526 | The β€-module β€ Γ β€ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) β β’ (π β LMod β§ β€ring = (Scalarβπ)) | ||
Theorem | zlmodzxzel 47527 | An element of the (base set of the) β€-module β€ Γ β€. (Contributed by AV, 21-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) β β’ ((π΄ β β€ β§ π΅ β β€) β {β¨0, π΄β©, β¨1, π΅β©} β (Baseβπ)) | ||
Theorem | zlmodzxz0 47528 | The 0 of the β€-module β€ Γ β€. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ 0 = {β¨0, 0β©, β¨1, 0β©} β β’ 0 = (0gβπ) | ||
Theorem | zlmodzxzscm 47529 | The scalar multiplication of the β€-module β€ Γ β€. (Contributed by AV, 20-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ β = ( Β·π βπ) β β’ ((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β (π΄ β {β¨0, π΅β©, β¨1, πΆβ©}) = {β¨0, (π΄ Β· π΅)β©, β¨1, (π΄ Β· πΆ)β©}) | ||
Theorem | zlmodzxzadd 47530 | The addition of the β€-module β€ Γ β€. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ + = (+gβπ) β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€)) β ({β¨0, π΄β©, β¨1, πΆβ©} + {β¨0, π΅β©, β¨1, π·β©}) = {β¨0, (π΄ + π΅)β©, β¨1, (πΆ + π·)β©}) | ||
Theorem | zlmodzxzsubm 47531 | The subtraction of the β€-module β€ Γ β€ expressed as addition. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ β = (-gβπ) β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€)) β ({β¨0, π΄β©, β¨1, πΆβ©} β {β¨0, π΅β©, β¨1, π·β©}) = ({β¨0, π΄β©, β¨1, πΆβ©} (+gβπ)(-1( Β·π βπ){β¨0, π΅β©, β¨1, π·β©}))) | ||
Theorem | zlmodzxzsub 47532 | The subtraction of the β€-module β€ Γ β€. (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ π = (β€ring freeLMod {0, 1}) & β’ β = (-gβπ) β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€)) β ({β¨0, π΄β©, β¨1, πΆβ©} β {β¨0, π΅β©, β¨1, π·β©}) = {β¨0, (π΄ β π΅)β©, β¨1, (πΆ β π·)β©}) | ||
Theorem | mgpsumunsn 47533* | Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (Contributed by AV, 29-Dec-2018.) |
β’ π = (mulGrpβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β πΌ β π) & β’ ((π β§ π β π) β π΄ β (Baseβπ )) & β’ (π β π β (Baseβπ )) & β’ (π = πΌ β π΄ = π) β β’ (π β (π Ξ£g (π β π β¦ π΄)) = ((π Ξ£g (π β (π β {πΌ}) β¦ π΄)) Β· π)) | ||
Theorem | mgpsumz 47534* | If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018.) |
β’ π = (mulGrpβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β πΌ β π) & β’ ((π β§ π β π) β π΄ β (Baseβπ )) & β’ 0 = (0gβπ ) & β’ (π = πΌ β π΄ = 0 ) β β’ (π β (π Ξ£g (π β π β¦ π΄)) = 0 ) | ||
Theorem | mgpsumn 47535* | If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (Contributed by AV, 29-Dec-2018.) |
β’ π = (mulGrpβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β πΌ β π) & β’ ((π β§ π β π) β π΄ β (Baseβπ )) & β’ 1 = (1rβπ ) & β’ (π = πΌ β π΄ = 1 ) β β’ (π β (π Ξ£g (π β π β¦ π΄)) = (π Ξ£g (π β (π β {πΌ}) β¦ π΄))) | ||
Theorem | exple2lt6 47536 | A nonnegative integer to the power of itself is less than 6 if it is less than or equal to 2. (Contributed by AV, 16-Mar-2019.) |
β’ ((π β β0 β§ π β€ 2) β (πβπ) < 6) | ||
Theorem | pgrple2abl 47537 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ ((π΄ β π β§ (β―βπ΄) β€ 2) β πΊ β Abel) | ||
Theorem | pgrpgt2nabl 47538 | Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ ((π΄ β π β§ 2 < (β―βπ΄)) β πΊ β Abel) | ||
Theorem | invginvrid 47539 | Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ π = (invgβπ ) & β’ πΌ = (invrβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π) β ((πβπ) Β· ((πΌβ(πβπ)) Β· π)) = π) | ||
Theorem | rmsupp0 47540* | The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Ring β§ π β π β§ πΆ = (0gβπ)) β§ π΄ β (π βm π)) β ((π£ β π β¦ (πΆ(.rβπ)(π΄βπ£))) supp (0gβπ)) = β ) | ||
Theorem | domnmsuppn0 47541* | The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Domn β§ π β π) β§ (πΆ β π β§ πΆ β (0gβπ)) β§ π΄ β (π βm π)) β ((π£ β π β¦ (πΆ(.rβπ)(π΄βπ£))) supp (0gβπ)) = (π΄ supp (0gβπ))) | ||
Theorem | rmsuppss 47542* | The support of a mapping of a multiplication of a constant with a function into a ring is a subset of the support of the function. (Contributed by AV, 11-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Ring β§ π β π β§ πΆ β π ) β§ π΄ β (π βm π)) β ((π£ β π β¦ (πΆ(.rβπ)(π΄βπ£))) supp (0gβπ)) β (π΄ supp (0gβπ))) | ||
Theorem | mndpsuppss 47543 | The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Mnd β§ π β π) β§ (π΄ β (π βm π) β§ π΅ β (π βm π))) β ((π΄ βf (+gβπ)π΅) supp (0gβπ)) β ((π΄ supp (0gβπ)) βͺ (π΅ supp (0gβπ)))) | ||
Theorem | scmsuppss 47544* | The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.) |
β’ π = (Scalarβπ) & β’ π = (Baseβπ) β β’ ((π β LMod β§ π β π« (Baseβπ) β§ π΄ β (π βm π)) β ((π£ β π β¦ ((π΄βπ£)( Β·π βπ)π£)) supp (0gβπ)) β (π΄ supp (0gβπ))) | ||
Theorem | rmsuppfi 47545* | The support of a mapping of a multiplication of a constant with a function into a ring is finite if the support of the function is finite. (Contributed by AV, 11-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Ring β§ π β π β§ πΆ β π ) β§ π΄ β (π βm π) β§ (π΄ supp (0gβπ)) β Fin) β ((π£ β π β¦ (πΆ(.rβπ)(π΄βπ£))) supp (0gβπ)) β Fin) | ||
Theorem | rmfsupp 47546* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by AV, 9-Jun-2019.) |
β’ π = (Baseβπ) β β’ (((π β Ring β§ π β π β§ πΆ β π ) β§ π΄ β (π βm π) β§ π΄ finSupp (0gβπ)) β (π£ β π β¦ (πΆ(.rβπ)(π΄βπ£))) finSupp (0gβπ)) | ||
Theorem | mndpsuppfi 47547 | The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.) |
β’ π = (Baseβπ) β β’ (((π β Mnd β§ π β π) β§ (π΄ β (π βm π) β§ π΅ β (π βm π)) β§ ((π΄ supp (0gβπ)) β Fin β§ (π΅ supp (0gβπ)) β Fin)) β ((π΄ βf (+gβπ)π΅) supp (0gβπ)) β Fin) | ||
Theorem | mndpfsupp 47548 | A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.) |
β’ π = (Baseβπ) β β’ (((π β Mnd β§ π β π) β§ (π΄ β (π βm π) β§ π΅ β (π βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π΄ βf (+gβπ)π΅) finSupp (0gβπ)) | ||
Theorem | scmsuppfi 47549* | The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.) |
β’ π = (Scalarβπ) & β’ π = (Baseβπ) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ π΄ β (π βm π) β§ (π΄ supp (0gβπ)) β Fin) β ((π£ β π β¦ ((π΄βπ£)( Β·π βπ)π£)) supp (0gβπ)) β Fin) | ||
Theorem | scmfsupp 47550* | A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.) |
β’ π = (Scalarβπ) & β’ π = (Baseβπ) β β’ (((π β LMod β§ π β π« (Baseβπ)) β§ π΄ β (π βm π) β§ π΄ finSupp (0gβπ)) β (π£ β π β¦ ((π΄βπ£)( Β·π βπ)π£)) finSupp (0gβπ)) | ||
Theorem | suppmptcfin 47551* | The support of a mapping with value 0 except of one is finite. (Contributed by AV, 27-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) β β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ supp 0 ) β Fin) | ||
Theorem | mptcfsupp 47552* | A mapping with value 0 except of one is finitely supported. (Contributed by AV, 9-Jun-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) β β’ ((π β LMod β§ π β π« π΅ β§ π β π) β πΉ finSupp 0 ) | ||
Theorem | fsuppmptdmf 47553* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
β’ β²π₯π & β’ πΉ = (π₯ β π΄ β¦ π) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π β π) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | lmodvsmdi 47554 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ πΈ = (.gβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β β0 β§ π β π)) β (π Β· (π β π)) = ((ππΈπ ) Β· π)) | ||
Theorem | gsumlsscl 47555* | Closure of a group sum in a linear subspace: A (finitely supported) sum of scalar multiplications of vectors of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π = (LSubSpβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) β β’ ((π β LMod β§ π β π β§ π β π) β ((πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ )) β (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π βπ)π£))) β π)) | ||
Theorem | assaascl0 47556 | The scalar 0 embedded into an associative algebra corresponds to the 0 of the associative algebra. (Contributed by AV, 31-Jul-2019.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β AssAlg) β β’ (π β (π΄β(0gβπΉ)) = (0gβπ)) | ||
Theorem | assaascl1 47557 | The scalar 1 embedded into an associative algebra corresponds to the 1 of the an associative algebra. (Contributed by AV, 31-Jul-2019.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β AssAlg) β β’ (π β (π΄β(1rβπΉ)) = (1rβπ)) | ||
Theorem | ply1vr1smo 47558 | The variable in a polynomial expressed as scaled monomial. (Contributed by AV, 12-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ 1 = (1rβπ ) & β’ Β· = ( Β·π βπ) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (var1βπ ) β β’ (π β Ring β ( 1 Β· (1 β π)) = π) | ||
Theorem | ply1sclrmsm 47559 | The ring multiplication of a polynomial with a scalar polynomial is equal to the scalar multiplication of the polynomial with the corresponding scalar. (Contributed by AV, 14-Aug-2019.) |
β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ πΈ = (Baseβπ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΎ β§ π β πΈ) β ((π΄βπΉ) Γ π) = (πΉ Β· π)) | ||
Theorem | coe1id 47560* | Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ πΌ = (1rβπ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β (coe1βπΌ) = (π₯ β β0 β¦ if(π₯ = 0, 1 , 0 ))) | ||
Theorem | coe1sclmulval 47561 | The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ π = ( Β·π βπ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β πΎ β§ π β π΅) β§ π β β0) β ((coe1β(πππ))βπ) = (π Β· ((coe1βπ)βπ))) | ||
Theorem | ply1mulgsumlem1 47562* | Lemma 1 for ply1mulgsum 47566. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0 (π < π β ((π΄βπ) = (0gβπ ) β§ (πΆβπ) = (0gβπ )))) | ||
Theorem | ply1mulgsumlem2 47563* | Lemma 2 for ply1mulgsum 47566. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0 (π < π β (π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ ))) | ||
Theorem | ply1mulgsumlem3 47564* | Lemma 3 for ply1mulgsum 47566. (Contributed by AV, 20-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (π β β0 β¦ (π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))))) finSupp (0gβπ )) | ||
Theorem | ply1mulgsumlem4 47565* | Lemma 4 for ply1mulgsum 47566. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (π β β0 β¦ ((π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))) finSupp (0gβπ)) | ||
Theorem | ply1mulgsum 47566* | The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (πΎ Γ πΏ) = (π Ξ£g (π β β0 β¦ ((π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))))) | ||
Theorem | evl1at0 47567 | Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (π β CRing β ((πβπ)β 0 ) = 0 ) | ||
Theorem | evl1at1 47568 | Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (1rβπ) β β’ (π β CRing β ((πβπΌ)β 1 ) = 1 ) | ||
Theorem | linply1 47569 | A term of the form π₯ β πΆ is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 26112). (Contributed by AV, 3-Jul-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) & β’ πΊ = (π β (π΄βπΆ)) & β’ (π β πΆ β πΎ) & β’ (π β π β Ring) β β’ (π β πΊ β π΅) | ||
Theorem | lineval 47570 | A term of the form π₯ β πΆ evaluated for π₯ = π results in π β πΆ (part of ply1remlem 26112). (Contributed by AV, 3-Jul-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) & β’ πΊ = (π β (π΄βπΆ)) & β’ (π β πΆ β πΎ) & β’ π = (eval1βπ ) & β’ (π β π β CRing) & β’ (π β π β πΎ) β β’ (π β ((πβπΊ)βπ) = (π(-gβπ )πΆ)) | ||
Theorem | linevalexample 47571 | The polynomial π₯ β 3 over β€ evaluated for π₯ = 5 results in 2. (Contributed by AV, 3-Jul-2019.) |
β’ π = (Poly1ββ€ring) & β’ π΅ = (Baseβπ) & β’ π = (var1ββ€ring) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) & β’ πΊ = (π β (π΄β3)) & β’ π = (eval1ββ€ring) β β’ ((πβ(π β (π΄β3)))β5) = 2 | ||
In the following, alternative definitions for diagonal and scalar matrices are provided. These definitions define diagonal and scalar matrices as extensible structures, whereas Definitions df-dmat 22405 and df-scmat 22406 define diagonal and scalar matrices as sets. | ||
Syntax | cdmatalt 47572 | Alternative notation for the algebra of diagonal matrices. |
class DMatALT | ||
Syntax | cscmatalt 47573 | Alternative notation for the algebra of scalar matrices. |
class ScMatALT | ||
Definition | df-dmatalt 47574* | Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in [Roman] p. 4 or Definition 3.12 in [Hefferon] p. 240. (Contributed by AV, 8-Dec-2019.) |
β’ DMatALT = (π β Fin, π β V β¦ β¦(π Mat π) / πβ¦(π βΎs {π β (Baseβπ) β£ βπ β π βπ β π (π β π β (πππ) = (0gβπ))})) | ||
Definition | df-scmatalt 47575* | Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cIn";. (Contributed by AV, 8-Dec-2019.) |
β’ ScMatALT = (π β Fin, π β V β¦ β¦(π Mat π) / πβ¦(π βΎs {π β (Baseβπ) β£ βπ β (Baseβπ)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ))})) | ||
Theorem | dmatALTval 47576* | The algebra of π x π diagonal matrices over a ring π . (Contributed by AV, 8-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ ) & β’ π· = (π DMatALT π ) β β’ ((π β Fin β§ π β V) β π· = (π΄ βΎs {π β π΅ β£ βπ β π βπ β π (π β π β (πππ) = 0 )})) | ||
Theorem | dmatALTbas 47577* | The base set of the algebra of π x π diagonal matrices over a ring π , i.e. the set of all π x π diagonal matrices over the ring π . (Contributed by AV, 8-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ ) & β’ π· = (π DMatALT π ) β β’ ((π β Fin β§ π β V) β (Baseβπ·) = {π β π΅ β£ βπ β π βπ β π (π β π β (πππ) = 0 )}) | ||
Theorem | dmatALTbasel 47578* | An element of the base set of the algebra of π x π diagonal matrices over a ring π , i.e. an π x π diagonal matrix over the ring π . (Contributed by AV, 8-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ ) & β’ π· = (π DMatALT π ) β β’ ((π β Fin β§ π β V) β (π β (Baseβπ·) β (π β π΅ β§ βπ β π βπ β π (π β π β (πππ) = 0 )))) | ||
Theorem | dmatbas 47579 | The set of all π x π diagonal matrices over (the ring) π is the base set of the algebra of π x π diagonal matrices over (the ring) π . (Contributed by AV, 8-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ ) & β’ π· = (π DMat π ) β β’ ((π β Fin β§ π β π) β π· = (Baseβ(π DMatALT π ))) | ||
According to Wikipedia ("Linear combination", 29-Mar-2019,
https://en.wikipedia.org/wiki/Linear_combination) "In mathematics, a
linear combination is an expression constructed from a set of terms by
multiplying each term by a constant and adding the results (e.g., a linear
combination of x and y would be any expression of the form ax + by, where a
and b are constants). The concept of linear combinations is central to
linear algebra and related fields of mathematics." In linear algebra, these
"terms" are "vectors" (elements from vector spaces or left modules), and the
constants are elements of the underlying field resp. ring. This corresponds
to the definition in [Lang] p. 129: "Let M be a module over a ring A and let
S be a subset of M. By a linear combination of elements of S (with
coefficients in A) one means a sum βx βS
axx where {ax} is a set of elements of A, ...". In the
definition in [Lang] p. 129, it is additionally claimed that "..., almost all
of which [elements of A] are equal to 0.". This is not necessarily required
in the following definition df-linc 47582, but it is essential if additions and
scalar multiplications of linear combinations are considered. Therefore, we
define the set of all linear combinations with finite support in df-lco 47583,
so that we can show that such sets are submodules of the corresponding
modules, see lincolss 47610.
| ||
Syntax | clinc 47580 | Extend class notation with the operation constructing a linear combination (of vectors from a left module). |
class linC | ||
Syntax | clinco 47581 | Extend class notation with the operation constructing a set of linear combinations (of vectors from a left module) with finite support. |
class LinCo | ||
Definition | df-linc 47582* | Define the operation constructing a linear combination. Although this definition is taylored for linear combinations of vectors from left modules, it can be used for any structure having a Base, Scalar s and a scalar multiplication Β·π . (Contributed by AV, 29-Mar-2019.) |
β’ linC = (π β V β¦ (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π βπ)π₯))))) | ||
Definition | df-lco 47583* | Define the operation constructing the set of all linear combinations for a set of vectors. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 28-Jul-2019.) |
β’ LinCo = (π β V, π£ β π« (Baseβπ) β¦ {π β (Baseβπ) β£ βπ β ((Baseβ(Scalarβπ)) βm π£)(π finSupp (0gβ(Scalarβπ)) β§ π = (π ( linC βπ)π£))}) | ||
Theorem | lincop 47584* | A linear combination as operation. (Contributed by AV, 30-Mar-2019.) |
β’ (π β π β ( linC βπ) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π βπ)π₯))))) | ||
Theorem | lincval 47585* | The value of a linear combination. (Contributed by AV, 30-Mar-2019.) |
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π βπ)π₯)))) | ||
Theorem | dflinc2 47586* | Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019.) |
β’ linC = (π β V β¦ (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π βf ( Β·π βπ)( I βΎ π£))))) | ||
Theorem | lcoop 47587* | A linear combination as operation. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) β β’ ((π β π β§ π β π« π΅) β (π LinCo π) = {π β π΅ β£ βπ β (π βm π)(π finSupp (0gβπ) β§ π = (π ( linC βπ)π))}) | ||
Theorem | lcoval 47588* | The value of a linear combination. (Contributed by AV, 5-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) β β’ ((π β π β§ π β π« π΅) β (πΆ β (π LinCo π) β (πΆ β π΅ β§ βπ β (π βm π)(π finSupp (0gβπ) β§ πΆ = (π ( linC βπ)π))))) | ||
Theorem | lincfsuppcl 47589 | A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉ( linC βπ)π) β π΅) | ||
Theorem | linccl 47590 | A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Baseβ(Scalarβπ)) β β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π βm π))) β (π( linC βπ)π) β π΅) | ||
Theorem | lincval0 47591 | The value of an empty linear combination. (Contributed by AV, 12-Apr-2019.) |
β’ (π β π β (β ( linC βπ)β ) = (0gβπ)) | ||
Theorem | lincvalsng 47592 | The linear combination over a singleton. (Contributed by AV, 25-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β LMod β§ π β π΅ β§ π β π ) β ({β¨π, πβ©} ( linC βπ){π}) = (π Β· π)) | ||
Theorem | lincvalsn 47593 | The linear combination over a singleton. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 25-May-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = {β¨π, πβ©} β β’ ((π β LMod β§ π β π΅ β§ π β π ) β (πΉ( linC βπ){π}) = (π Β· π)) | ||
Theorem | lincvalpr 47594 | The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ πΉ = {β¨π, πβ©, β¨π, πβ©} β β’ (((π β LMod β§ π β π) β§ (π β π΅ β§ π β π ) β§ (π β π΅ β§ π β π )) β (πΉ( linC βπ){π, π}) = ((π Β· π) + (π Β· π))) | ||
Theorem | lincval1 47595 | The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΉ = {β¨π, (0gβπ)β©} β β’ ((π β LMod β§ π β π΅) β (πΉ( linC βπ){π}) = (0gβπ)) | ||
Theorem | lcosn0 47596 | Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΉ = {β¨π, (0gβπ)β©} β β’ ((π β LMod β§ π β π΅) β (πΉ β (π βm {π}) β§ πΉ finSupp (0gβπ) β§ (πΉ( linC βπ){π}) = (0gβπ))) | ||
Theorem | lincvalsc0 47597* | The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ πΉ = (π₯ β π β¦ 0 ) β β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = π) | ||
Theorem | lcoc0 47598* | Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ πΉ = (π₯ β π β¦ 0 ) & β’ π = (Baseβπ) β β’ ((π β LMod β§ π β π« π΅) β (πΉ β (π βm π) β§ πΉ finSupp 0 β§ (πΉ( linC βπ)π) = π)) | ||
Theorem | linc0scn0 47599* | If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) & β’ π = (0gβπ) & β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) β β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = π) | ||
Theorem | lincdifsn 47600 | A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
β’ π΅ = (Baseβπ) & β’ π = (Scalarβπ) & β’ π = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ ) β β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΉ( linC βπ)π) = ((πΊ( linC βπ)(π β {π})) + ((πΉβπ) Β· π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |