![]() |
Metamath
Proof Explorer Theorem List (p. 330 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cyc3co2 32901 | Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) & β’ Β· = (+gβπ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) = ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))) | ||
Theorem | cycpmconjvlem 32902 | Lemma for cycpmconjv 32903. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
β’ (π β πΉ:π·β1-1-ontoβπ·) & β’ (π β π΅ β π·) β β’ (π β ((πΉ βΎ (π· β π΅)) β β‘πΉ) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) | ||
Theorem | cycpmconjv 32903 | A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (toCycβπ·) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π΅ = (Baseβπ) β β’ ((π· β π β§ πΊ β π΅ β§ π β dom π) β ((πΊ + (πβπ)) β πΊ) = (πβ(πΊ β π))) | ||
Theorem | cycpmrn 32904 | The range of the word used to build a cycle is the cycle's orbit, i.e., the set of points it moves. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β 1 < (β―βπ)) β β’ (π β ran π = dom ((πβπ) β I )) | ||
Theorem | tocyccntz 32905* | All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (Cntzβπ) & β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β Disj π₯ β π΄ ran π₯) & β’ (π β π΄ β dom π) β β’ (π β (π β π΄) β (πβ(π β π΄))) | ||
Theorem | evpmval 32906 | Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π΄ = (pmEvenβπ·) β β’ (π· β π β π΄ = (β‘(pmSgnβπ·) β {1})) | ||
Theorem | cnmsgn0g 32907 | The neutral element of the sign subgroup of the complex numbers. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ 1 = (0gβπ) | ||
Theorem | evpmsubg 32908 | The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β π΄ β (SubGrpβπ)) | ||
Theorem | evpmid 32909 | The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ π = (SymGrpβπ·) β β’ (π· β Fin β ( I βΎ π·) β (pmEvenβπ·)) | ||
Theorem | altgnsg 32910 | The alternating group (pmEvenβπ·) is a normal subgroup of the symmetric group. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ π = (SymGrpβπ·) β β’ (π· β Fin β (pmEvenβπ·) β (NrmSGrpβπ)) | ||
Theorem | cyc3evpm 32911 | 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = ((toCycβπ·) β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β πΆ β π΄) | ||
Theorem | cyc3genpmlem 32912* | Lemma for cyc3genpm 32913. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ Β· = (+gβπ) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΏ β π·) & β’ (π β πΈ = (πββ¨βπΌπ½ββ©)) & β’ (π β πΉ = (πββ¨βπΎπΏββ©)) & β’ (π β π· β π) & β’ (π β πΌ β π½) & β’ (π β πΎ β πΏ) β β’ (π β βπ β Word πΆ(πΈ Β· πΉ) = (π Ξ£g π)) | ||
Theorem | cyc3genpm 32913* | The alternating group π΄ is generated by 3-cycles. Property (a) of [Lang] p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) β β’ (π· β Fin β (π β π΄ β βπ€ β Word πΆπ = (π Ξ£g π€))) | ||
Theorem | cycpmgcl 32914 | Cyclic permutations are permutations, similar to cycpmcl 32877, but where the set of cyclic permutations of length π is expressed in terms of a preimage. (Contributed by Thierry Arnoux, 13-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) β β’ ((π· β π β§ π β (0...π)) β πΆ β π΅) | ||
Theorem | cycpmconjslem1 32915 | Lemma for cycpmconjs 32917. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β (β―βπ) = π) β β’ (π β ((β‘π β (πβπ)) β π) = (( I βΎ (0..^π)) cyclShift 1)) | ||
Theorem | cycpmconjslem2 32916* | Lemma for cycpmconjs 32917. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β π β (0...π)) & β’ (π β π· β Fin) & β’ (π β π β πΆ) β β’ (π β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) | ||
Theorem | cycpmconjs 32917* | All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β π β (0...π)) & β’ (π β π· β Fin) & β’ (π β π β πΆ) & β’ (π β π β πΆ) β β’ (π β βπ β π΅ π = ((π + π) β π)) | ||
Theorem | cyc3conja 32918* | All 3-cycles are conjugate in the alternating group An for n>= 5. Property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β 5 β€ π) & β’ (π β π· β Fin) & β’ (π β π β πΆ) & β’ (π β π β πΆ) β β’ (π β βπ β π΄ π = ((π + π) β π)) | ||
Syntax | csgns 32919 | Extend class notation to include the Signum function. |
class sgns | ||
Definition | df-sgns 32920* | Signum function for a structure. See also df-sgn 15061 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.) |
β’ sgns = (π β V β¦ (π₯ β (Baseβπ) β¦ if(π₯ = (0gβπ), 0, if((0gβπ)(ltβπ)π₯, 1, -1)))) | ||
Theorem | sgnsv 32921* | The sign mapping. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π = (π₯ β π΅ β¦ if(π₯ = 0 , 0, if( 0 < π₯, 1, -1)))) | ||
Theorem | sgnsval 32922 | The sign value. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ ((π β π β§ π β π΅) β (πβπ) = if(π = 0 , 0, if( 0 < π, 1, -1))) | ||
Theorem | sgnsf 32923 | The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π:π΅βΆ{-1, 0, 1}) | ||
Syntax | cinftm 32924 | Class notation for the infinitesimal relation. |
class β | ||
Syntax | carchi 32925 | Class notation for the Archimedean property. |
class Archi | ||
Definition | df-inftm 32926* | Define the relation "π₯ is infinitesimal with respect to π¦ " for a structure π€. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ β = (π€ β V β¦ {β¨π₯, π¦β© β£ ((π₯ β (Baseβπ€) β§ π¦ β (Baseβπ€)) β§ ((0gβπ€)(ltβπ€)π₯ β§ βπ β β (π(.gβπ€)π₯)(ltβπ€)π¦))}) | ||
Definition | df-archi 32927 | A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ Archi = {π€ β£ (ββπ€) = β } | ||
Theorem | inftmrel 32928 | The infinitesimal relation for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) β β’ (π β π β (ββπ) β (π΅ Γ π΅)) | ||
Theorem | isinftm 32929* | Express π₯ is infinitesimal with respect to π¦ for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ Β· = (.gβπ) & β’ < = (ltβπ) β β’ ((π β π β§ π β π΅ β§ π β π΅) β (π(ββπ)π β ( 0 < π β§ βπ β β (π Β· π) < π))) | ||
Theorem | isarchi 32930* | Express the predicate "π is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ββπ) β β’ (π β π β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯ < π¦)) | ||
Theorem | pnfinf 32931 | Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018.) |
β’ (π΄ β β+ β π΄(βββ*π )+β) | ||
Theorem | xrnarchi 32932 | The completed real line is not Archimedean. (Contributed by Thierry Arnoux, 1-Feb-2018.) |
β’ Β¬ β*π β Archi | ||
Theorem | isarchi2 32933* | 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 32934 | A submonoid is archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Archi) | ||
Theorem | isarchi3 32935* | 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 32936* | 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 32937* | 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 32938* | 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 32939* | Lemma for archiabl 32946: 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 32940* | Lemma for archiabl 32946. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) β β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) | ||
Theorem | archiabllem1 32941* | 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 32942* | Lemma for archiabl 32946, 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 32943* | Lemma for archiabl 32946. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β Β¬ (π + π) < (π + π)) | ||
Theorem | archiabllem2b 32944* | Lemma for archiabl 32946. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) = (π + π)) | ||
Theorem | archiabllem2 32945* | 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 32946 | Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ ((π β oGrp β§ (oppgβπ) β oGrp β§ π β Archi) β π β Abel) | ||
Syntax | cslmd 32947 | Extend class notation with class of all semimodules. |
class SLMod | ||
Definition | df-slmd 32948* | 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 32949* | 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 32950 | 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 32951 | Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β LMod β π β SLMod) | ||
Theorem | slmdcmn 32952 | A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β SLMod β π β CMnd) | ||
Theorem | slmdmnd 32953 | A semimodule is a monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β SLMod β π β Mnd) | ||
Theorem | slmdsrg 32954 | 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 32955 | 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 32956 | Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) | ||
Theorem | slmdmcl 32957 | 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 32958 | 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 32959 | 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 32960 | 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 32961 | Closure of scalar product for a semiring left module. (hvmulcl 30862 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 32962 | Distributive law for scalar product. (ax-hvdistr1 30857 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 32963 | Distributive law for scalar product. (ax-hvdistr1 30857 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 32964 | Associative law for scalar product. (ax-hvmulass 30856 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 32965 | 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 32966 | 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 32967 | Scalar product with ring unity. (ax-hvmulid 30855 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 32968 | The zero vector is a vector. (ax-hv0cl 30852 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 32969 | Left identity law for the zero vector. (hvaddlid 30872 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 32970 | Right identity law for the zero vector. (ax-hvaddid 30853 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 32971 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 30859 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 32972 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 30873 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 32973* | 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 32974* | 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 32975 | 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 | cringmul32d 32976 | Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32 11405. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π Β· π) Β· π) = ((π Β· π) Β· π)) | ||
Theorem | ringdid 32977 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
Theorem | ringdird 32978 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | urpropd 32979* | Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) & β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (π₯(.rβπ)π¦) = (π₯(.rβπ)π¦)) β β’ (π β (1rβπ) = (1rβπ)) | ||
Theorem | frobrhm 32980* | 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 32981 | 1r is unaffected by restriction. This is a bit more generic than subrg1 20520. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 1 β π΄ β§ π΄ β π΅) β 1 = (1rβπ)) | ||
Theorem | ringinvval 32982* | 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 32983 | Cancellation law for common factor in ratio. (divcan5 11941 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π β§ π β π)) β ((π Β· π) / (π Β· π)) = (π / π)) | ||
Theorem | subrgchr 32984 | If π΄ is a subring of π , then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
β’ (π΄ β (SubRingβπ ) β (chrβ(π βΎs π΄)) = (chrβπ )) | ||
Theorem | rmfsupp2 32985* | 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βπ)) | ||
Theorem | unitnz 32986 | In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β NzRing) & β’ (π β π β π) β β’ (π β π β 0 ) | ||
Theorem | irrednzr 32987 | A ring with an irreducible element cannot be the zero ring. (Contributed by Thierry Arnoux, 18-May-2025.) |
β’ πΌ = (Irredβπ ) & β’ (π β π β Ring) & β’ (π β π β πΌ) β β’ (π β π β NzRing) | ||
Theorem | 0ringsubrg 32988 | A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) & β’ (π β π β (SubRingβπ )) β β’ (π β (β―βπ) = 1) | ||
Theorem | 0ringcring 32989 | The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) β β’ (π β π β CRing) | ||
Syntax | cerl 32990 | Syntax for ring localization equivalence class operation. |
class ~RL | ||
Syntax | crloc 32991 | Syntax for ring localization operation. |
class RLocal | ||
Definition | df-erl 32992* | Define the operation giving the equivalence relation used in the localization of a ring π by a set π . Two pairs π = β¨π₯, π¦β© and π = β¨π§, π€β© are equivalent if there exists π‘ β π such that π‘ Β· (π₯ Β· π€ β π§ Β· π¦) = 0. This corresponds to the usual comparison of fractions π₯ / π¦ and π§ / π€. (Contributed by Thierry Arnoux, 28-Apr-2025.) |
β’ ~RL = (π β V, π β V β¦ β¦(.rβπ) / π₯β¦β¦((Baseβπ) Γ π ) / π€β¦{β¨π, πβ© β£ ((π β π€ β§ π β π€) β§ βπ‘ β π (π‘π₯(((1st βπ)π₯(2nd βπ))(-gβπ)((1st βπ)π₯(2nd βπ)))) = (0gβπ))}) | ||
Definition | df-rloc 32993* | Define the operation giving the localization of a ring π by a given set π . The localized ring π RLocal π is the set of equivalence classes of pairs of elements in π over the relation π ~RL π with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025.) |
β’ RLocal = (π β V, π β V β¦ β¦(.rβπ) / π₯β¦β¦((Baseβπ) Γ π ) / π€β¦((({β¨(Baseβndx), π€β©, β¨(+gβndx), (π β π€, π β π€ β¦ β¨(((1st βπ)π₯(2nd βπ))(+gβπ)((1st βπ)π₯(2nd βπ))), ((2nd βπ)π₯(2nd βπ))β©)β©, β¨(.rβndx), (π β π€, π β π€ β¦ β¨((1st βπ)π₯(1st βπ)), ((2nd βπ)π₯(2nd βπ))β©)β©} βͺ {β¨(Scalarβndx), (Scalarβπ)β©, β¨( Β·π βndx), (π β (Baseβ(Scalarβπ)), π β π€ β¦ β¨(π( Β·π βπ)(1st βπ)), (2nd βπ)β©)β©, β¨(Β·πβndx), β β©}) βͺ {β¨(TopSetβndx), ((TopSetβπ) Γt ((TopSetβπ) βΎt π ))β©, β¨(leβndx), {β¨π, πβ© β£ ((π β π€ β§ π β π€) β§ ((1st βπ)π₯(2nd βπ))(leβπ)((1st βπ)π₯(2nd βπ)))}β©, β¨(distβndx), (π β π€, π β π€ β¦ (((1st βπ)π₯(2nd βπ))(distβπ)((1st βπ)π₯(2nd βπ))))β©}) /s (π ~RL π ))) | ||
Theorem | reldmrloc 32994 | Ring localization is a proper operator, so it can be used with ovprc1 7452. (Contributed by Thierry Arnoux, 10-May-2025.) |
β’ Rel dom RLocal | ||
Theorem | erlval 32995* | Value of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (π΅ Γ π) & β’ βΌ = {β¨π, πβ© β£ ((π β π β§ π β π) β§ βπ‘ β π (π‘ Β· (((1st βπ) Β· (2nd βπ)) β ((1st βπ) Β· (2nd βπ)))) = 0 )} & β’ (π β π β π΅) β β’ (π β (π ~RL π) = βΌ ) | ||
Theorem | rlocval 32996* | Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ β€ = (leβπ ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ πΆ = ( Β·π βπ ) & β’ π = (π΅ Γ π) & β’ βΌ = (π ~RL π) & β’ π½ = (TopSetβπ ) & β’ π· = (distβπ ) & β’ β = (π β π, π β π β¦ β¨(((1st βπ) Β· (2nd βπ)) + ((1st βπ) Β· (2nd βπ))), ((2nd βπ) Β· (2nd βπ))β©) & β’ β = (π β π, π β π β¦ β¨((1st βπ) Β· (1st βπ)), ((2nd βπ) Β· (2nd βπ))β©) & β’ Γ = (π β πΎ, π β π β¦ β¨(ππΆ(1st βπ)), (2nd βπ)β©) & β’ β² = {β¨π, πβ© β£ ((π β π β§ π β π) β§ ((1st βπ) Β· (2nd βπ)) β€ ((1st βπ) Β· (2nd βπ)))} & β’ πΈ = (π β π, π β π β¦ (((1st βπ) Β· (2nd βπ))π·((1st βπ) Β· (2nd βπ)))) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β (π RLocal π) = ((({β¨(Baseβndx), πβ©, β¨(+gβndx), β β©, β¨(.rβndx), β β©} βͺ {β¨(Scalarβndx), πΉβ©, β¨( Β·π βndx), Γ β©, β¨(Β·πβndx), β β©}) βͺ {β¨(TopSetβndx), (π½ Γt (π½ βΎt π))β©, β¨(leβndx), β² β©, β¨(distβndx), πΈβ©}) /s βΌ )) | ||
Theorem | erlcl1 32997 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~RL π) & β’ (π β π β π΅) & β’ (π β π βΌ π) β β’ (π β π β (π΅ Γ π)) | ||
Theorem | erlcl2 32998 | Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~RL π) & β’ (π β π β π΅) & β’ (π β π βΌ π) β β’ (π β π β (π΅ Γ π)) | ||
Theorem | erldi 32999* | Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~RL π) & β’ (π β π β π΅) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π βΌ π) β β’ (π β βπ‘ β π (π‘ Β· (((1st βπ) Β· (2nd βπ)) β ((1st βπ) Β· (2nd βπ)))) = 0 ) | ||
Theorem | erlbrd 33000 | Deduce the ring localization equivalence relation. If for some π β π we have π Β· (πΈ Β· π» β πΉ Β· πΊ) = 0, then pairs β¨πΈ, πΊβ© and β¨πΉ, π»β© are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.) |
β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~RL π) & β’ (π β π β π΅) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π = β¨πΈ, πΊβ©) & β’ (π β π = β¨πΉ, π»β©) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π) & β’ (π β π» β π) & β’ (π β π β π) & β’ (π β (π Β· ((πΈ Β· π») β (πΉ Β· πΊ))) = 0 ) β β’ (π β π βΌ π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |