Home | Metamath
Proof Explorer Theorem List (p. 417 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1odd 41601* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} ⇒ ⊢ 1 ∈ 𝑂 | ||
Theorem | 2nodd 41602* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} ⇒ ⊢ 2 ∉ 𝑂 | ||
Theorem | oddibas 41603* | Lemma 1 for oddinmgm 41605: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} & ⊢ 𝑀 = (ℂfld ↾s 𝑂) ⇒ ⊢ 𝑂 = (Base‘𝑀) | ||
Theorem | oddiadd 41604* | Lemma 2 for oddinmgm 41605: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} & ⊢ 𝑀 = (ℂfld ↾s 𝑂) ⇒ ⊢ + = (+g‘𝑀) | ||
Theorem | oddinmgm 41605* | The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 41734, and even a non-unital ring, see 2zrng 41725. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} & ⊢ 𝑀 = (ℂfld ↾s 𝑂) ⇒ ⊢ 𝑀 ∉ Mgm | ||
Theorem | nnsgrpmgm 41606 | The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝑀 = (ℂfld ↾s ℕ) ⇒ ⊢ 𝑀 ∈ Mgm | ||
Theorem | nnsgrp 41607 | The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝑀 = (ℂfld ↾s ℕ) ⇒ ⊢ 𝑀 ∈ SGrp | ||
Theorem | nnsgrpnmnd 41608 | The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝑀 = (ℂfld ↾s ℕ) ⇒ ⊢ 𝑀 ∉ Mnd | ||
With df-mpt2 6554, binary operations are defined by a rule, and with df-ov 6552, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation (19-Jan-2020), "... a binary operation on a set 𝑆 is a mapping of the elements of the Cartesian product 𝑆 × 𝑆 to S: 𝑓:(𝑆 × 𝑆⟶𝑆). Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, we call binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 internal binary operations, see df-intop 41625. If, in addition, the result is also contained in the set 𝑆, the operation is called closed internal binary operation, see df-clintop 41626. Therefore, a "binary operation on a set 𝑆" according to Wikipedia is a "closed internal binary operation" in our terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 41626 and df-assintop 41627), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obeys these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternative definition df-cllaw 41612 for an internal binary operation is provided, which does not require to be a function, but only closure. Therefore, this definition could be used as binary operation (slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 41620, or for an alternative definition df-mgm2 41645 for a magma as extensible structure. Similar results are obtained for an associative operation resp. semigroups. | ||
In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi. | ||
Syntax | ccllaw 41609 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 41610 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 41611 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 41612* | The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.) |
⊢ clLaw = {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚} | ||
Definition | df-comlaw 41613* | The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.) |
⊢ comLaw = {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)} | ||
Definition | df-asslaw 41614* | The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
⊢ assLaw = {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} | ||
Theorem | iscllaw 41615* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀)) | ||
Theorem | iscomlaw 41616* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥))) | ||
Theorem | clcllaw 41617 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
⊢ (( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀) → (𝑋 ⚬ 𝑌) ∈ 𝑀) | ||
Theorem | isasslaw 41618* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ assLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
Theorem | asslawass 41619* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
⊢ ( ⚬ assLaw 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) | ||
Theorem | mgmplusgiopALT 41620 | Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑀 ∈ Mgm → (+g‘𝑀) clLaw (Base‘𝑀)) | ||
Theorem | sgrpplusgaopALT 41621 | Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ SGrp → (+g‘𝐺) assLaw (Base‘𝐺)) | ||
In this subsection, "internal binary operations" obeying different laws are defined. | ||
Syntax | cintop 41622 | Extend class notation with class of internal (binary) operations for a set. |
class intOp | ||
Syntax | cclintop 41623 | Extend class notation with class of closed operations for a set. |
class clIntOp | ||
Syntax | cassintop 41624 | Extend class notation with class of associative operations for a set. |
class assIntOp | ||
Definition | df-intop 41625* | Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.) |
⊢ intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑𝑚 (𝑚 × 𝑚))) | ||
Definition | df-clintop 41626 | Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.) |
⊢ clIntOp = (𝑚 ∈ V ↦ (𝑚 intOp 𝑚)) | ||
Definition | df-assintop 41627* | Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.) |
⊢ assIntOp = (𝑚 ∈ V ↦ {𝑜 ∈ ( clIntOp ‘𝑚) ∣ 𝑜 assLaw 𝑚}) | ||
Theorem | intopval 41628 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑𝑚 (𝑀 × 𝑀))) | ||
Theorem | intop 41629 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁) | ||
Theorem | clintopval 41630 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑𝑚 (𝑀 × 𝑀))) | ||
Theorem | assintopval 41631* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀}) | ||
Theorem | assintopmap 41632* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑𝑚 (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀}) | ||
Theorem | isclintop 41633 | The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘𝑀) ↔ ⚬ :(𝑀 × 𝑀)⟶𝑀)) | ||
Theorem | clintop 41634 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀) | ||
Theorem | assintop 41635 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀)) | ||
Theorem | isassintop 41636* | The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘𝑀) ↔ ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
Theorem | clintopcllaw 41637 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀) | ||
Theorem | assintopcllaw 41638 | The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ⚬ clLaw 𝑀) | ||
Theorem | assintopasslaw 41639 | The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ⚬ assLaw 𝑀) | ||
Theorem | assintopass 41640* | An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) | ||
Syntax | cmgm2 41641 | Extend class notation with class of all magmas. |
class MgmALT | ||
Syntax | ccmgm2 41642 | Extend class notation with class of all commutative magmas. |
class CMgmALT | ||
Syntax | csgrp2 41643 | Extend class notation with class of all semigroups. |
class SGrpALT | ||
Syntax | ccsgrp2 41644 | Extend class notation with class of all commutative semigroups. |
class CSGrpALT | ||
Definition | df-mgm2 41645 | A magma is a set equipped with a closed operation. Definition 1 of [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by AV, 6-Jan-2020.) |
⊢ MgmALT = {𝑚 ∣ (+g‘𝑚) clLaw (Base‘𝑚)} | ||
Definition | df-cmgm2 41646 | A commutative magma is a magma with a commutative operation. Definition 8 of [BourbakiAlg1] p. 7. (Contributed by AV, 20-Jan-2020.) |
⊢ CMgmALT = {𝑚 ∈ MgmALT ∣ (+g‘𝑚) comLaw (Base‘𝑚)} | ||
Definition | df-sgrp2 41647 | A semigroup is a magma with an associative operation. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4, or of a semi-group in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.) |
⊢ SGrpALT = {𝑔 ∈ MgmALT ∣ (+g‘𝑔) assLaw (Base‘𝑔)} | ||
Definition | df-csgrp2 41648 | A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.) |
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)} | ||
Theorem | ismgmALT 41649 | The predicate "is a magma." (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ MgmALT ↔ ⚬ clLaw 𝐵)) | ||
Theorem | iscmgmALT 41650 | The predicate "is a commutative magma." (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ CMgmALT ↔ (𝑀 ∈ MgmALT ∧ ⚬ comLaw 𝐵)) | ||
Theorem | issgrpALT 41651 | The predicate "is a semigroup." (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ SGrpALT ↔ (𝑀 ∈ MgmALT ∧ ⚬ assLaw 𝐵)) | ||
Theorem | iscsgrpALT 41652 | The predicate "is a commutative semigroup." (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ CSGrpALT ↔ (𝑀 ∈ SGrpALT ∧ ⚬ comLaw 𝐵)) | ||
Theorem | mgm2mgm 41653 | Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.) |
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm) | ||
Theorem | sgrp2sgrp 41654 | Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.) |
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ SGrp) | ||
Theorem | idfusubc0 41655* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = 〈( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥(Hom ‘𝑆)𝑦)))〉) | ||
Theorem | idfusubc 41656* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐼 = (idfunc‘𝑆) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐽 ∈ (Subcat‘𝐶) → 𝐼 = 〈( I ↾ 𝐵), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦)))〉) | ||
Theorem | inclfusubc 41657* | The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.) |
⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) & ⊢ 𝑆 = (𝐶 ↾cat 𝐽) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 = ( I ↾ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥𝐽𝑦)))) ⇒ ⊢ (𝜑 → 𝐹(𝑆 Func 𝐶)𝐺) | ||
Theorem | lmod0rng 41658 | If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019.) |
⊢ ((𝑀 ∈ LMod ∧ ¬ (Scalar‘𝑀) ∈ NzRing) → (Base‘𝑀) = {(0g‘𝑀)}) | ||
Theorem | nzrneg1ne0 41659 | The additive inverse of the 1 in a nonzero ring is not zero ( -1 =/= 0 ). (Contributed by AV, 29-Apr-2019.) |
⊢ (𝑅 ∈ NzRing → ((invg‘𝑅)‘(1r‘𝑅)) ≠ (0g‘𝑅)) | ||
Theorem | 0ringdif 41660 | A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ (Ring ∖ NzRing) ↔ (𝑅 ∈ Ring ∧ 𝐵 = { 0 })) | ||
Theorem | 0ringbas 41661 | The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 𝐵 = { 0 }) | ||
Theorem | 0ring1eq0 41662 | In a zero ring, a ring which is not a nonzero ring, the unit equals the zero element. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ (Ring ∖ NzRing) → 1 = 0 ) | ||
Theorem | nrhmzr 41663 | There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ((𝑍 ∈ (Ring ∖ NzRing) ∧ 𝑅 ∈ NzRing) → (𝑍 RingHom 𝑅) = ∅) | ||
According to Wikipedia, "... in abstract algebra, a rng (or pseudo-ring or non-unital ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 6-Jan-2020). | ||
Syntax | crng 41664 | Extend class notation with class of all non-unital rings. |
class Rng | ||
Definition | df-rng0 41665* | Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.) |
⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ SGrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} | ||
Theorem | isrng 41666* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ SGrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) | ||
Theorem | rngabl 41667 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) | ||
Theorem | rngmgp 41668 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝐺 ∈ SGrp) | ||
Theorem | ringrng 41669 | A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Rng) | ||
Theorem | ringssrng 41670 | The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.) |
⊢ Ring ⊆ Rng | ||
Theorem | isringrng 41671* | The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Rng ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 𝑦 ∧ (𝑦 · 𝑥) = 𝑦))) | ||
Theorem | rngdir 41672 | Distributive law for the multiplication operation of a nonunital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
Theorem | rngcl 41673 | Closure of the multiplication operation of a nonunital ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | rnglz 41674 | The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
Syntax | crngh 41675 | non-unital ring homomorphisms. |
class RngHomo | ||
Syntax | crngs 41676 | non-unital ring isomorphisms. |
class RngIsom | ||
Definition | df-rnghomo 41677* | Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
⊢ RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}) | ||
Definition | df-rngisom 41678* | Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.) |
⊢ RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ ◡𝑓 ∈ (𝑠 RngHomo 𝑟)}) | ||
Theorem | rnghmrcl 41679 | Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝑅 ∈ Rng ∧ 𝑆 ∈ Rng)) | ||
Theorem | rnghmfn 41680 | The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.) |
⊢ RngHomo Fn (Rng × Rng) | ||
Theorem | rnghmval 41681* | The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∗ = (.r‘𝑆) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑆) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = {𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ✚ (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) ∗ (𝑓‘𝑦)))}) | ||
Theorem | isrnghm 41682* | A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∗ = (.r‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))))) | ||
Theorem | isrnghmmul 41683 | A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) ↔ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ (𝑀 MgmHom 𝑁)))) | ||
Theorem | rnghmmgmhm 41684 | A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑀 MgmHom 𝑁)) | ||
Theorem | rnghmval2 41685 | The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020.) |
⊢ ((𝑅 ∈ Rng ∧ 𝑆 ∈ Rng) → (𝑅 RngHomo 𝑆) = ((𝑅 GrpHom 𝑆) ∩ ((mulGrp‘𝑅) MgmHom (mulGrp‘𝑆)))) | ||
Theorem | isrngisom 41686 | An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ ◡𝐹 ∈ (𝑆 RngHomo 𝑅)))) | ||
Theorem | rngimrcl 41687 | Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → (𝑅 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | rnghmghm 41688 | A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | rnghmf 41689 | A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → 𝐹:𝐵⟶𝐶) | ||
Theorem | rnghmmul 41690 | A homomorphism of non-unital rings preserves multiplication. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) × (𝐹‘𝐵))) | ||
Theorem | isrnghm2d 41691* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | isrnghmd 41692* | Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) & ⊢ 𝐶 = (Base‘𝑆) & ⊢ + = (+g‘𝑅) & ⊢ ⨣ = (+g‘𝑆) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmf1o 41693 | A non-unital ring homomorphism is bijective iff its converse is also a non-unital ring homomorphism. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngHomo 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 RngHomo 𝑅))) | ||
Theorem | isrngim 41694 | An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RngIsom 𝑆) ↔ (𝐹 ∈ (𝑅 RngHomo 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))) | ||
Theorem | rngimf1o 41695 | An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | rngimrnghm 41696 | An isomorphism of non-unital rings is a homomorphism. (Contributed by AV, 23-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 RngIsom 𝑆) → 𝐹 ∈ (𝑅 RngHomo 𝑆)) | ||
Theorem | rnghmco 41697 | The composition of non-unital ring homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
⊢ ((𝐹 ∈ (𝑇 RngHomo 𝑈) ∧ 𝐺 ∈ (𝑆 RngHomo 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 RngHomo 𝑈)) | ||
Theorem | idrnghm 41698 | The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → ( I ↾ 𝐵) ∈ (𝑅 RngHomo 𝑅)) | ||
Theorem | c0mgm 41699* | The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MgmHom 𝑇)) | ||
Theorem | c0mhm 41700* | The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) ⇒ ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MndHom 𝑇)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |