HomeTheorem List (p. 327 of 480)
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. 327 of 480) | < 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-30439) |
Hilbert Space Explorer
(30440-31962) |
Users' Mathboxes
(31963-47940) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xrnarchi 32601 | The completed real line is not Archimedean. (Contributed by Thierry Arnoux, 1-Feb-2018.) |
| β’ Β¬ β*π β Archi | ||
| Theorem | isarchi2 32602* | Alternative way to express the predicate "π is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ Β· = (.gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) β β’ ((π β Toset β§ π β Mnd) β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)))) | ||
| Theorem | submarchi 32603 | A submonoid is archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Archi) | ||
| Theorem | isarchi3 32604* | This is the usual definition of the Archimedean property for an ordered group. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) β β’ (π β oGrp β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) | ||
| Theorem | archirng 32605* | Property of Archimedean ordered groups, framing positive π between multiples of π. (Contributed by Thierry Arnoux, 12-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β 0 < π) β β’ (π β βπ β β0 ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) | ||
| Theorem | archirngz 32606* | Property of Archimedean left and right ordered groups. (Contributed by Thierry Arnoux, 6-May-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β (oppgβπ) β oGrp) β β’ (π β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) | ||
| Theorem | archiexdiv 32607* | In an Archimedean group, given two positive elements, there exists a "divisor" π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) β β’ (((π β oGrp β§ π β Archi) β§ (π β π΅ β§ π β π΅) β§ 0 < π) β βπ β β π < (π Β· π)) | ||
| Theorem | archiabllem1a 32608* | Lemma for archiabl 32615: In case an archimedean group π admits a smallest positive element π, then any positive element π of π can be written as (π Β· π) with π β β. Since the reciprocal holds for negative elements, π is then isomorphic to β€. (Contributed by Thierry Arnoux, 12-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) & β’ (π β π β π΅) & β’ (π β 0 < π) β β’ (π β βπ β β π = (π Β· π)) | ||
| Theorem | archiabllem1b 32609* | Lemma for archiabl 32615. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) β β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) | ||
| Theorem | archiabllem1 32610* | Archimedean ordered groups with a minimal positive value are abelian. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) β β’ (π β π β Abel) | ||
| Theorem | archiabllem2a 32611* | Lemma for archiabl 32615, which requires the group to be both left- and right-ordered. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β 0 < π) β β’ (π β βπ β π΅ ( 0 < π β§ (π + π) β€ π)) | ||
| Theorem | archiabllem2c 32612* | Lemma for archiabl 32615. (Contributed by Thierry Arnoux, 1-May-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β Β¬ (π + π) < (π + π)) | ||
| Theorem | archiabllem2b 32613* | Lemma for archiabl 32615. (Contributed by Thierry Arnoux, 1-May-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) = (π + π)) | ||
| Theorem | archiabllem2 32614* | Archimedean ordered groups with no minimal positive value are abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) β β’ (π β π β Abel) | ||
| Theorem | archiabl 32615 | Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
| β’ ((π β oGrp β§ (oppgβπ) β oGrp β§ π β Archi) β π β Abel) | ||
| Syntax | cslmd 32616 | Extend class notation with class of all semimodules. |
| class SLMod | ||
| Definition | df-slmd 32617* | Define the class of all (left) modules over semirings, i.e. semimodules, which are generalizations of left modules. A semimodule is a commutative monoid (=vectors) together with a semiring (=scalars) and a left scalar product connecting them. (0[,]+β) for example is not a full fledged left module, but is a semimodule. Definition of [Golan] p. 149. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ SLMod = {π β CMnd β£ [(Baseβπ) / π£][(+gβπ) / π][( Β·π βπ) / π ][(Scalarβπ) / π][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β SRing β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€ β§ ((0gβπ)π π€) = (0gβπ))))} | ||
| Theorem | isslmd 32618* | The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ π = (0gβπΉ) β β’ (π β SLMod β (π β CMnd β§ πΉ β SRing β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€ β§ (π Β· π€) = 0 )))) | ||
| Theorem | slmdlema 32619 | Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ π = (0gβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ) β§ (π β π β§ π β π)) β (((π Β· π) β π β§ (π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) β§ (((π Γ π ) Β· π) = (π Β· (π Β· π)) β§ ( 1 Β· π) = π β§ (π Β· π) = 0 ))) | ||
| Theorem | lmodslmd 32620 | Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ (π β LMod β π β SLMod) | ||
| Theorem | slmdcmn 32621 | A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ (π β SLMod β π β CMnd) | ||
| Theorem | slmdmnd 32622 | A semimodule is a monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ (π β SLMod β π β Mnd) | ||
| Theorem | slmdsrg 32623 | The scalar component of a semimodule is a semiring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) β β’ (π β SLMod β πΉ β SRing) | ||
| Theorem | slmdbn0 32624 | The base set of a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
| β’ π΅ = (Baseβπ) β β’ (π β SLMod β π΅ β β ) | ||
| Theorem | slmdacl 32625 | Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) | ||
| Theorem | slmdmcl 32626 | Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = (.rβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β πΎ) β (π Β· π) β πΎ) | ||
| Theorem | slmdsn0 32627 | The set of scalars in a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
| β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π β SLMod β π΅ β β ) | ||
| Theorem | slmdvacl 32628 | Closure of vector addition for a semiring left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β SLMod β§ π β π β§ π β π) β (π + π) β π) | ||
| Theorem | slmdass 32629 | Semiring left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β SLMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) | ||
| Theorem | slmdvscl 32630 | Closure of scalar product for a semiring left module. (hvmulcl 30534 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β π) β (π Β· π) β π) | ||
| Theorem | slmdvsdi 32631 | Distributive law for scalar product. (ax-hvdistr1 30529 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β π β§ π β π)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
| Theorem | slmdvsdir 32632 | Distributive law for scalar product. (ax-hvdistr1 30529 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) | ||
| Theorem | slmdvsass 32633 | Associative law for scalar product. (ax-hvmulass 30528 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ Γ = (.rβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π ) Β· π) = (π Β· (π Β· π))) | ||
| Theorem | slmd0cl 32634 | The ring zero in a semimodule belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) β β’ (π β SLMod β 0 β πΎ) | ||
| Theorem | slmd1cl 32635 | The ring unity in a semiring left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 1 = (1rβπΉ) β β’ (π β SLMod β 1 β πΎ) | ||
| Theorem | slmdvs1 32636 | Scalar product with ring unity. (ax-hvmulid 30527 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπΉ) β β’ ((π β SLMod β§ π β π) β ( 1 Β· π) = π) | ||
| Theorem | slmd0vcl 32637 | The zero vector is a vector. (ax-hv0cl 30524 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ (π β SLMod β 0 β π) | ||
| Theorem | slmd0vlid 32638 | Left identity law for the zero vector. (hvaddlid 30544 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β ( 0 + π) = π) | ||
| Theorem | slmd0vrid 32639 | Right identity law for the zero vector. (ax-hvaddid 30525 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β (π + 0 ) = π) | ||
| Theorem | slmd0vs 32640 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30531 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β π) β (π Β· π) = 0 ) | ||
| Theorem | slmdvs0 32641 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 30545 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπ) β β’ ((π β SLMod β§ π β πΎ) β (π Β· 0 ) = 0 ) | ||
| Theorem | gsumvsca1 32642* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) |
| β’ π΅ = (Baseβπ) & β’ πΊ = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ (π β πΎ β (BaseβπΊ)) & β’ (π β π΄ β Fin) & β’ (π β π β SLMod) & β’ (π β π β πΎ) & β’ ((π β§ π β π΄) β π β π΅) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) | ||
| Theorem | gsumvsca2 32643* | Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) (Proof shortened by AV, 12-Dec-2019.) |
| β’ π΅ = (Baseβπ) & β’ πΊ = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ (π β πΎ β (BaseβπΊ)) & β’ (π β π΄ β Fin) & β’ (π β π β SLMod) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β πΎ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = ((πΊ Ξ£g (π β π΄ β¦ π)) Β· π)) | ||
| Theorem | prmsimpcyc 32644 | A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023.) |
| β’ π΅ = (BaseβπΊ) β β’ ((β―βπ΅) β β β (πΊ β SimpGrp β πΊ β CycGrp)) | ||
| Theorem | idomdomd 32645 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ (π β π β IDomn) β β’ (π β π β Domn) | ||
| Theorem | idomringd 32646 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ (π β π β IDomn) β β’ (π β π β Ring) | ||
| Theorem | domnlcan 32647 | Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Domn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
| Theorem | idomrcan 32648 | Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β IDomn) & β’ (π β (π Β· π) = (π Β· π)) β β’ (π β π = π) | ||
| Theorem | urpropd 32649* | Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) & β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (π₯(.rβπ)π¦) = (π₯(.rβπ)π¦)) β β’ (π β (1rβπ) = (1rβπ)) | ||
| Theorem | 0ringsubrg 32650 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) & β’ (π β π β (SubRingβπ )) β β’ (π β (β―βπ) = 1) | ||
| Theorem | dvdschrmulg 32651 | In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016.) |
| β’ πΆ = (chrβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΆ β₯ π β§ π΄ β π΅) β (π Β· π΄) = 0 ) | ||
| Theorem | freshmansdream 32652 | For a prime number π, if π and π are members of a commutative ring π of characteristic π, then ((π + π)βπ) = ((πβπ) + (πβπ)). This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.gβ(mulGrpβπ )) & β’ π = (chrβπ ) & β’ (π β π β CRing) & β’ (π β π β β) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π + π)) = ((π β π) + (π β π))) | ||
| Theorem | frobrhm 32653* | In a commutative ring with prime characteristic, the Frobenius function πΉ is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.) |
| β’ π΅ = (Baseβπ ) & β’ π = (chrβπ ) & β’ β = (.gβ(mulGrpβπ )) & β’ πΉ = (π₯ β π΅ β¦ (π β π₯)) & β’ (π β π β CRing) & β’ (π β π β β) β β’ (π β πΉ β (π RingHom π )) | ||
| Theorem | ress1r 32654 | 1r is unaffected by restriction. This is a bit more generic than subrg1 20473. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 1 β π΄ β§ π΄ β π΅) β 1 = (1rβπ)) | ||
| Theorem | ringinvval 32655* | The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| β’ π΅ = (Baseβπ ) & β’ β = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = (Unitβπ ) β β’ ((π β Ring β§ π β π) β (πβπ) = (β©π¦ β π (π¦ β π) = 1 )) | ||
| Theorem | dvrcan5 32656 | Cancellation law for common factor in ratio. (divcan5 11921 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
| β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) / (π Β· π)) = (π / π)) | ||
| Theorem | subrgchr 32657 | If π΄ is a subring of π , then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
| β’ (π΄ β (SubRingβπ ) β (chrβ(π βΎs π΄)) = (chrβπ )) | ||
| Theorem | rmfsupp2 32658* | A mapping of a multiplication of a constant with a function into a ring is finitely supported if the function is finitely supported. (Contributed by Thierry Arnoux, 3-Jun-2023.) |
| β’ π = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ ((π β§ π£ β π) β πΆ β π ) & β’ (π β π΄:πβΆπ ) & β’ (π β π΄ finSupp (0gβπ)) β β’ (π β (π£ β π β¦ ((π΄βπ£)(.rβπ)πΆ)) finSupp (0gβπ)) | ||
| Syntax | ceuf 32659 | Declare the syntax for the Euclidean function index extractor. |
| class EuclF | ||
| Definition | df-euf 32660 | Define the Euclidean function. (Contributed by Thierry Arnoux, 22-Mar-2025.) Use its index-independent form eufid 32662 instead. (New usage is discouraged.) |
| β’ EuclF = Slot ;21 | ||
| Theorem | eufndx 32661 | Index value of the Euclidean function slot. Use ndxarg 17134. (Contributed by Thierry Arnoux, 22-Mar-2025.) (New usage is discouraged.) |
| β’ (EuclFβndx) = ;21 | ||
| Theorem | eufid 32662 | Utility theorem: index-independent form of df-euf 32660. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ EuclF = Slot (EuclFβndx) | ||
| Syntax | cedom 32663 | Declare the syntax for the Euclidean Domain. |
| class EDomn | ||
| Definition | df-edom 32664* | Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ EDomn = {π β IDomn β£ [(EuclFβπ) / π][(Baseβπ) / π£](Fun π β§ (π β (π£ β {(0gβπ)})) β (0[,)+β) β§ βπ β π£ βπ β (π£ β {(0gβπ)})βπ β π£ βπ β π£ (π = ((π(.rβπ)π)(+gβπ)π) β§ (π = (0gβπ) β¨ (πβπ) < (πβπ))))} | ||
| Theorem | ringinveu 32665 | If a ring unit element π admits both a left inverse π and a right inverse π, they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π Β· π) = 1 ) & β’ (π β (π Β· π) = 1 ) β β’ (π β π = π) | ||
| Theorem | isdrng4 32666* | A division ring is a ring in which 1 β 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ Β· = (.rβπ ) & β’ π = (Unitβπ ) & β’ (π β π β Ring) β β’ (π β (π β DivRing β ( 1 β 0 β§ βπ₯ β (π΅ β { 0 })βπ¦ β π΅ ((π₯ Β· π¦) = 1 β§ (π¦ Β· π₯) = 1 )))) | ||
| Theorem | rndrhmcl 32667 | The image of a division ring by a ring homomorphism is a division ring. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| β’ π = (π βΎs ran πΉ) & β’ 0 = (0gβπ) & β’ (π β πΉ β (π RingHom π)) & β’ (π β ran πΉ β { 0 }) & β’ (π β π β DivRing) β β’ (π β π β DivRing) | ||
| Theorem | sdrgdvcl 32668 | A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ / = (/rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π΄ β (SubDRingβπ )) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) β β’ (π β (π / π) β π΄) | ||
| Theorem | sdrginvcl 32669 | A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ πΌ = (invrβπ ) & β’ 0 = (0gβπ ) β β’ ((π΄ β (SubDRingβπ ) β§ π β π΄ β§ π β 0 ) β (πΌβπ) β π΄) | ||
| Theorem | primefldchr 32670 | The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| β’ π = (π βΎs β© (SubDRingβπ )) β β’ (π β DivRing β (chrβπ) = (chrβπ )) | ||
| Syntax | cfldgen 32671 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 32672* | Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 32675). If the base structure is a field, this is a subfield (see fldgenfld 32681 and fldsdrgfld 20558). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.) |
| β’ fldGen = (π β V, π β V β¦ β© {π β (SubDRingβπ) β£ π β π}) | ||
| Theorem | fldgenval 32673* | Value of the field generating function: (πΉ fldGen π) is the smallest sub-division-ring of πΉ containing π. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) = β© {π β (SubDRingβπΉ) β£ π β π}) | ||
| Theorem | fldgenssid 32674 | The field generated by a set of elements contains those elements. See lspssid 20741. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β π β (πΉ fldGen π)) | ||
| Theorem | fldgensdrg 32675 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β (SubDRingβπΉ)) | ||
| Theorem | fldgenssv 32676 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) β β’ (π β (πΉ fldGen π) β π΅) | ||
| Theorem | fldgenss 32677 | Generated subfields preserve subset ordering. ( see lspss 20740 and spanss 30869) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β (πΉ fldGen π)) | ||
| Theorem | fldgenidfld 32678 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) β β’ (π β (πΉ fldGen π) = π) | ||
| Theorem | fldgenssp 32679 | The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β π) | ||
| Theorem | fldgenid 32680 | The subfield of a field πΉ generated by the whole base set of πΉ is πΉ itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) β β’ (π β (πΉ fldGen π΅) = π΅) | ||
| Theorem | fldgenfld 32681 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β Field) & β’ (π β π β π΅) β β’ (π β (πΉ βΎs (πΉ fldGen π)) β Field) | ||
| Theorem | primefldgen1 32682 | The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ (π β π β DivRing) β β’ (π β β© (SubDRingβπ ) = (π fldGen { 1 })) | ||
| Theorem | 1fldgenq 32683 | The field of rational numbers β is generated by 1 in βfld, that is, β is the prime field of βfld. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ (βfld fldGen {1}) = β | ||
| Syntax | corng 32684 | Extend class notation with the class of all ordered rings. |
| class oRing | ||
| Syntax | cofld 32685 | Extend class notation with the class of all ordered fields. |
| class oField | ||
| Definition | df-orng 32686* | Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ oRing = {π β (Ring β© oGrp) β£ [(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π))} | ||
| Definition | df-ofld 32687 | Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
| β’ oField = (Field β© oRing) | ||
| Theorem | isorng 32688* | An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β€ = (leβπ ) β β’ (π β oRing β (π β Ring β§ π β oGrp β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) | ||
| Theorem | orngring 32689 | An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β Ring) | ||
| Theorem | orngogrp 32690 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β oGrp) | ||
| Theorem | isofld 32691 | An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (πΉ β oField β (πΉ β Field β§ πΉ β oRing)) | ||
| Theorem | orngmul 32692 | In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ (π β π΅ β§ 0 β€ π) β§ (π β π΅ β§ 0 β€ π)) β 0 β€ (π Β· π)) | ||
| Theorem | orngsqr 32693 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ π β π΅) β 0 β€ (π Β· π)) | ||
| Theorem | ornglmulle 32694 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ β€ = (leβπ ) & β’ (π β π β€ π) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
| Theorem | orngrmulle 32695 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ β€ = (leβπ ) & β’ (π β π β€ π) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
| Theorem | ornglmullt 32696 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ < = (ltβπ ) & β’ (π β π β DivRing) & β’ (π β π < π) & β’ (π β 0 < π) β β’ (π β (π Β· π) < (π Β· π)) | ||
| Theorem | orngrmullt 32697 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β oRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ < = (ltβπ ) & β’ (π β π β DivRing) & β’ (π β π < π) & β’ (π β 0 < π) β β’ (π β (π Β· π) < (π Β· π)) | ||
| Theorem | orngmullt 32698 | In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ (π β π β oRing) & β’ (π β π β DivRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β 0 < π) β β’ (π β 0 < (π Β· π)) | ||
| Theorem | ofldfld 32699 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Field) | ||
| Theorem | ofldtos 32700 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Toset) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |