HomeTheorem List (p. 384 of 504)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 384 of 504) | < 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-31065) |
Hilbert Space Explorer
(31066-32588) |
Users' Mathboxes
(32589-50379) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-mgmOLD 38301* | Obsolete version of df-mgm 18655 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡} | ||
| Theorem | ismgmOLD 38302 | Obsolete version of ismgm 18656 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋)) | ||
| Theorem | clmgmOLD 38303 | Obsolete version of mgmcl 18658 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ ((𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | opidonOLD 38304 | Obsolete version of mndpfo 18772 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
| Theorem | rngopidOLD 38305 | Obsolete version of mndpfo 18772 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺) | ||
| Theorem | opidon2OLD 38306 | Obsolete version of mndpfo 18772 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
| Theorem | isexid2 38307* | If 𝐺 ∈ (Magma ∩ ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) | ||
| Theorem | exidu1 38308* | Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) | ||
| Theorem | idrval 38309* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝐴 → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) | ||
| Theorem | iorlid 38310 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝑈 ∈ 𝑋) | ||
| Theorem | cmpidelt 38311 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴)) | ||
| Syntax | csem 38312 | Extend class notation with the class of all semigroups. |
| class SemiGrp | ||
| Definition | df-sgrOLD 38313 | Obsolete version of df-sgrp 18734 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ SemiGrp = (Magma ∩ Ass) | ||
| Theorem | smgrpismgmOLD 38314 | Obsolete version of sgrpmgm 18739 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ SemiGrp → 𝐺 ∈ Magma) | ||
| Theorem | issmgrpOLD 38315* | Obsolete version of issgrp 18735 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ SemiGrp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))) | ||
| Theorem | smgrpmgm 38316 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | smgrpassOLD 38317* | Obsolete version of sgrpass 18740 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ SemiGrp → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) | ||
| Syntax | cmndo 38318 | Extend class notation with the class of all monoids. |
| class MndOp | ||
| Definition | df-mndo 38319 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ MndOp = (SemiGrp ∩ ExId ) | ||
| Theorem | mndoissmgrpOLD 38320 | Obsolete version of mndsgrp 18755 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp) | ||
| Theorem | mndoisexid 38321 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ ExId ) | ||
| Theorem | mndoismgmOLD 38322 | Obsolete version of mndmgm 18756 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ Magma) | ||
| Theorem | mndomgmid 38323 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId )) | ||
| Theorem | ismndo 38324* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺 ∈ SemiGrp ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | ismndo1 38325* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | ismndo2 38326* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))) | ||
| Theorem | grpomndo 38327 | A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ GrpOp → 𝐺 ∈ MndOp) | ||
| Theorem | exidcl 38328 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | exidreslem 38329* | Lemma for exidres 38330 and exidresid 38331. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) | ||
| Theorem | exidres 38330 | The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝐻 ∈ ExId ) | ||
| Theorem | exidresid 38331 | The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ (((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈) | ||
| Theorem | ablo4pnp 38332 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹))) | ||
| Theorem | grpoeqdivid 38333 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈)) | ||
| Theorem | grposnOLD 38334 | The group operation for the singleton group. Obsolete, use grp1 19070. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp | ||
| Syntax | cghomOLD 38335 | Obsolete version of cghm 19234 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
| class GrpOpHom | ||
| Definition | df-ghomOLD 38336* | Obsolete version of df-ghm 19235 as of 15-Mar-2020. Define the set of group homomorphisms from 𝑔 to ℎ. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
| ⊢ GrpOpHom = (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))}) | ||
| Theorem | elghomlem1OLD 38337* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38339. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆) | ||
| Theorem | elghomlem2OLD 38338* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 38339. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | ||
| Theorem | elghomOLD 38339* | Obsolete version of isghm 19237 as of 15-Mar-2020. Membership in the set of group homomorphisms from 𝐺 to 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = ran 𝐻 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:𝑋⟶𝑊 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | ||
| Theorem | ghomlinOLD 38340 | Obsolete version of ghmlin 19242 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴)𝐻(𝐹‘𝐵)) = (𝐹‘(𝐴𝐺𝐵))) | ||
| Theorem | ghomidOLD 38341 | Obsolete version of ghmid 19243 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑇 = (GId‘𝐻) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹‘𝑈) = 𝑇) | ||
| Theorem | ghomf 38342 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = ran 𝐻 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊) | ||
| Theorem | ghomco 38343 | The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) ∧ (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾))) → (𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾)) | ||
| Theorem | ghomdiv 38344 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝐶 = ( /𝑔 ‘𝐻) ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵))) | ||
| Theorem | grpokerinj 38345 | A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = (GId‘𝐺) & ⊢ 𝑌 = ran 𝐻 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑈}) = {𝑊})) | ||
| Syntax | crngo 38346 | Extend class notation with the class of all unital rings. |
| class RingOps | ||
| Definition | df-rngo 38347* | Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.) |
| ⊢ RingOps = {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))} | ||
| Theorem | relrngo 38348 | The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ Rel RingOps | ||
| Theorem | isrngo 38349* | The predicate "is a (unital) ring." Definition of "ring with unit" in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐻 ∈ 𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))) | ||
| Theorem | isrngod 38350* | Conditions that determine a ring. (Changed label from isringd 20318 to isrngod 38350-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐺 ∈ AbelOp) & ⊢ (𝜑 → 𝑋 = ran 𝐺) & ⊢ (𝜑 → 𝐻:(𝑋 × 𝑋)⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) & ⊢ (𝜑 → 𝑈 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐻𝑦) = 𝑦) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝑈) = 𝑦) ⇒ ⊢ (𝜑 → ⟨𝐺, 𝐻⟩ ∈ RingOps) | ||
| Theorem | rngoi 38351* | The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) | ||
| Theorem | rngosm 38352 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | rngocl 38353 | Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) ∈ 𝑋) | ||
| Theorem | rngoid 38354* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑢 ∈ 𝑋 ((𝑢𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑢) = 𝐴)) | ||
| Theorem | rngoideu 38355* | The unity element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | ||
| Theorem | rngodi 38356 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐺𝐶)) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻𝐶))) | ||
| Theorem | rngodir 38357 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(𝐵𝐻𝐶))) | ||
| Theorem | rngoass 38358 | Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = (𝐴𝐻(𝐵𝐻𝐶))) | ||
| Theorem | rngo2 38359* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝐺𝐴) = ((𝑥𝐺𝑥)𝐻𝐴)) | ||
| Theorem | rngoablo 38360 | A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ AbelOp) | ||
| Theorem | rngoablo2 38361 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ AbelOp) | ||
| Theorem | rngogrpo 38362 | A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) | ||
| Theorem | rngone0 38363 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅) | ||
| Theorem | rngogcl 38364 | Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | rngocom 38365 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | rngoaass 38366 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | rngoa32 38367 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
| Theorem | rngoa4 38368 | Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷))) | ||
| Theorem | rngorcan 38369 | Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rngolcan 38370 | Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rngo0cl 38371 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) | ||
| Theorem | rngo0rid 38372 | The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
| Theorem | rngo0lid 38373 | The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑍𝐺𝐴) = 𝐴) | ||
| Theorem | rngolz 38374 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑍𝐻𝐴) = 𝑍) | ||
| Theorem | rngorz 38375 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
| ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑍) = 𝑍) | ||
| Theorem | rngosn3 38376 | Obsolete as of 25-Jan-2020. Use ring1zr 20803 or srg1zr 20242 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩)) | ||
| Theorem | rngosn4 38377 | Obsolete as of 25-Jan-2020. Use rngen1zr 20804 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩)) | ||
| Theorem | rngosn6 38378 | Obsolete as of 25-Jan-2020. Use ringen1zr 20805 or srgen1zr 20243 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔ 𝑅 = ⟨{⟨⟨𝑍, 𝑍⟩, 𝑍⟩}, {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩)) | ||
| Theorem | rngonegcl 38379 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
| Theorem | rngoaddneg1 38380 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑍) | ||
| Theorem | rngoaddneg2 38381 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑍) | ||
| Theorem | rngosub 38382 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
| Theorem | rngmgmbs4 38383* | The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ ((𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) → ran 𝐺 = 𝑋) | ||
| Theorem | rngodm1dm2 38384 | In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻) | ||
| Theorem | rngorn1 38385 | In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐻) | ||
| Theorem | rngorn1eq 38386 | In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻) | ||
| Theorem | rngomndo 38387 | In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp) | ||
| Theorem | rngoidmlem 38388 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐻𝐴) = 𝐴 ∧ (𝐴𝐻𝑈) = 𝐴)) | ||
| Theorem | rngolidm 38389 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑈𝐻𝐴) = 𝐴) | ||
| Theorem | rngoridm 38390 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝐴𝐻𝑈) = 𝐴) | ||
| Theorem | rngo1cl 38391 | The unity element of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) | ||
| Theorem | rngoueqz 38392 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20559 instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔ 𝑈 = 𝑍)) | ||
| Theorem | rngonegmn1l 38393 | Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = ((𝑁‘𝑈)𝐻𝐴)) | ||
| Theorem | rngonegmn1r 38394 | Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐻(𝑁‘𝑈))) | ||
| Theorem | rngoneglmul 38395 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = ((𝑁‘𝐴)𝐻𝐵)) | ||
| Theorem | rngonegrmul 38396 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐻𝐵)) = (𝐴𝐻(𝑁‘𝐵))) | ||
| Theorem | rngosubdi 38397 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶))) | ||
| Theorem | rngosubdir 38398 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶))) | ||
| Theorem | zerdivemp1x 38399* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20328. (Contributed by Jeff Madsen, 18-Apr-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃𝑎 ∈ 𝑋 (𝑎𝐻𝐴) = 𝑈) → (𝐵 ∈ 𝑋 → ((𝐴𝐻𝐵) = 𝑍 → 𝐵 = 𝑍))) | ||
| Syntax | cdrng 38400 | Extend class notation with the class of all division rings. |
| class DivRingOps | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |