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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ringccatALTV 46101 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) β β’ (π β π β πΆ β Cat) | ||
Theorem | ringcidALTV 46102 | The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ 1 = (IdβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ π = (Baseβπ) β β’ (π β ( 1 βπ) = ( I βΎ π)) | ||
Theorem | ringcsectALTV 46103 | A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΈ = (Baseβπ) & β’ π = (SectβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingHom π) β§ πΊ β (π RingHom π) β§ (πΊ β πΉ) = ( I βΎ πΈ)))) | ||
Theorem | ringcinvALTV 46104 | An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (InvβπΆ) β β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RingIso π) β§ πΊ = β‘πΉ))) | ||
Theorem | ringcisoALTV 46105 | An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ πΌ = (IsoβπΆ) β β’ (π β (πΉ β (ππΌπ) β πΉ β (π RingIso π))) | ||
Theorem | ringcbasbasALTV 46106 | An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ πΆ = (RingCatALTVβπ) & β’ π΅ = (BaseβπΆ) & β’ (π β π β WUni) β β’ ((π β§ π β π΅) β (Baseβπ ) β π) | ||
Theorem | funcringcsetclem1ALTV 46107* | Lemma 1 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) | ||
Theorem | funcringcsetclem2ALTV 46108* | Lemma 2 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ ((π β§ π β π΅) β (πΉβπ) β π) | ||
Theorem | funcringcsetclem3ALTV 46109* | Lemma 3 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) β β’ (π β πΉ:π΅βΆπΆ) | ||
Theorem | funcringcsetclem4ALTV 46110* | Lemma 4 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΊ Fn (π΅ Γ π΅)) | ||
Theorem | funcringcsetclem5ALTV 46111* | Lemma 5 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ (π RingHom π))) | ||
Theorem | funcringcsetclem6ALTV 46112* | Lemma 6 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅) β§ π» β (π RingHom π)) β ((ππΊπ)βπ») = π») | ||
Theorem | funcringcsetclem7ALTV 46113* | Lemma 7 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ π β π΅) β ((ππΊπ)β((Idβπ )βπ)) = ((Idβπ)β(πΉβπ))) | ||
Theorem | funcringcsetclem8ALTV 46114* | Lemma 8 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ):(π(Hom βπ )π)βΆ((πΉβπ)(Hom βπ)(πΉβπ))) | ||
Theorem | funcringcsetclem9ALTV 46115* | Lemma 9 for funcringcsetcALTV 46116. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π» β (π(Hom βπ )π) β§ πΎ β (π(Hom βπ )π))) β ((ππΊπ)β(πΎ(β¨π, πβ©(compβπ )π)π»)) = (((ππΊπ)βπΎ)(β¨(πΉβπ), (πΉβπ)β©(compβπ)(πΉβπ))((ππΊπ)βπ»))) | ||
Theorem | funcringcsetcALTV 46116* | The "natural forgetful functor" from the category of rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.) (New usage is discouraged.) |
β’ π = (RingCatALTVβπ) & β’ π = (SetCatβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) & β’ (π β π β WUni) & β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RingHom π¦)))) β β’ (π β πΉ(π Func π)πΊ) | ||
Theorem | irinitoringc 46117 | The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.) |
β’ (π β π β π) & β’ (π β β€ring β π) & β’ πΆ = (RingCatβπ) β β’ (π β β€ring β (InitOβπΆ)) | ||
Theorem | zrtermoringc 46118 | The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RingCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) β β’ (π β π β (TermOβπΆ)) | ||
Theorem | zrninitoringc 46119* | The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RingCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) & β’ (π β βπ β (BaseβπΆ)π β NzRing) β β’ (π β π β (InitOβπΆ)) | ||
Theorem | nzerooringczr 46120 | There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.) |
β’ (π β π β π) & β’ πΆ = (RingCatβπ) & β’ (π β π β (Ring β NzRing)) & β’ (π β π β π) & β’ (π β β€ring β π) β β’ (π β (ZeroOβπΆ) = β ) | ||
Theorem | srhmsubclem1 46121* | Lemma 1 for srhmsubc 46124. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ (π β πΆ β π β (π β© Ring)) | ||
Theorem | srhmsubclem2 46122* | Lemma 2 for srhmsubc 46124. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatβπ))) | ||
Theorem | srhmsubclem3 46123* | Lemma 3 for srhmsubc 46124. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatβπ))π)) | ||
Theorem | srhmsubc 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 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.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | sringcat 46125* | The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | crhmsubc 46126* | 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | cringcat 46127* | 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.) |
β’ πΆ = (π β© CRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | drhmsubc 46128* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β π½ β (Subcatβ(RingCatβπ))) | ||
Theorem | drngcat 46129* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat π½) β Cat) | ||
Theorem | fldcat 46130* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β ((RingCatβπ) βΎcat πΉ) β Cat) | ||
Theorem | fldc 46131* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β (((RingCatβπ) βΎcat π½) βΎcat πΉ) β Cat) | ||
Theorem | fldhmsubc 46132* | 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.) |
β’ πΆ = (π β© DivRing) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) & β’ π· = (π β© Field) & β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) β β’ (π β π β πΉ β (Subcatβ((RingCatβπ) βΎcat π½))) | ||
Theorem | rngcrescrhm 46133 | 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 46134 | Lemma 1 for rhmsubc 46138. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubclem2 46135 | Lemma 2 for rhmsubc 46138. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubclem3 46136* | Lemma 3 for rhmsubc 46138. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubclem4 46137* | Lemma 4 for rhmsubc 46138. (Contributed by AV, 2-Mar-2020.) |
β’ (π β π β π) & β’ πΆ = (RngCatβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubc 46138 | 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 46139 | 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 46140* | Lemma 1 for srhmsubcALTV 46142. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) β β’ ((π β π β§ π β πΆ) β π β (Baseβ(RingCatALTVβπ))) | ||
Theorem | srhmsubcALTVlem2 46141* | Lemma 2 for srhmsubcALTV 46142. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
β’ βπ β π π β Ring & β’ πΆ = (π β© π) & β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) β β’ ((π β π β§ (π β πΆ β§ π β πΆ)) β (ππ½π) = (π(Hom β(RingCatALTVβπ))π)) | ||
Theorem | srhmsubcALTV 46142* | 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 46143* | 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 46144* | 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 46145* | 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 46146* | 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 46147* | 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 46148* | 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 46149* | 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 46150* | 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 46151 | 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 46152 | Lemma 1 for rhmsubcALTV 46156. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ (π β π» Fn (π Γ π )) | ||
Theorem | rhmsubcALTVlem2 46153 | Lemma 2 for rhmsubcALTV 46156. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π β π β§ π β π ) β (ππ»π) = (π RingHom π)) | ||
Theorem | rhmsubcALTVlem3 46154* | Lemma 3 for rhmsubcALTV 46156. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((π β§ π₯ β π ) β ((Idβ(RngCatALTVβπ))βπ₯) β (π₯π»π₯)) | ||
Theorem | rhmsubcALTVlem4 46155* | Lemma 4 for rhmsubcALTV 46156. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
β’ (π β π β π) & β’ πΆ = (RngCatALTVβπ) & β’ (π β π = (Ring β© π)) & β’ π» = ( RingHom βΎ (π Γ π )) β β’ ((((π β§ π₯ β π ) β§ (π¦ β π β§ π§ β π )) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatALTVβπ))π§)π) β (π₯π»π§)) | ||
Theorem | rhmsubcALTV 46156 | 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 46157 | 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 46158 | 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 46159* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5790. (Contributed by AV, 30-Mar-2019.) |
β’ (πΆ β βͺ π¦ β π΅ (π΄ Γ {π¦}) β βπ₯βπ¦(πΆ = β¨π₯, π¦β© β§ (π₯ β π΄ β§ π¦ β π΅))) | ||
Theorem | mpomptx2 46160* | 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 46161* | 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 46162* | 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 46163* | 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 46164* | 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 46165* | 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 46166* | 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 46167* | 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 46168* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
β’ (π β π΄ β π) & β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΄) β β’ (π β (πΉ βf π πΊ) = (π₯ β π΄ β¦ ((πΉβπ₯)π (πΊβπ₯)))) | ||
Theorem | ofaddmndmap 46169 | 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 46170 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
β’ πΉ = {β¨π, πβ©} β β’ ((π β π β§ π β π β§ π β π) β πΉ β (π βm {π})) | ||
Theorem | fprmappr 46171 | 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 46172 | 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 46173 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
β’ ((π β β€ β§ π΄ β β β§ π΅ β β) β ((π Β· π΄) = π΅ β π΄ = π΅)) | ||
Theorem | 2t6m3t4e0 46174 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
β’ ((2 Β· 6) β (3 Β· 4)) = 0 | ||
Theorem | ssnn0ssfz 46175* | For any finite subset of β0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 31485. (Contributed by AV, 30-Sep-2019.) |
β’ (π΄ β (π« β0 β© Fin) β βπ β β0 π΄ β (0...π)) | ||
Theorem | nn0sumltlt 46176 | 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 46177 | 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 46178* | 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 46177) instead of the binomial theorem (binom 15650) , see altgsumbcALT 46179. (Contributed by AV, 13-Sep-2019.) |
β’ (π β β β Ξ£π β (0...π)((-1βπ) Β· (πCπ)) = 0) | ||
Theorem | altgsumbcALT 46179* | Alternate proof of altgsumbc 46178, using Pascal's rule (bcpascm1 46177) 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 46180 | 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 46181 | 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 46182 | 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 46183 | 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 46184 | 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 46185 | 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 46186 | 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 46187* | 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 46188* | 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 46189* | 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 46190 | 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 46191 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ ((π΄ β π β§ (β―βπ΄) β€ 2) β πΊ β Abel) | ||
Theorem | pgrpgt2nabl 46192 | 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 46193 | 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 46194* | 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 46195* | 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 46196* | 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 46197 | 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 46198* | 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 46199* | 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 46200* | 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βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |