![]() |
Metamath
Proof Explorer Theorem List (p. 481 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xpiun 48001* | A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.) |
⊢ (𝐵 × 𝐶) = ∪ 𝑥 ∈ 𝐵 {〈𝑎, 𝑏〉 ∣ (𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶)} | ||
Theorem | ovn0ssdmfun 48002* | If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6949. (Contributed by AV, 27-Jan-2020.) |
⊢ (∀𝑎 ∈ 𝐷 ∀𝑏 ∈ 𝐸 (𝑎𝐹𝑏) ≠ ∅ → ((𝐷 × 𝐸) ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ (𝐷 × 𝐸)))) | ||
Theorem | fnxpdmdm 48003 | The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.) |
⊢ (𝐹 Fn (𝐴 × 𝐴) → dom dom 𝐹 = 𝐴) | ||
Theorem | cnfldsrngbas 48004 | The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝑅 = (ℂfld ↾s 𝑆) ⇒ ⊢ (𝑆 ⊆ ℂ → 𝑆 = (Base‘𝑅)) | ||
Theorem | cnfldsrngadd 48005 | The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝑅 = (ℂfld ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ 𝑉 → + = (+g‘𝑅)) | ||
Theorem | cnfldsrngmul 48006 | The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝑅 = (ℂfld ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ 𝑉 → · = (.r‘𝑅)) | ||
Theorem | plusfreseq 48007 | If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ⨣ = (+𝑓‘𝑀) ⇒ ⊢ (∅ ∉ ran ⨣ → ( + ↾ (𝐵 × 𝐵)) = ⨣ ) | ||
Theorem | mgmplusfreseq 48008 | If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ⨣ = (+𝑓‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵) → ( + ↾ (𝐵 × 𝐵)) = ⨣ ) | ||
Theorem | 0mgm 48009 | A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.) |
⊢ (Base‘𝑀) = ∅ ⇒ ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm) | ||
Theorem | opmpoismgm 48010* | A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mgm) | ||
Theorem | copissgrp 48011* | A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑀 ∈ Smgrp) | ||
Theorem | copisnmnd 48012* | A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 1 < (♯‘𝐵)) ⇒ ⊢ (𝜑 → 𝑀 ∉ Mnd) | ||
Theorem | 0nodd 48013* | 0 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} ⇒ ⊢ 0 ∉ 𝑂 | ||
Theorem | 1odd 48014* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} ⇒ ⊢ 1 ∈ 𝑂 | ||
Theorem | 2nodd 48015* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} ⇒ ⊢ 2 ∉ 𝑂 | ||
Theorem | oddibas 48016* | Lemma 1 for oddinmgm 48018: 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 48017* | Lemma 2 for oddinmgm 48018: 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 48018* | 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 48093, and even a non-unital ring, see 2zrng 48084. (Contributed by AV, 3-Feb-2020.) |
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)} & ⊢ 𝑀 = (ℂfld ↾s 𝑂) ⇒ ⊢ 𝑀 ∉ Mgm | ||
Theorem | nnsgrpmgm 48019 | 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 48020 | The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝑀 = (ℂfld ↾s ℕ) ⇒ ⊢ 𝑀 ∈ Smgrp | ||
Theorem | nnsgrpnmnd 48021 | 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 | ||
Theorem | nn0mnd 48022 | The set of nonnegative integers under (complex) addition is a monoid. Example in [Lang] p. 6. Remark: 𝑀 could have also been written as (ℂfld ↾s ℕ0). (Contributed by AV, 27-Dec-2023.) |
⊢ 𝑀 = {〈(Base‘ndx), ℕ0〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ 𝑀 ∈ Mnd | ||
Theorem | gsumsplit2f 48023* | 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 48024* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
⊢ Ⅎ𝑘𝑌 & ⊢ Ⅎ𝑘𝜑 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumfsupp 48025 | A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in [Lang] p. 5, last two formulas. (Contributed by AV, 27-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (𝐹 supp 0 ) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐼)) = (𝐺 Σg 𝐹)) | ||
With df-mpo 7435, binary operations are defined by a rule, and with df-ov 7433, 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 7433 (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 48042. If, in addition, the result is also contained in the set 𝑆, the operation is called closed internal binary operation, see df-clintop 48043. 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 48043 ). 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 48043 and df-assintop 48044), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey 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 alternate definition df-cllaw 48029 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 48037, or for an alternate definition df-mgm2 48062 for a magma as extensible structure. Similar results are obtained for an associative operation (defining 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 48026 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 48027 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 48028 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 48029* | 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 48030* | 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 48031* | 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 48032* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀)) | ||
Theorem | iscomlaw 48033* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥))) | ||
Theorem | clcllaw 48034 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
⊢ (( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀) → (𝑋 ⚬ 𝑌) ∈ 𝑀) | ||
Theorem | isasslaw 48035* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ assLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
Theorem | asslawass 48036* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
⊢ ( ⚬ assLaw 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) | ||
Theorem | mgmplusgiopALT 48037 | 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 48038 | 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.) |
⊢ (𝐺 ∈ Smgrp → (+g‘𝐺) assLaw (Base‘𝐺)) | ||
In this subsection, "internal binary operations" obeying different laws are defined. | ||
Syntax | cintop 48039 | Extend class notation with class of internal (binary) operations for a set. |
class intOp | ||
Syntax | cclintop 48040 | Extend class notation with class of closed operations for a set. |
class clIntOp | ||
Syntax | cassintop 48041 | Extend class notation with class of associative operations for a set. |
class assIntOp | ||
Definition | df-intop 48042* | Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.) |
⊢ intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚))) | ||
Definition | df-clintop 48043 | 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 48044* | 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 48045 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑m (𝑀 × 𝑀))) | ||
Theorem | intop 48046 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁) | ||
Theorem | clintopval 48047 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑m (𝑀 × 𝑀))) | ||
Theorem | assintopval 48048* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀}) | ||
Theorem | assintopmap 48049* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑m (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀}) | ||
Theorem | isclintop 48050 | 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 48051 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀) | ||
Theorem | assintop 48052 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀)) | ||
Theorem | isassintop 48053* | 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 48054 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀) | ||
Theorem | assintopcllaw 48055 | 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 48056 | 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 48057* | 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 48058 | Extend class notation with class of all magmas. |
class MgmALT | ||
Syntax | ccmgm2 48059 | Extend class notation with class of all commutative magmas. |
class CMgmALT | ||
Syntax | csgrp2 48060 | Extend class notation with class of all semigroups. |
class SGrpALT | ||
Syntax | ccsgrp2 48061 | Extend class notation with class of all commutative semigroups. |
class CSGrpALT | ||
Definition | df-mgm2 48062 | 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 48063 | 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 48064 | 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 semigroup in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.) |
⊢ SGrpALT = {𝑔 ∈ MgmALT ∣ (+g‘𝑔) assLaw (Base‘𝑔)} | ||
Definition | df-csgrp2 48065 | A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.) |
⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)} | ||
Theorem | ismgmALT 48066 | 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 48067 | 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 48068 | 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 48069 | 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 48070 | Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.) |
⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm) | ||
Theorem | sgrp2sgrp 48071 | Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.) |
⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp) | ||
Theorem | lmod0rng 48072 | 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 48073 | 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 | lidldomn1 48074* | If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 )) | ||
Theorem | lidlabl 48075 | A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) | ||
Theorem | lidlrng 48076 | A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) (Proof shortened by AV, 11-Mar-2025.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) | ||
Theorem | zlidlring 48077 | The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring) | ||
Theorem | uzlidlring 48078 | Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿) → (𝐼 ∈ Ring ↔ (𝑈 = { 0 } ∨ 𝑈 = 𝐵))) | ||
Theorem | lidldomnnring 48079 | A (left) ideal of a domain which is neither the zero ideal nor the unit ideal is not a unital ring. (Contributed by AV, 18-Feb-2020.) |
⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ∧ 𝑈 ≠ 𝐵)) → 𝐼 ∉ Ring) | ||
Theorem | 0even 48080* | 0 is an even integer. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 0 ∈ 𝐸 | ||
Theorem | 1neven 48081* | 1 is not an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 1 ∉ 𝐸 | ||
Theorem | 2even 48082* | 2 is an even integer. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 2 ∈ 𝐸 | ||
Theorem | 2zlidl 48083* | The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) ⇒ ⊢ 𝐸 ∈ 𝑈 | ||
Theorem | 2zrng 48084* | The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm 48018. (Contributed by AV, 20-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) & ⊢ 𝑅 = (ℤring ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngbas 48085* | The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝐸 = (Base‘𝑅) | ||
Theorem | 2zrngadd 48086* | The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ + = (+g‘𝑅) | ||
Theorem | 2zrng0 48087* | The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 0 = (0g‘𝑅) | ||
Theorem | 2zrngamgm 48088* | R is an (additive) magma. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mgm | ||
Theorem | 2zrngasgrp 48089* | R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Smgrp | ||
Theorem | 2zrngamnd 48090* | R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mnd | ||
Theorem | 2zrngacmnd 48091* | R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ CMnd | ||
Theorem | 2zrngagrp 48092* | R is an (additive) group. (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Grp | ||
Theorem | 2zrngaabl 48093* | R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Abel | ||
Theorem | 2zrngmul 48094* | The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ · = (.r‘𝑅) | ||
Theorem | 2zrngmmgm 48095* | R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Mgm | ||
Theorem | 2zrngmsgrp 48096* | R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Smgrp | ||
Theorem | 2zrngALT 48097* | The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng 48084, based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl 48093) and a multiplicative semigroup (see 2zrngmsgrp 48096). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | 2zrngnmlid 48098* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
Theorem | 2zrngnmrid 48099* | R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 | ||
Theorem | 2zrngnmlid2 48100* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |