Home | Metamath
Proof Explorer Theorem List (p. 462 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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rngcrescrhm 46101 | The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π ) sSet β¨(Hom βndx), π»β©)) | ||
Theorem | rhmsubclem1 46102 | Lemma 1 for rhmsubc 46106. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubclem2 46103 | Lemma 2 for rhmsubc 46106. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubclem3 46104* | Lemma 3 for rhmsubc 46106. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubclem4 46105* | Lemma 4 for rhmsubc 46106. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubc 46106 | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» β (Subcatβ(RngCatβπ))) | ||
Theorem | rhmsubccat 46107 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β ((RngCatβπ) βΎcat π») β Cat) | ||
Theorem | srhmsubcALTVlem1 46108* | Lemma 1 for srhmsubcALTV 46110. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatALTVβπ))) | ||
Theorem | srhmsubcALTVlem2 46109* | Lemma 2 for srhmsubcALTV 46110. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatALTVβπ))π)) | ||
Theorem | srhmsubcALTV 46110* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | sringcatALTV 46111* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubcALTV 46112* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | cringcatALTV 46113* | The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | drhmsubcALTV 46114* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatALTVβπ))) | ||
Theorem | drngcatALTV 46115* | The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatALTVβπ) βΎcat π½) β Cat) | ||
Theorem | fldcatALTV 46116* | 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 46117* | 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 46118* | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). 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 | rngcrescrhmALTV 46119 | The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π ) sSet β¨(Hom βndx), π»β©)) | ||
Theorem | rhmsubcALTVlem1 46120 | Lemma 1 for rhmsubcALTV 46124. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubcALTVlem2 46121 | Lemma 2 for rhmsubcALTV 46124. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubcALTVlem3 46122* | Lemma 3 for rhmsubcALTV 46124. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatALTVβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcALTVlem4 46123* | Lemma 4 for rhmsubcALTV 46124. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatALTVβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcALTV 46124 | According to df-subc 17630, the subcategories (SubcatβπΆ) of a category πΆ are subsets of the homomorphisms of πΆ (see subcssc 17661 and subcss2 17664). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» β (Subcatβ(RngCatALTVβπ))) | ||
Theorem | rhmsubcALTVcat 46125 | The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β ((RngCatALTVβπ) βΎcat π») β Cat) | ||
Theorem | opeliun2xp 46126 | Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5696. (Contributed by AV, 30-Mar-2019.) |
β’ (β¨πΆ, π¦β© β βͺ π¦ β π΅ (π΄ Γ {π¦}) β (π¦ β π΅ β§ πΆ β π΄)) | ||
Theorem | eliunxp2 46127* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5790. (Contributed by AV, 30-Mar-2019.) |
β’ (πΆ β βͺ π¦ β π΅ (π΄ Γ {π¦}) β βπ₯βπ¦(πΆ = β¨π₯, π¦β© β§ (π₯ β π΄ β§ π¦ β π΅))) | ||
Theorem | mpomptx2 46128* | 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 7462. (Contributed by AV, 30-Mar-2019.) |
β’ (π§ = β¨π₯, π¦β© β πΆ = π·) β β’ (π§ β βͺ π¦ β π΅ (π΄ Γ {π¦}) β¦ πΆ) = (π₯ β π΄, π¦ β π΅ β¦ π·) | ||
Theorem | cbvmpox2 46129* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7444 allows π΄ to be a function of π¦, analogous to cbvmpox 7443. (Contributed by AV, 30-Mar-2019.) |
β’ β²π§π΄ & β’ β²π¦π· & β’ β²π§πΆ & β’ β²π€πΆ & β’ β²π₯πΈ & β’ β²π¦πΈ & β’ (π¦ = π§ β π΄ = π·) & β’ ((π¦ = π§ β§ π₯ = π€) β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π€ β π·, π§ β π΅ β¦ πΈ) | ||
Theorem | dmmpossx2 46130* | 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 7987. (Contributed by AV, 30-Mar-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ dom πΉ β βͺ π¦ β π΅ (π΄ Γ {π¦}) | ||
Theorem | mpoexxg2 46131* | 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 7997. (Contributed by AV, 30-Mar-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((π΅ β π β§ βπ¦ β π΅ π΄ β π) β πΉ β V) | ||
Theorem | ovmpordxf 46132* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7498. (Contributed by AV, 30-Mar-2019.) |
β’ (π β πΉ = (π₯ β πΆ, π¦ β π· β¦ π )) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β π = π) & β’ ((π β§ π¦ = π΅) β πΆ = πΏ) & β’ (π β π΄ β πΏ) & β’ (π β π΅ β π·) & β’ (π β π β π) & β’ β²π₯π & β’ β²π¦π & β’ β²π¦π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π¦π β β’ (π β (π΄πΉπ΅) = π) | ||
Theorem | ovmpordx 46133* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7498. (Contributed by AV, 30-Mar-2019.) |
β’ (π β πΉ = (π₯ β πΆ, π¦ β π· β¦ π )) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β π = π) & β’ ((π β§ π¦ = π΅) β πΆ = πΏ) & β’ (π β π΄ β πΏ) & β’ (π β π΅ β π·) & β’ (π β π β π) β β’ (π β (π΄πΉπ΅) = π) | ||
Theorem | ovmpox2 46134* | The value of an operation class abstraction. Variant of ovmpoga 7502 which does not require π· and π₯ to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ ((π₯ = π΄ β§ π¦ = π΅) β π = π) & β’ (π¦ = π΅ β πΆ = πΏ) & β’ πΉ = (π₯ β πΆ, π¦ β π· β¦ π ) β β’ ((π΄ β πΏ β§ π΅ β π· β§ π β π») β (π΄πΉπ΅) = π) | ||
Theorem | fdmdifeqresdif 46135* | 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 46136* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
β’ (π β π΄ β π) & β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΄) β β’ (π β (πΉ βf π πΊ) = (π₯ β π΄ β¦ ((πΉβπ₯)π (πΊβπ₯)))) | ||
Theorem | ofaddmndmap 46137 | 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 46138 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
β’ πΉ = {β¨π, πβ©} β β’ ((π β π β§ π β π β§ π β π) β πΉ β (π βm {π})) | ||
Theorem | fprmappr 46139 | 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 46140 | 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 46141 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
β’ ((π β β€ β§ π΄ β β β§ π΅ β β) β ((π Β· π΄) = π΅ β π΄ = π΅)) | ||
Theorem | 2t6m3t4e0 46142 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
β’ ((2 Β· 6) β (3 Β· 4)) = 0 | ||
Theorem | ssnn0ssfz 46143* | For any finite subset of β0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 31472. (Contributed by AV, 30-Sep-2019.) |
β’ (π΄ β (π« β0 β© Fin) β βπ β β0 π΄ β (0...π)) | ||
Theorem | nn0sumltlt 46144 | 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 46145 | 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 46146* | 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 46145) instead of the binomial theorem (binom 15650) , see altgsumbcALT 46147. (Contributed by AV, 13-Sep-2019.) |
β’ (π β β β Ξ£π β (0...π)((-1βπ) Β· (πCπ)) = 0) | ||
Theorem | altgsumbcALT 46147* | Alternate proof of altgsumbc 46146, using Pascal's rule (bcpascm1 46145) instead of the binomial theorem (binom 15650). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β β Ξ£π β (0...π)((-1βπ) Β· (πCπ)) = 0) | ||
Theorem | zlmodzxzlmod 46148 | 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 46149 | 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 46150 | 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 46151 | 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 46152 | 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 46153 | 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 46154 | 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 46155* | 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 46156* | 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 46157* | 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 46158 | 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 46159 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ ((π΄ β π β§ (β―βπ΄) β€ 2) β πΊ β Abel) | ||
Theorem | pgrpgt2nabl 46160 | 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 46161 | 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 46162* | 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 46163* | 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 46164* | 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 46165 | 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 46166* | 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 46167* | 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 46168* | 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 46169 | 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 46170 | 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 46171* | 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 46172* | 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 46173* | 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 46174* | 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 46175* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
β’ β²π₯π & β’ πΉ = (π₯ β π΄ β¦ π) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π β π) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | lmodvsmdi 46176 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ πΈ = (.gβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β β0 β§ π β π)) β (π Β· (π β π)) = ((ππΈπ ) Β· π)) | ||
Theorem | gsumlsscl 46177* | 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 46178 | 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 46179 | 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 46180 | 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 | ply1ass23l 46181 | Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.) |
β’ π = (Poly1βπ ) & β’ Γ = (.rβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) β β’ ((π β Ring β§ (π΄ β πΎ β§ π β π΅ β§ π β π΅)) β ((π΄ Β· π) Γ π) = (π΄ Β· (π Γ π))) | ||
Theorem | ply1sclrmsm 46182 | 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 46183* | 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 46184 | 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 46185* | Lemma 1 for ply1mulgsum 46189. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0 (π < π β ((π΄βπ) = (0gβπ ) β§ (πΆβπ) = (0gβπ )))) | ||
Theorem | ply1mulgsumlem2 46186* | Lemma 2 for ply1mulgsum 46189. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0 (π < π β (π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ ))) | ||
Theorem | ply1mulgsumlem3 46187* | Lemma 3 for ply1mulgsum 46189. (Contributed by AV, 20-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (π β β0 β¦ (π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))))) finSupp (0gβπ )) | ||
Theorem | ply1mulgsumlem4 46188* | Lemma 4 for ply1mulgsum 46189. (Contributed by AV, 19-Oct-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (coe1βπΎ) & β’ πΆ = (coe1βπΏ) & β’ π = (var1βπ ) & β’ Γ = (.rβπ) & β’ Β· = ( Β·π βπ) & β’ β = (.rβπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (π β β0 β¦ ((π Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))) finSupp (0gβπ)) | ||
Theorem | ply1mulgsum 46189* | 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 46190 | Polynomial evaluation for the 0 scalar. (Contributed by AV, 10-Aug-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) β β’ (π β CRing β ((πβπ)β 0 ) = 0 ) | ||
Theorem | evl1at1 46191 | Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019.) |
β’ π = (eval1βπ ) & β’ π = (Poly1βπ ) & β’ 1 = (1rβπ ) & β’ πΌ = (1rβπ) β β’ (π β CRing β ((πβπΌ)β 1 ) = 1 ) | ||
Theorem | linply1 46192 | A term of the form π₯ β πΆ is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem 25449). (Contributed by AV, 3-Jul-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) & β’ πΊ = (π β (π΄βπΆ)) & β’ (π β πΆ β πΎ) & β’ (π β π β Ring) β β’ (π β πΊ β π΅) | ||
Theorem | lineval 46193 | A term of the form π₯ β πΆ evaluated for π₯ = π results in π β πΆ (part of ply1remlem 25449). (Contributed by AV, 3-Jul-2019.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π = (var1βπ ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) & β’ πΊ = (π β (π΄βπΆ)) & β’ (π β πΆ β πΎ) & β’ π = (eval1βπ ) & β’ (π β π β CRing) & β’ (π β π β πΎ) β β’ (π β ((πβπΊ)βπ) = (π(-gβπ )πΆ)) | ||
Theorem | linevalexample 46194 | 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 21761 and df-scmat 21762 define diagonal and scalar matrices as sets. | ||
Syntax | cdmatalt 46195 | Alternative notation for the algebra of diagonal matrices. |
class DMatALT | ||
Syntax | cscmatalt 46196 | Alternative notation for the algebra of scalar matrices. |
class ScMatALT | ||
Definition | df-dmatalt 46197* | 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 46198* | 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 46199* | 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 46200* | 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 )}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |