| Metamath
Proof Explorer Theorem List (p. 482 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | ccomlaw 48101 | Extend class notation for the commutative law. |
| class comLaw | ||
| Definition | df-cllaw 48102* | 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 48103* | 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 48104* | 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 48105* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
| ⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀)) | ||
| Theorem | iscomlaw 48106* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
| ⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥))) | ||
| Theorem | clcllaw 48107 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
| ⊢ (( ⚬ clLaw 𝑀 ∧ 𝑋 ∈ 𝑀 ∧ 𝑌 ∈ 𝑀) → (𝑋 ⚬ 𝑌) ∈ 𝑀) | ||
| Theorem | isasslaw 48108* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
| ⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ assLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
| Theorem | asslawass 48109* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
| ⊢ ( ⚬ assLaw 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))) | ||
| Theorem | mgmplusgiopALT 48110 | 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 48111 | 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 48112 | Extend class notation with class of internal (binary) operations for a set. |
| class intOp | ||
| Syntax | cclintop 48113 | Extend class notation with class of closed operations for a set. |
| class clIntOp | ||
| Syntax | cassintop 48114 | Extend class notation with class of associative operations for a set. |
| class assIntOp | ||
| Definition | df-intop 48115* | 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 48116 | 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 48117* | 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 48118 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 intOp 𝑁) = (𝑁 ↑m (𝑀 × 𝑀))) | ||
| Theorem | intop 48119 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ ( ⚬ ∈ (𝑀 intOp 𝑁) → ⚬ :(𝑀 × 𝑀)⟶𝑁) | ||
| Theorem | clintopval 48120 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ (𝑀 ∈ 𝑉 → ( clIntOp ‘𝑀) = (𝑀 ↑m (𝑀 × 𝑀))) | ||
| Theorem | assintopval 48121* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ ( clIntOp ‘𝑀) ∣ 𝑜 assLaw 𝑀}) | ||
| Theorem | assintopmap 48122* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
| ⊢ (𝑀 ∈ 𝑉 → ( assIntOp ‘𝑀) = {𝑜 ∈ (𝑀 ↑m (𝑀 × 𝑀)) ∣ 𝑜 assLaw 𝑀}) | ||
| Theorem | isclintop 48123 | 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 48124 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ :(𝑀 × 𝑀)⟶𝑀) | ||
| Theorem | assintop 48125 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ ( ⚬ ∈ ( assIntOp ‘𝑀) → ( ⚬ :(𝑀 × 𝑀)⟶𝑀 ∧ ⚬ assLaw 𝑀)) | ||
| Theorem | isassintop 48126* | 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 48127 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
| ⊢ ( ⚬ ∈ ( clIntOp ‘𝑀) → ⚬ clLaw 𝑀) | ||
| Theorem | assintopcllaw 48128 | 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 48129 | 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 48130* | 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 48131 | Extend class notation with class of all magmas. |
| class MgmALT | ||
| Syntax | ccmgm2 48132 | Extend class notation with class of all commutative magmas. |
| class CMgmALT | ||
| Syntax | csgrp2 48133 | Extend class notation with class of all semigroups. |
| class SGrpALT | ||
| Syntax | ccsgrp2 48134 | Extend class notation with class of all commutative semigroups. |
| class CSGrpALT | ||
| Definition | df-mgm2 48135 | 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 48136 | 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 48137 | 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 48138 | A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.) |
| ⊢ CSGrpALT = {𝑔 ∈ SGrpALT ∣ (+g‘𝑔) comLaw (Base‘𝑔)} | ||
| Theorem | ismgmALT 48139 | 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 48140 | 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 48141 | 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 48142 | 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 48143 | Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.) |
| ⊢ (𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm) | ||
| Theorem | sgrp2sgrp 48144 | Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.) |
| ⊢ (𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp) | ||
| Theorem | lmod0rng 48145 | 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 48146 | 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 48147* | 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 48148 | A (left) ideal of a ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
| ⊢ 𝐿 = (LIdeal‘𝑅) & ⊢ 𝐼 = (𝑅 ↾s 𝑈) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Abel) | ||
| Theorem | lidlrng 48149 | 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 48150 | 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 48151 | 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 48152 | 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 48153* | 0 is an even integer. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 0 ∈ 𝐸 | ||
| Theorem | 1neven 48154* | 1 is not an even integer. (Contributed by AV, 12-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 1 ∉ 𝐸 | ||
| Theorem | 2even 48155* | 2 is an even integer. (Contributed by AV, 12-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} ⇒ ⊢ 2 ∈ 𝐸 | ||
| Theorem | 2zlidl 48156* | The even integers are a (left) ideal of the ring of integers. (Contributed by AV, 20-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) ⇒ ⊢ 𝐸 ∈ 𝑈 | ||
| Theorem | 2zrng 48157* | 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 48091. (Contributed by AV, 20-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑈 = (LIdeal‘ℤring) & ⊢ 𝑅 = (ℤring ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Rng | ||
| Theorem | 2zrngbas 48158* | The base set of R is the set of all even integers. (Contributed by AV, 31-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝐸 = (Base‘𝑅) | ||
| Theorem | 2zrngadd 48159* | The group addition operation of R is the addition of complex numbers. (Contributed by AV, 31-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ + = (+g‘𝑅) | ||
| Theorem | 2zrng0 48160* | The additive identity of R is the complex number 0. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 0 = (0g‘𝑅) | ||
| Theorem | 2zrngamgm 48161* | R is an (additive) magma. (Contributed by AV, 6-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mgm | ||
| Theorem | 2zrngasgrp 48162* | R is an (additive) semigroup. (Contributed by AV, 4-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Smgrp | ||
| Theorem | 2zrngamnd 48163* | R is an (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Mnd | ||
| Theorem | 2zrngacmnd 48164* | R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ CMnd | ||
| Theorem | 2zrngagrp 48165* | R is an (additive) group. (Contributed by AV, 6-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Grp | ||
| Theorem | 2zrngaabl 48166* | R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ 𝑅 ∈ Abel | ||
| Theorem | 2zrngmul 48167* | The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) ⇒ ⊢ · = (.r‘𝑅) | ||
| Theorem | 2zrngmmgm 48168* | R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Mgm | ||
| Theorem | 2zrngmsgrp 48169* | R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑀 ∈ Smgrp | ||
| Theorem | 2zrngALT 48170* | The ring of integers restricted to the even integers is a non-unital ring, the "ring of even integers". Alternate version of 2zrng 48157, 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 48166) and a multiplicative semigroup (see 2zrngmsgrp 48169). (Contributed by AV, 11-Feb-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∈ Rng | ||
| Theorem | 2zrngnmlid 48171* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑏 ∈ 𝐸 ∃𝑎 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
| Theorem | 2zrngnmrid 48172* | R has no multiplicative (right) identity. (Contributed by AV, 12-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ≠ 𝑎 | ||
| Theorem | 2zrngnmlid2 48173* | R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ∀𝑎 ∈ (𝐸 ∖ {0})∀𝑏 ∈ 𝐸 (𝑏 · 𝑎) ≠ 𝑎 | ||
| Theorem | 2zrngnring 48174* | R is not a unital ring. (Contributed by AV, 6-Jan-2020.) |
| ⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} & ⊢ 𝑅 = (ℂfld ↾s 𝐸) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ 𝑅 ∉ Ring | ||
| Theorem | cznrnglem 48175 | Lemma for cznrng 48177: The base set of the ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the ℤ/nℤ structure. (Contributed by AV, 16-Feb-2020.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) ⇒ ⊢ 𝐵 = (Base‘𝑋) | ||
| Theorem | cznabel 48176 | The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (Contributed by AV, 16-Feb-2020.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Abel) | ||
| Theorem | cznrng 48177* | The ring constructed from a ℤ/nℤ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng) | ||
| Theorem | cznnring 48178* | The ring constructed from a ℤ/nℤ structure with 1 < 𝑛 by replacing the (multiplicative) ring operation by a constant operation is not a unital ring. (Contributed by AV, 17-Feb-2020.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑋 = (𝑌 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)〉) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐶 ∈ 𝐵) → 𝑋 ∉ Ring) | ||
As an alternative to df-rngc 20617, the "category of non-unital rings" can be defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, according to dfrngc2 20628. | ||
| Syntax | crngcALTV 48179 | Extend class notation to include the category Rng. (New usage is discouraged.) |
| class RngCatALTV | ||
| Definition | df-rngcALTV 48180* | Definition of the category Rng, relativized to a subset 𝑢. This is the category of all non-unital rings in 𝑢 and homomorphisms between these rings. Generally, we will take 𝑢 to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ RngCatALTV = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Rng) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 RngHom 𝑦))〉, 〈(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))〉}) | ||
| Theorem | rngcvalALTV 48181* | Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦))) & ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) ⇒ ⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), · 〉}) | ||
| Theorem | rngcbasALTV 48182 | Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng)) | ||
| Theorem | rngchomfvalALTV 48183* | Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦))) | ||
| Theorem | rngchomALTV 48184 | Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋 RngHom 𝑌)) | ||
| Theorem | elrngchomALTV 48185 | A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) | ||
| Theorem | rngccofvalALTV 48186* | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) RngHom 𝑧), 𝑓 ∈ ((1st ‘𝑣) RngHom (2nd ‘𝑣)) ↦ (𝑔 ∘ 𝑓)))) | ||
| Theorem | rngccoALTV 48187 | Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 RngHom 𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌 RngHom 𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) | ||
| Theorem | rngccatidALTV 48188* | Lemma for rngccatALTV 48189. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ ( I ↾ (Base‘𝑥))))) | ||
| Theorem | rngccatALTV 48189 | The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) | ||
| Theorem | rngcidALTV 48190 | The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑆 = (Base‘𝑋) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = ( I ↾ 𝑆)) | ||
| Theorem | rngcsectALTV 48191 | A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐸 = (Base‘𝑋) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑆𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngHom 𝑌) ∧ 𝐺 ∈ (𝑌 RngHom 𝑋) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐸)))) | ||
| Theorem | rngcinvALTV 48192 | An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑁 = (Inv‘𝐶) ⇒ ⊢ (𝜑 → (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹 ∈ (𝑋 RngIso 𝑌) ∧ 𝐺 = ◡𝐹))) | ||
| Theorem | rngcisoALTV 48193 | An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RngIso 𝑌))) | ||
| Theorem | rngchomffvalALTV 48194* | The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐹 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 RngHom 𝑦))) | ||
| Theorem | rngchomrnghmresALTV 48195 | The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
| ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ 𝐵 = (Rng ∩ 𝑈) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐹 = (Homf ‘𝐶) ⇒ ⊢ (𝜑 → 𝐹 = ( RngHom ↾ (𝐵 × 𝐵))) | ||
| Theorem | rngcrescrhmALTV 48196 | 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 48197 | Lemma 1 for rhmsubcALTV 48201. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ (𝜑 → 𝐻 Fn (𝑅 × 𝑅)) | ||
| Theorem | rhmsubcALTVlem2 48198 | Lemma 2 for rhmsubcALTV 48201. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝐻𝑌) = (𝑋 RingHom 𝑌)) | ||
| Theorem | rhmsubcALTVlem3 48199* | Lemma 3 for rhmsubcALTV 48201. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑅) → ((Id‘(RngCatALTV‘𝑈))‘𝑥) ∈ (𝑥𝐻𝑥)) | ||
| Theorem | rhmsubcALTVlem4 48200* | Lemma 4 for rhmsubcALTV 48201. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RngCatALTV‘𝑈) & ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈)) & ⊢ 𝐻 = ( RingHom ↾ (𝑅 × 𝑅)) ⇒ ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑅) ∧ (𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(RngCatALTV‘𝑈))𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |