![]() |
Metamath
Proof Explorer Theorem List (p. 205 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issubdrg 20401* | Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β DivRing β§ π΄ β (SubRingβπ )) β (π β DivRing β βπ₯ β (π΄ β { 0 })(πΌβπ₯) β π΄)) | ||
Syntax | csdrg 20402 | Syntax for subfields (sub-division-rings). |
class SubDRing | ||
Definition | df-sdrg 20403* | Define the function associating with a ring the set of its sub-division-rings. A sub-division-ring of a ring is a subset of its base set which is a division ring when equipped with the induced structure (sum, multiplication, zero, and unity). If a ring is commutative (resp., a field), then its sub-division-rings are commutative (resp., are fields) (fldsdrgfld 20414), so we do not make a specific definition for subfields. (Contributed by Stefan O'Rear, 3-Oct-2015.) TODO: extend this definition to a function with domain V or at least Ring and not only DivRing. |
β’ SubDRing = (π€ β DivRing β¦ {π β (SubRingβπ€) β£ (π€ βΎs π ) β DivRing}) | ||
Theorem | issdrg 20404 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ (π βΎs π) β DivRing)) | ||
Theorem | sdrgrcl 20405 | Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgdrng 20406 | A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π β DivRing) | ||
Theorem | sdrgsubrg 20407 | A sub-division-ring is a subring. (Contributed by SN, 19-Feb-2025.) |
β’ (π΄ β (SubDRingβπ ) β π΄ β (SubRingβπ )) | ||
Theorem | sdrgid 20408 | Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β π΅ β (SubDRingβπ )) | ||
Theorem | sdrgss 20409 | A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π΅ = (Baseβπ ) β β’ (π β (SubDRingβπ ) β π β π΅) | ||
Theorem | sdrgbas 20410 | Base set of a sub-division-ring structure. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) β β’ (π΄ β (SubDRingβπ ) β π΄ = (Baseβπ)) | ||
Theorem | issdrg2 20411* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ πΌ = (invrβπ ) & β’ 0 = (0gβπ ) β β’ (π β (SubDRingβπ ) β (π β DivRing β§ π β (SubRingβπ ) β§ βπ₯ β (π β { 0 })(πΌβπ₯) β π)) | ||
Theorem | sdrgunit 20412 | A unit of a sub-division-ring is a nonzero element of the subring. (Contributed by SN, 19-Feb-2025.) |
β’ π = (π βΎs π΄) & β’ 0 = (0gβπ ) & β’ π = (Unitβπ) β β’ (π΄ β (SubDRingβπ ) β (π β π β (π β π΄ β§ π β 0 ))) | ||
Theorem | imadrhmcl 20413 | The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025.) |
β’ π = (π βΎs (πΉ β π)) & β’ 0 = (0gβπ) & β’ (π β πΉ β (π RingHom π)) & β’ (π β π β (SubDRingβπ)) & β’ (π β ran πΉ β { 0 }) β β’ (π β π β DivRing) | ||
Theorem | fldsdrgfld 20414 | A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
β’ ((πΉ β Field β§ π΄ β (SubDRingβπΉ)) β (πΉ βΎs π΄) β Field) | ||
Theorem | acsfn1p 20415* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π β π β§ βπ β π πΈ β π) β {π β π« π β£ βπ β (π β© π)πΈ β π} β (ACSβπ)) | ||
Theorem | subrgacs 20416 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (SubRingβπ ) β (ACSβπ΅)) | ||
Theorem | sdrgacs 20417 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β DivRing β (SubDRingβπ ) β (ACSβπ΅)) | ||
Theorem | cntzsdrg 20418 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (mulGrpβπ ) & β’ π = (Cntzβπ) β β’ ((π β DivRing β§ π β π΅) β (πβπ) β (SubDRingβπ )) | ||
Theorem | subdrgint 20419* | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ πΏ = (π βΎs β© π) & β’ (π β π β DivRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β β ) & β’ ((π β§ π β π) β (π βΎs π ) β DivRing) β β’ (π β πΏ β DivRing) | ||
Theorem | sdrgint 20420 | The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ ((π β DivRing β§ π β (SubDRingβπ ) β§ π β β ) β β© π β (SubDRingβπ )) | ||
Theorem | primefld 20421 | The smallest sub division ring of a division ring, here named π, is a field, called the Prime Field of π . (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023.) |
β’ π = (π βΎs β© (SubDRingβπ )) β β’ (π β DivRing β π β Field) | ||
Theorem | primefld0cl 20422 | The prime field contains the zero element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
β’ 0 = (0gβπ ) β β’ (π β DivRing β 0 β β© (SubDRingβπ )) | ||
Theorem | primefld1cl 20423 | The prime field contains the unity element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023.) |
β’ 1 = (1rβπ ) β β’ (π β DivRing β 1 β β© (SubDRingβπ )) | ||
Syntax | cabv 20424 | The set of absolute values on a ring. |
class AbsVal | ||
Definition | df-abv 20425* | Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15183 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ AbsVal = (π β Ring β¦ {π β ((0[,)+β) βm (Baseβπ)) β£ βπ₯ β (Baseβπ)(((πβπ₯) = 0 β π₯ = (0gβπ)) β§ βπ¦ β (Baseβπ)((πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯(+gβπ)π¦)) β€ ((πβπ₯) + (πβπ¦))))}) | ||
Theorem | abvfval 20426* | Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β π΄ = {π β ((0[,)+β) βm π΅) β£ βπ₯ β π΅ (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πβ(π₯ Β· π¦)) = ((πβπ₯) Β· (πβπ¦)) β§ (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦))))}) | ||
Theorem | isabv 20427* | Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΉ β π΄ β (πΉ:π΅βΆ(0[,)+β) β§ βπ₯ β π΅ (((πΉβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π΅ ((πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) | ||
Theorem | isabvd 20428* | Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.) |
β’ (π β π΄ = (AbsValβπ )) & β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β 0 = (0gβπ )) & β’ (π β π β Ring) & β’ (π β πΉ:π΅βΆβ) & β’ (π β (πΉβ 0 ) = 0) & β’ ((π β§ π₯ β π΅ β§ π₯ β 0 ) β 0 < (πΉβπ₯)) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) & β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β β’ (π β πΉ β π΄) | ||
Theorem | abvrcl 20429 | Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) β β’ (πΉ β π΄ β π β Ring) | ||
Theorem | abvfge0 20430 | An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π΄ β πΉ:π΅βΆ(0[,)+β)) | ||
Theorem | abvf 20431 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ (πΉ β π΄ β πΉ:π΅βΆβ) | ||
Theorem | abvcl 20432 | An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β (πΉβπ) β β) | ||
Theorem | abvge0 20433 | The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β 0 β€ (πΉβπ)) | ||
Theorem | abveq0 20434 | The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β ((πΉβπ) = 0 β π = 0 )) | ||
Theorem | abvne0 20435 | The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β (πΉβπ) β 0) | ||
Theorem | abvgt0 20436 | The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β 0 ) β 0 < (πΉβπ)) | ||
Theorem | abvmul 20437 | An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π Β· π)) = ((πΉβπ) Β· (πΉβπ))) | ||
Theorem | abvtri 20438 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) β€ ((πΉβπ) + (πΉβπ))) | ||
Theorem | abv0 20439 | The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 0 = (0gβπ ) β β’ (πΉ β π΄ β (πΉβ 0 ) = 0) | ||
Theorem | abv1z 20440 | The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ ((πΉ β π΄ β§ 1 β 0 ) β (πΉβ 1 ) = 1) | ||
Theorem | abv1 20441 | The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ 1 = (1rβπ ) β β’ ((π β DivRing β§ πΉ β π΄) β (πΉβ 1 ) = 1) | ||
Theorem | abvneg 20442 | The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ π = (invgβπ ) β β’ ((πΉ β π΄ β§ π β π΅) β (πΉβ(πβπ)) = (πΉβπ)) | ||
Theorem | abvsubtri 20443 | An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ β = (-gβπ ) β β’ ((πΉ β π΄ β§ π β π΅ β§ π β π΅) β (πΉβ(π β π)) β€ ((πΉβπ) + (πΉβπ))) | ||
Theorem | abvrec 20444 | The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΌ = (invrβπ ) β β’ (((π β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β 0 )) β (πΉβ(πΌβπ)) = (1 / (πΉβπ))) | ||
Theorem | abvdiv 20445 | The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ / = (/rβπ ) β β’ (((π β DivRing β§ πΉ β π΄) β§ (π β π΅ β§ π β π΅ β§ π β 0 )) β (πΉβ(π / π)) = ((πΉβπ) / (πΉβπ))) | ||
Theorem | abvdom 20446 | Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((πΉ β π΄ β§ (π β π΅ β§ π β 0 ) β§ (π β π΅ β§ π β 0 )) β (π Β· π) β 0 ) | ||
Theorem | abvres 20447 | The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΄ = (AbsValβπ ) & β’ π = (π βΎs πΆ) & β’ π΅ = (AbsValβπ) β β’ ((πΉ β π΄ β§ πΆ β (SubRingβπ )) β (πΉ βΎ πΆ) β π΅) | ||
Theorem | abvtrivd 20448* | The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΉ = (π₯ β π΅ β¦ if(π₯ = 0 , 0, 1)) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (π¦ Β· π§) β 0 ) β β’ (π β πΉ β π΄) | ||
Theorem | abvtriv 20449* | The trivial absolute value. (This theorem is true as long as π is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 20446 is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΄ = (AbsValβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΉ = (π₯ β π΅ β¦ if(π₯ = 0 , 0, 1)) β β’ (π β DivRing β πΉ β π΄) | ||
Theorem | abvpropd 20450* | If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (AbsValβπΎ) = (AbsValβπΏ)) | ||
Syntax | cstf 20451 | Extend class notation with the functionalization of the *-ring involution. |
class *rf | ||
Syntax | csr 20452 | Extend class notation with class of all *-rings. |
class *-Ring | ||
Definition | df-staf 20453* | Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *π as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ *rf = (π β V β¦ (π₯ β (Baseβπ) β¦ ((*πβπ)βπ₯))) | ||
Definition | df-srng 20454* | Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.) |
β’ *-Ring = {π β£ [(*rfβπ) / π](π β (π RingHom (opprβπ)) β§ π = β‘π)} | ||
Theorem | staffval 20455* | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ β = (*rfβπ ) β β’ β = (π₯ β π΅ β¦ ( β βπ₯)) | ||
Theorem | stafval 20456 | The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ β = (*rfβπ ) β β’ (π΄ β π΅ β ( β βπ΄) = ( β βπ΄)) | ||
Theorem | staffn 20457 | The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ β = (*rfβπ ) β β’ ( β Fn π΅ β β = β ) | ||
Theorem | issrng 20458 | The predicate "is a star ring". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.) |
β’ π = (opprβπ ) & β’ β = (*rfβπ ) β β’ (π β *-Ring β ( β β (π RingHom π) β§ β = β‘ β )) | ||
Theorem | srngrhm 20459 | The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (opprβπ ) & β’ β = (*rfβπ ) β β’ (π β *-Ring β β β (π RingHom π)) | ||
Theorem | srngring 20460 | A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (π β *-Ring β π β Ring) | ||
Theorem | srngcnv 20461 | The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*rfβπ ) β β’ (π β *-Ring β β = β‘ β ) | ||
Theorem | srngf1o 20462 | The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*rfβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β *-Ring β β :π΅β1-1-ontoβπ΅) | ||
Theorem | srngcl 20463 | The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*πβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β *-Ring β§ π β π΅) β ( β βπ) β π΅) | ||
Theorem | srngnvl 20464 | The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*πβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β *-Ring β§ π β π΅) β ( β β( β βπ)) = π) | ||
Theorem | srngadd 20465 | The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*πβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β *-Ring β§ π β π΅ β§ π β π΅) β ( β β(π + π)) = (( β βπ) + ( β βπ))) | ||
Theorem | srngmul 20466 | The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*πβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β *-Ring β§ π β π΅ β§ π β π΅) β ( β β(π Β· π)) = (( β βπ) Β· ( β βπ))) | ||
Theorem | srng1 20467 | The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *π to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd 20469.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ β = (*πβπ ) & β’ 1 = (1rβπ ) β β’ (π β *-Ring β ( β β 1 ) = 1 ) | ||
Theorem | srng0 20468 | The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ β = (*πβπ ) & β’ 0 = (0gβπ ) β β’ (π β *-Ring β ( β β 0 ) = 0 ) | ||
Theorem | issrngd 20469* | Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2015.) |
β’ (π β πΎ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β β = (*πβπ )) & β’ (π β π β Ring) & β’ ((π β§ π₯ β πΎ) β ( β βπ₯) β πΎ) & β’ ((π β§ π₯ β πΎ β§ π¦ β πΎ) β ( β β(π₯ + π¦)) = (( β βπ₯) + ( β βπ¦))) & β’ ((π β§ π₯ β πΎ β§ π¦ β πΎ) β ( β β(π₯ Β· π¦)) = (( β βπ¦) Β· ( β βπ₯))) & β’ ((π β§ π₯ β πΎ) β ( β β( β βπ₯)) = π₯) β β’ (π β π β *-Ring) | ||
Theorem | idsrngd 20470* | A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.) |
β’ π΅ = (Baseβπ ) & β’ β = (*πβπ ) & β’ (π β π β CRing) & β’ ((π β§ π₯ β π΅) β ( β βπ₯) = π₯) β β’ (π β π β *-Ring) | ||
Syntax | clmod 20471 | Extend class notation with class of all left modules. |
class LMod | ||
Syntax | cscaf 20472 | The functionalization of the scalar multiplication operation. |
class Β·sf | ||
Definition | df-lmod 20473* | Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.) |
β’ LMod = {π β Grp β£ [(Baseβπ) / π£][(+gβπ) / π][(Scalarβπ) / π][( Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))} | ||
Definition | df-scaf 20474* | Define the functionalization of the Β·π operator. This restricts the value of Β·π to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ Β·sf = (π β V β¦ (π₯ β (Baseβ(Scalarβπ)), π¦ β (Baseβπ) β¦ (π₯( Β·π βπ)π¦))) | ||
Theorem | islmod 20475* | The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) β β’ (π β LMod β (π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) | ||
Theorem | lmodlema 20476 | Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β πΎ) β§ (π β π β§ π β π)) β (((π Β· π) β π β§ (π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) β§ (((π Γ π ) Β· π) = (π Β· (π Β· π)) β§ ( 1 Β· π) = π))) | ||
Theorem | islmodd 20477* | Properties that determine a left module. See note in isgrpd2 18842 regarding the π on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.) |
β’ (π β π = (Baseβπ)) & β’ (π β + = (+gβπ)) & β’ (π β πΉ = (Scalarβπ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β π΅ = (BaseβπΉ)) & β’ (π β ⨣ = (+gβπΉ)) & β’ (π β Γ = (.rβπΉ)) & β’ (π β 1 = (1rβπΉ)) & β’ (π β πΉ β Ring) & β’ (π β π β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π β§ π§ β π)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π)) β ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π)) β ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ π₯ β π) β ( 1 Β· π₯) = π₯) β β’ (π β π β LMod) | ||
Theorem | lmodgrp 20478 | A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.) |
β’ (π β LMod β π β Grp) | ||
Theorem | lmodring 20479 | The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) β β’ (π β LMod β πΉ β Ring) | ||
Theorem | lmodfgrp 20480 | The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) β β’ (π β LMod β πΉ β Grp) | ||
Theorem | lmodgrpd 20481 | A left module is a group. (Contributed by SN, 16-May-2024.) |
β’ (π β π β LMod) β β’ (π β π β Grp) | ||
Theorem | lmodbn0 20482 | The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π΅ = (Baseβπ) β β’ (π β LMod β π΅ β β ) | ||
Theorem | lmodacl 20483 | Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) | ||
Theorem | lmodmcl 20484 | Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = (.rβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β πΎ) β (π Β· π) β πΎ) | ||
Theorem | lmodsn0 20485 | The set of scalars in a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π β LMod β π΅ β β ) | ||
Theorem | lmodvacl 20486 | Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | lmodass 20487 | Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β LMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | lmodlcan 20488 | Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β LMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | lmodvscl 20489 | Closure of scalar product for a left module. (hvmulcl 30266 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ π β πΎ β§ π β π) β (π Β· π) β π) | ||
Theorem | scaffval 20490* | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = ( Β·sf βπ) & β’ Β· = ( Β·π βπ) β β’ β = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) | ||
Theorem | scafval 20491 | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = ( Β·sf βπ) & β’ Β· = ( Β·π βπ) β β’ ((π β πΎ β§ π β π΅) β (π β π) = (π Β· π)) | ||
Theorem | scafeq 20492 | If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = ( Β·sf βπ) & β’ Β· = ( Β·π βπ) β β’ ( Β· Fn (πΎ Γ π΅) β β = Β· ) | ||
Theorem | scaffn 20493 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = ( Β·sf βπ) β β’ β Fn (πΎ Γ π΅) | ||
Theorem | lmodscaf 20494 | The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π΅ = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = ( Β·sf βπ) β β’ (π β LMod β β :(πΎ Γ π΅)βΆπ΅) | ||
Theorem | lmodvsdi 20495 | Distributive law for scalar product (left-distributivity). (ax-hvdistr1 30261 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β π β§ π β π)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
Theorem | lmodvsdir 20496 | Distributive law for scalar product (right-distributivity). (ax-hvdistr1 30261 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | lmodvsass 20497 | Associative law for scalar product. (ax-hvmulass 30260 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) & β’ Γ = (.rβπΉ) β β’ ((π β LMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π Γ π ) Β· π) = (π Β· (π Β· π))) | ||
Theorem | lmod0cl 20498 | The ring zero in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 0 = (0gβπΉ) β β’ (π β LMod β 0 β πΎ) | ||
Theorem | lmod1cl 20499 | The ring unity in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ 1 = (1rβπΉ) β β’ (π β LMod β 1 β πΎ) | ||
Theorem | lmodvs1 20500 | Scalar product with the ring unity. (ax-hvmulid 30259 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπΉ) β β’ ((π β LMod β§ π β π) β ( 1 Β· π) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |