![]() |
Metamath
Proof Explorer Theorem List (p. 432 of 437) | < 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | srhmsubc 43101* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43102* | 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 43103* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43104* | 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 43105* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43106* | 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 43107* | 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 43108* | 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 43109* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43110 | 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 43111 | Lemma 1 for rhmsubc 43115. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
Theorem | rhmsubclem2 43112 | Lemma 2 for rhmsubc 43115. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | rhmsubclem3 43113* | Lemma 3 for rhmsubc 43115. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rhmsubclem4 43114* | Lemma 4 for rhmsubc 43115. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rhmsubc 43115 | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43116 | 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 43117* | Lemma 1 for srhmsubcALTV 43119. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCatALTV‘𝑈))) | ||
Theorem | srhmsubcALTVlem2 43118* | Lemma 2 for srhmsubcALTV 43119. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCatALTV‘𝑈))𝑌)) | ||
Theorem | srhmsubcALTV 43119* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43120* | 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 43121* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43122* | 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 43123* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43124* | 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 43125* | 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 43126* | 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 43127* | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43128 | 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 43129 | Lemma 1 for rhmsubcALTV 43133. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
Theorem | rhmsubcALTVlem2 43130 | Lemma 2 for rhmsubcALTV 43133. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | rhmsubcALTVlem3 43131* | Lemma 3 for rhmsubcALTV 43133. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rhmsubcALTVlem4 43132* | Lemma 4 for rhmsubcALTV 43133. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rhmsubcALTV 43133 | According to df-subc 16861, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 16889 and subcss2 16892). 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 43134 | 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 | xpprsng 43135 | The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {〈𝐴, 𝐶〉, 〈𝐵, 𝐶〉}) | ||
Theorem | opeliun2xp 43136 | Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5418. (Contributed by AV, 30-Mar-2019.) |
⊢ (〈𝐶, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eliunxp2 43137* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5507. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | mpt2mptx2 43138* | 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 mpt2mptx 7030. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | cbvmpt2x2 43139* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 7013 allows 𝐴 to be a function of 𝑦, analogous to cbvmpt2x 7012. (Contributed by AV, 30-Mar-2019.) |
⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐷 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷) & ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | dmmpt2ssx2 43140* | The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpt2ssx 7517. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | ||
Theorem | mpt2exxg2 43141* | 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 mpt2exxg 7526. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | ovmpt2rdxf 43142* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 7065. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2rdx 43143* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 7065. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpt2x2 43144* | The value of an operation class abstraction. Variant of ovmpt2ga 7069 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | fdmdifeqresdif 43145* | 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 43146* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | ofaddmndmap 43147 | 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 ∧ 𝑉 ∈ 𝑌 ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓 + 𝐵) ∈ (𝑅 ↑𝑚 𝑉)) | ||
Theorem | mapsnop 43148 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑𝑚 {𝑋})) | ||
Theorem | mapprop 43149 | An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅) ∧ (𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅) ∧ (𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊)) → 𝐹 ∈ (𝑅 ↑𝑚 {𝑋, 𝑌})) | ||
Theorem | ztprmneprm 43150 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | 2t6m3t4e0 43151 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
⊢ ((2 · 6) − (3 · 4)) = 0 | ||
Theorem | ssnn0ssfz 43152* | For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 30117. (Contributed by AV, 30-Sep-2019.) |
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛)) | ||
Theorem | nn0sumltlt 43153 | 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 43154 | 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 43155* | 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 43154) instead of the binomial theorem (binom 14970) , see altgsumbcALT 43156. (Contributed by AV, 13-Sep-2019.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | altgsumbcALT 43156* | Alternate proof of altgsumbc 43155, using Pascal's rule (bcpascm1 43154) instead of the binomial theorem (binom 14970). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | zlmodzxzlmod 43157 | 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 43158 | 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 43159 | 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 43160 | 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 43161 | 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 43162 | 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 43163 | 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 | gsumpr 43164* | Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁} ↦ 𝐴)) = (𝐶 + 𝐷)) | ||
Theorem | mgpsumunsn 43165* | 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 43166* | 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 43167* | 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 | gsumsplit2f 43168* | Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋)))) | ||
Theorem | gsumdifsndf 43169* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑘𝑌 & ⊢ Ⅎ𝑘𝜑 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌)) | ||
Theorem | exple2lt6 43170 | 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 43171 | Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) ≤ 2) → 𝐺 ∈ Abel) | ||
Theorem | pgrpgt2nabl 43172 | 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 43173 | 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 43174* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = ∅) | ||
Theorem | domnmsuppn0 43175* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = (𝐴 supp (0g‘𝑀))) | ||
Theorem | rmsuppss 43176* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑀))) | ||
Theorem | mndpsuppss 43177 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓 (+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) | ||
Theorem | scmsuppss 43178* | 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‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑆))) | ||
Theorem | rmsuppfi 43179* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝐴 supp (0g‘𝑀)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | rmfsupp 43180* | 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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑀)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) finSupp (0g‘𝑀)) | ||
Theorem | mndpsuppfi 43181 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ ((𝐴 supp (0g‘𝑀)) ∈ Fin ∧ (𝐵 supp (0g‘𝑀)) ∈ Fin)) → ((𝐴 ∘𝑓 (+g‘𝑀)𝐵) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | mndpfsupp 43182 | 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 ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑀) ∧ 𝐵 finSupp (0g‘𝑀))) → (𝐴 ∘𝑓 (+g‘𝑀)𝐵) finSupp (0g‘𝑀)) | ||
Theorem | scmsuppfi 43183* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝐴 supp (0g‘𝑆)) ∈ Fin) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) supp (0g‘𝑀)) ∈ Fin) | ||
Theorem | scmfsupp 43184* | 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‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠 ‘𝑀)𝑣)) finSupp (0g‘𝑀)) | ||
Theorem | suppmptcfin 43185* | 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 43186* | 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 43187* | A mapping with a finite domain is finitely supported. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | lmodvsmdi 43188 | Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ ↑ = (.g‘𝑊) & ⊢ 𝐸 = (.g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑁 ↑ 𝑋)) = ((𝑁𝐸𝑅) · 𝑋)) | ||
Theorem | gsumlsscl 43189* | 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 ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) ∈ 𝑍)) | ||
Theorem | ascl0 43190 | The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘(0g‘𝐹)) = (0g‘𝑊)) | ||
Theorem | ascl1 43191 | The scalar 1 embedded into a left module corresponds to the 1 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘(1r‘𝐹)) = (1r‘𝑊)) | ||
Theorem | assaascl0 43192 | 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 43193 | 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 43194 | 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 43195 | Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐴 · 𝑋) × 𝑌) = (𝐴 · (𝑋 × 𝑌))) | ||
Theorem | ply1sclrmsm 43196 | 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 43197* | 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 43198 | 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 43199* | Lemma 1 for ply1mulgsum 43203. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝐴‘𝑛) = (0g‘𝑅) ∧ (𝐶‘𝑛) = (0g‘𝑅)))) | ||
Theorem | ply1mulgsumlem2 43200* | Lemma 2 for ply1mulgsum 43203. (Contributed by AV, 19-Oct-2019.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (coe1‘𝐾) & ⊢ 𝐶 = (coe1‘𝐿) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ × = (.r‘𝑃) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑀) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴‘𝑙) ∗ (𝐶‘(𝑛 − 𝑙))))) = (0g‘𝑅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |