Home | Metamath
Proof Explorer Theorem List (p. 457 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ringcinv 45601 | An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐶 = (RingCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ 𝐺 = ◡𝐹))) | ||
Theorem | ringciso 45602 | An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐶 = (RingCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌))) | ||
Theorem | ringcbasbas 45603 | An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) |
⊢ 𝐶 = (RingCat‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ WUni) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ 𝐵) → (Base‘𝑅) ∈ 𝑈) | ||
Theorem | funcringcsetc 45604* | The "natural forgetful functor" from the category of unital 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, 26-Mar-2020.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | funcringcsetcALTV2lem1 45605* | Lemma 1 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) | ||
Theorem | funcringcsetcALTV2lem2 45606* | Lemma 2 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcringcsetcALTV2lem3 45607* | Lemma 3 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcringcsetcALTV2lem4 45608* | Lemma 4 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcringcsetcALTV2lem5 45609* | Lemma 5 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑋 RingHom 𝑌))) | ||
Theorem | funcringcsetcALTV2lem6 45610* | Lemma 6 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑋 RingHom 𝑌)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcringcsetcALTV2lem7 45611* | Lemma 7 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
Theorem | funcringcsetcALTV2lem8 45612* | Lemma 8 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑅)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) | ||
Theorem | funcringcsetcALTV2lem9 45613* | Lemma 9 for funcringcsetcALTV2 45614. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑅)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑅)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑅)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcringcsetcALTV2 45614* | The "natural forgetful functor" from the category of unital 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.) |
⊢ 𝑅 = (RingCat‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) | ||
Theorem | ringcbasALTV 45615 | Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Ring)) | ||
Theorem | ringchomfvalALTV 45616* | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RingHom 𝑦))) | ||
Theorem | ringchomALTV 45617 | Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | elringchomALTV 45618 | A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
Theorem | ringccofvalALTV 45619* | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RingHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RingHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) | ||
Theorem | ringccoALTV 45620 | Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 RingHom 𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌 RingHom 𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
Theorem | ringccatidALTV 45621* | Lemma for ringccatALTV 45622. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥))))) | ||
Theorem | ringccatALTV 45622 | The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.) |
⊢ 𝐶 = (RingCatALTV‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
Theorem | ringcidALTV 45623 | 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 45624 | 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 45625 | 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 45626 | 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 45627 | 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 45628* | Lemma 1 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (Base‘𝑋)) | ||
Theorem | funcringcsetclem2ALTV 45629* | Lemma 2 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝑈) | ||
Theorem | funcringcsetclem3ALTV 45630* | Lemma 3 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) | ||
Theorem | funcringcsetclem4ALTV 45631* | Lemma 4 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) | ||
Theorem | funcringcsetclem5ALTV 45632* | Lemma 5 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌) = ( I ↾ (𝑋 RingHom 𝑌))) | ||
Theorem | funcringcsetclem6ALTV 45633* | Lemma 6 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝐻 ∈ (𝑋 RingHom 𝑌)) → ((𝑋𝐺𝑌)‘𝐻) = 𝐻) | ||
Theorem | funcringcsetclem7ALTV 45634* | Lemma 7 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → ((𝑋𝐺𝑋)‘((Id‘𝑅)‘𝑋)) = ((Id‘𝑆)‘(𝐹‘𝑋))) | ||
Theorem | funcringcsetclem8ALTV 45635* | Lemma 8 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐺𝑌):(𝑋(Hom ‘𝑅)𝑌)⟶((𝐹‘𝑋)(Hom ‘𝑆)(𝐹‘𝑌))) | ||
Theorem | funcringcsetclem9ALTV 45636* | Lemma 9 for funcringcsetcALTV 45637. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.) |
⊢ 𝑅 = (RingCatALTV‘𝑈) & ⊢ 𝑆 = (SetCat‘𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝐻 ∈ (𝑋(Hom ‘𝑅)𝑌) ∧ 𝐾 ∈ (𝑌(Hom ‘𝑅)𝑍))) → ((𝑋𝐺𝑍)‘(𝐾(〈𝑋, 𝑌〉(comp‘𝑅)𝑍)𝐻)) = (((𝑌𝐺𝑍)‘𝐾)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉(comp‘𝑆)(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝐻))) | ||
Theorem | funcringcsetcALTV 45637* | 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 45638 | 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 45639 | 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 45640* | 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 45641 | 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 45642* | Lemma 1 for srhmsubc 45645. (Contributed by AV, 19-Feb-2020.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) ⇒ ⊢ (𝑋 ∈ 𝐶 → 𝑋 ∈ (𝑈 ∩ Ring)) | ||
Theorem | srhmsubclem2 45643* | Lemma 2 for srhmsubc 45645. (Contributed by AV, 19-Feb-2020.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCat‘𝑈))) | ||
Theorem | srhmsubclem3 45644* | Lemma 3 for srhmsubc 45645. (Contributed by AV, 19-Feb-2020.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCat‘𝑈))𝑌)) | ||
Theorem | srhmsubc 45645* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45646* | 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 45647* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45648* | 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 45649* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45650* | 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 45651* | 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 45652* | 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 45653* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45654 | 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 45655 | Lemma 1 for rhmsubc 45659. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
Theorem | rhmsubclem2 45656 | Lemma 2 for rhmsubc 45659. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | rhmsubclem3 45657* | Lemma 3 for rhmsubc 45659. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCat‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rhmsubclem4 45658* | Lemma 4 for rhmsubc 45659. (Contributed by AV, 2-Mar-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCat‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCat‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rhmsubc 45659 | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45660 | 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 45661* | Lemma 1 for srhmsubcALTV 45663. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ (Base‘(RingCatALTV‘𝑈))) | ||
Theorem | srhmsubcALTVlem2 45662* | Lemma 2 for srhmsubcALTV 45663. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.) |
⊢ ∀𝑟 ∈ 𝑆 𝑟 ∈ Ring & ⊢ 𝐶 = (𝑈 ∩ 𝑆) & ⊢ 𝐽 = (𝑟 ∈ 𝐶, 𝑠 ∈ 𝐶 ↦ (𝑟 RingHom 𝑠)) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋𝐽𝑌) = (𝑋(Hom ‘(RingCatALTV‘𝑈))𝑌)) | ||
Theorem | srhmsubcALTV 45663* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45664* | 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 45665* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45666* | 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 45667* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45668* | 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 45669* | 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 45670* | 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 45671* | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45672 | 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 45673 | Lemma 1 for rhmsubcALTV 45677. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
Theorem | rhmsubcALTVlem2 45674 | Lemma 2 for rhmsubcALTV 45677. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
Theorem | rhmsubcALTVlem3 45675* | Lemma 3 for rhmsubcALTV 45677. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
Theorem | rhmsubcALTVlem4 45676* | Lemma 4 for rhmsubcALTV 45677. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
Theorem | rhmsubcALTV 45677 | According to df-subc 17533, the subcategories (Subcat‘𝐶) of a category 𝐶 are subsets of the homomorphisms of 𝐶 (see subcssc 17564 and subcss2 17567). 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 45678 | 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 45679 | Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 5655. (Contributed by AV, 30-Mar-2019.) |
⊢ (〈𝐶, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eliunxp2 45680* | Membership in a union of Cartesian products over its second component, analogous to eliunxp 5749. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | mpomptx2 45681* | 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 7396. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | cbvmpox2 45682* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 7378 allows 𝐴 to be a function of 𝑦, analogous to cbvmpox 7377. (Contributed by AV, 30-Mar-2019.) |
⊢ Ⅎ𝑧𝐴 & ⊢ Ⅎ𝑦𝐷 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐷) & ⊢ ((𝑦 = 𝑧 ∧ 𝑥 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ 𝐷, 𝑧 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | dmmpossx2 45683* | 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 7915. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | ||
Theorem | mpoexxg2 45684* | 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 7925. (Contributed by AV, 30-Mar-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐵 𝐴 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | ovmpordxf 45685* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7432. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpordx 45686* | Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf 7432. (Contributed by AV, 30-Mar-2019.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐶 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐿) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpox2 45687* | The value of an operation class abstraction. Variant of ovmpoga 7436 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐿) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐿 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | fdmdifeqresdif 45688* | 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 45689* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | ofaddmndmap 45690 | 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 45691 | A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊) → 𝐹 ∈ (𝑅 ↑m {𝑋})) | ||
Theorem | fprmappr 45692 | 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 45693 | 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 45694 | A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.) |
⊢ ((𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ) → ((𝑍 · 𝐴) = 𝐵 → 𝐴 = 𝐵)) | ||
Theorem | 2t6m3t4e0 45695 | 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019.) |
⊢ ((2 · 6) − (3 · 4)) = 0 | ||
Theorem | ssnn0ssfz 45696* | For any finite subset of ℕ0, find a superset in the form of a set of sequential integers, analogous to ssnnssfz 31117. (Contributed by AV, 30-Sep-2019.) |
⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → ∃𝑛 ∈ ℕ0 𝐴 ⊆ (0...𝑛)) | ||
Theorem | nn0sumltlt 45697 | 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 45698 | 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 45699* | 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 45698) instead of the binomial theorem (binom 15551) , see altgsumbcALT 45700. (Contributed by AV, 13-Sep-2019.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) | ||
Theorem | altgsumbcALT 45700* | Alternate proof of altgsumbc 45699, using Pascal's rule (bcpascm1 45698) instead of the binomial theorem (binom 15551). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |