HomeTheorem List (p. 325 of 479)
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. 325 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: | Metamath Proof Explorer
(1-30166) |
Hilbert Space Explorer
(30167-31689) |
Users' Mathboxes
(31690-47842) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fldgenss 32401 | Generated subfields preserve subset ordering. ( see lspss 20594 and spanss 30596) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β π΅) & β’ (π β π β π) β β’ (π β (πΉ fldGen π) β (πΉ fldGen π)) | ||
| Theorem | fldgenidfld 32402 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β DivRing) & β’ (π β π β (SubDRingβπΉ)) β β’ (π β (πΉ fldGen π) = π) | ||
| Theorem | fldgenssp 32403 | 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 32404 | 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 32405 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| β’ π΅ = (BaseβπΉ) & β’ (π β πΉ β Field) & β’ (π β π β π΅) β β’ (π β (πΉ βΎs (πΉ fldGen π)) β Field) | ||
| Theorem | primefldgen1 32406 | 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 32407 | 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 32408 | Extend class notation with the class of all ordered rings. |
| class oRing | ||
| Syntax | cofld 32409 | Extend class notation with the class of all ordered fields. |
| class oField | ||
| Definition | df-orng 32410* | 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 32411 | 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 32412* | 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 32413 | An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β Ring) | ||
| Theorem | orngogrp 32414 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (π β oRing β π β oGrp) | ||
| Theorem | isofld 32415 | 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 32416 | 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 32417 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ π΅ = (Baseβπ ) & β’ β€ = (leβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β oRing β§ π β π΅) β 0 β€ (π Β· π)) | ||
| Theorem | ornglmulle 32418 | 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 32419 | 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 32420 | 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 32421 | 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 32422 | 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 32423 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Field) | ||
| Theorem | ofldtos 32424 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| β’ (πΉ β oField β πΉ β Toset) | ||
| Theorem | orng0le1 32425 | In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ 0 = (0gβπΉ) & β’ 1 = (1rβπΉ) & β’ β€ = (leβπΉ) β β’ (πΉ β oRing β 0 β€ 1 ) | ||
| Theorem | ofldlt1 32426 | In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ 0 = (0gβπΉ) & β’ 1 = (1rβπΉ) & β’ < = (ltβπΉ) β β’ (πΉ β oField β 0 < 1 ) | ||
| Theorem | ofldchr 32427 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
| β’ (πΉ β oField β (chrβπΉ) = 0) | ||
| Theorem | suborng 32428 | Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ ((π β oRing β§ (π βΎs π΄) β Ring) β (π βΎs π΄) β oRing) | ||
| Theorem | subofld 32429 | Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ ((πΉ β oField β§ (πΉ βΎs π΄) β Field) β (πΉ βΎs π΄) β oField) | ||
| Theorem | isarchiofld 32430* | Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| β’ π΅ = (Baseβπ) & β’ π» = (β€RHomβπ) & β’ < = (ltβπ) β β’ (π β oField β (π β Archi β βπ₯ β π΅ βπ β β π₯ < (π»βπ))) | ||
| Theorem | rhmdvd 32431 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| β’ π = (Unitβπ) & β’ π = (Baseβπ ) & β’ / = (/rβπ) & β’ Β· = (.rβπ ) β β’ ((πΉ β (π RingHom π) β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ((πΉβπ΅) β π β§ (πΉβπΆ) β π)) β ((πΉβπ΄) / (πΉβπ΅)) = ((πΉβ(π΄ Β· πΆ)) / (πΉβ(π΅ Β· πΆ)))) | ||
| Theorem | kerunit 32432 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
| β’ π = (Unitβπ ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) β β’ ((πΉ β (π RingHom π) β§ (π β© (β‘πΉ β { 0 })) β β ) β 1 = 0 ) | ||
| Syntax | cresv 32433 | Extend class notation with the scalar restriction operation. |
| class βΎv | ||
| Definition | df-resv 32434* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
| β’ βΎv = (π€ β V, π₯ β V β¦ if((Baseβ(Scalarβπ€)) β π₯, π€, (π€ sSet β¨(Scalarβndx), ((Scalarβπ€) βΎs π₯)β©))) | ||
| Theorem | reldmresv 32435 | The scalar restriction is a proper operator, so it can be used with ovprc1 7447. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ Rel dom βΎv | ||
| Theorem | resvval 32436 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π β π β§ π΄ β π) β π = if(π΅ β π΄, π, (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) | ||
| Theorem | resvid2 32437 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π΅ β π΄ β§ π β π β§ π΄ β π) β π = π) | ||
| Theorem | resvval2 32438 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) | ||
| Theorem | resvsca 32439 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ )) | ||
| Theorem | resvlem 32440 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (Scalarβndx) β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
| Theorem | resvlemOLD 32441 | Obsolete version of resvlem 32440 as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot π & β’ π β β & β’ π β 5 β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
| Theorem | resvbas 32442 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
| Theorem | resvbasOLD 32443 | Obsolete proof of resvbas 32442 as of 31-Oct-2024. Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
| Theorem | resvplusg 32444 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
| Theorem | resvplusgOLD 32445 | Obsolete proof of resvplusg 32444 as of 31-Oct-2024. +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
| Theorem | resvvsca 32446 | Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
| Theorem | resvvscaOLD 32447 | Obsolete proof of resvvsca 32446 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
| Theorem | resvmulr 32448 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
| Theorem | resvmulrOLD 32449 | Obsolete proof of resvmulr 32448 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
| Theorem | resv0g 32450 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β 0 = (0gβπ»)) | ||
| Theorem | resv1r 32451 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) & β’ 1 = (1rβπΊ) β β’ (π΄ β π β 1 = (1rβπ»)) | ||
| Theorem | resvcmn 32452 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ π» = (πΊ βΎv π΄) β β’ (π΄ β π β (πΊ β CMnd β π» β CMnd)) | ||
| Theorem | gzcrng 32453 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| β’ (βfld βΎs β€[i]) β CRing | ||
| Theorem | reofld 32454 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| β’ βfld β oField | ||
| Theorem | nn0omnd 32455 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| β’ (βfld βΎs β0) β oMnd | ||
| Theorem | rearchi 32456 | The field of the real numbers is Archimedean. See also arch 12468. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| β’ βfld β Archi | ||
| Theorem | nn0archi 32457 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| β’ (βfld βΎs β0) β Archi | ||
| Theorem | xrge0slmod 32458 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| β’ πΊ = (β*π βΎs (0[,]+β)) & β’ π = (πΊ βΎv (0[,)+β)) β β’ π β SLMod | ||
| Theorem | qusker 32459* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| β’ π = (Baseβπ) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) & β’ π = (π /s (π ~QG πΊ)) & β’ 0 = (0gβπ) β β’ (πΊ β (NrmSGrpβπ) β (β‘πΉ β { 0 }) = πΊ) | ||
| Theorem | eqgvscpbl 32460 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) β β’ (π β (π βΌ π β (πΎ Β· π) βΌ (πΎ Β· π))) | ||
| Theorem | qusvscpbl 32461* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) & β’ π = (π /s (π ~QG πΊ)) & β’ β = ( Β·π βπ) & β’ πΉ = (π₯ β π΅ β¦ [π₯](π ~QG πΊ)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΉβπ) = (πΉβπ) β (πΉβ(πΎ Β· π)) = (πΉβ(πΎ Β· π)))) | ||
| Theorem | qusvsval 32462 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) & β’ π = (π /s (π ~QG πΊ)) & β’ β = ( Β·π βπ) & β’ (π β π β π΅) β β’ (π β (πΎ β [π](π ~QG πΊ)) = [(πΎ Β· π)](π ~QG πΊ)) | ||
| Theorem | imaslmod 32463* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
| β’ (π β π = (πΉ βs π)) & β’ π = (Baseβπ) & β’ π = (Baseβ(Scalarβπ)) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π β LMod) β β’ (π β π β LMod) | ||
| Theorem | quslmod 32464 | If πΊ is a submodule in π, then π = π / πΊ is a left module, called the quotient module of π by πΊ. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π = (π /s (π ~QG πΊ)) & β’ π = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) β β’ (π β π β LMod) | ||
| Theorem | quslmhm 32465* | If πΊ is a submodule of π, then the "natural map" from elements to their cosets is a left module homomorphism from π to π / πΊ. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π = (π /s (π ~QG πΊ)) & β’ π = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) β β’ (π β πΉ β (π LMHom π)) | ||
| Theorem | quslvec 32466 | If π is a vector subspace in π, then π = π / π is a vector space, called the quotient space of π by π. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π = (π /s (π ~QG π)) & β’ (π β π β LVec) & β’ (π β π β (LSubSpβπ)) β β’ (π β π β LVec) | ||
| Theorem | ecxpid 32467 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ (π β π΄ β [π](π΄ Γ π΄) = π΄) | ||
| Theorem | eqg0el 32468 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ βΌ = (πΊ ~QG π») β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ)) β ([π] βΌ = π» β π β π»)) | ||
| Theorem | qsxpid 32469 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| β’ (π΄ β β β (π΄ / (π΄ Γ π΄)) = {π΄}) | ||
| Theorem | qusxpid 32470 | The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β (πΊ ~QG π΅) = (π΅ Γ π΅)) | ||
| Theorem | qustriv 32471 | The quotient of a group πΊ by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π΅)) β β’ (πΊ β Grp β (Baseβπ) = {π΅}) | ||
| Theorem | qustrivr 32472 | Converse of qustriv 32471. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π»)) β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ) β§ (Baseβπ) = {π»}) β π» = π΅) | ||
| Theorem | fermltlchr 32473 | A generalization of Fermat's little theorem in a commutative ring πΉ of prime characteristic. See fermltl 16716. (Contributed by Thierry Arnoux, 9-Jan-2024.) |
| β’ π = (chrβπΉ) & β’ π΅ = (BaseβπΉ) & β’ β = (.gβ(mulGrpβπΉ)) & β’ π΄ = ((β€RHomβπΉ)βπΈ) & β’ (π β π β β) & β’ (π β πΈ β β€) & β’ (π β πΉ β CRing) β β’ (π β (π β π΄) = π΄) | ||
| Theorem | znfermltl 32474 | Fermat's little theorem in β€/nβ€. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβ(mulGrpβπ)) β β’ ((π β β β§ π΄ β π΅) β (π β π΄) = π΄) | ||
| Theorem | islinds5 32475* | A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π΅ = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπΉ) β β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β βπ β (πΎ βm π)((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })))) | ||
| Theorem | ellspds 32476* | Variation on ellspd 21356. (Contributed by Thierry Arnoux, 18-May-2023.) |
| β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β π΅) β β’ (π β (π β (πβπ) β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
| Theorem | 0ellsp 32477 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
| β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π΅) β 0 β (πβπ)) | ||
| Theorem | 0nellinds 32478 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
| β’ 0 = (0gβπ) β β’ ((π β LVec β§ πΉ β (LIndSβπ)) β Β¬ 0 β πΉ) | ||
| Theorem | rspsnel 32479* | Membership in a principal ideal. Analogous to lspsnel 20613. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅) β (πΌ β (πΎβ{π}) β βπ₯ β π΅ πΌ = (π₯ Β· π))) | ||
| Theorem | rspsnid 32480 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβ{πΊ})) | ||
| Theorem | elrsp 32481* | Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| β’ π = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) β β’ (π β (π β (πβπΌ) β βπ β (π΅ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π β πΌ β¦ ((πβπ) Β· π)))))) | ||
| Theorem | rspidlid 32482 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| β’ πΎ = (RSpanβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΎβπΌ) = πΌ) | ||
| Theorem | pidlnz 32483 | A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β 0 ) β (πΎβ{π}) β { 0 }) | ||
| Theorem | dvdsruassoi 32484 | If two elements π and π of a ring π are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ (π β (π Β· π) = π) β β’ (π β (π β₯ π β§ π β₯ π)) | ||
| Theorem | dvdsruasso 32485* | Two elements π and π of a ring π are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β IDomn) β β’ (π β ((π β₯ π β§ π β₯ π) β βπ’ β π (π’ Β· π) = π)) | ||
| Theorem | dvdsrspss 32486 | In a ring, an element π divides π iff the ideal generated by π is a subset of the ideal generated by π (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Ring) β β’ (π β (π β₯ π β (πΎβ{π}) β (πΎβ{π}))) | ||
| Theorem | rspsnasso 32487 | Two elements π and π of a ring π are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Ring) β β’ (π β ((π β₯ π β§ π β₯ π) β (πΎβ{π}) = (πΎβ{π}))) | ||
| Theorem | lbslsp 32488* | Any element of a left module π can be expressed as a linear combination of the elements of a basis π of π. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
| β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β (LBasisβπ)) β β’ (π β (π β π΅ β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
| Theorem | lindssn 32489 | Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
| β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π β π΅ β§ π β 0 ) β {π} β (LIndSβπ)) | ||
| Theorem | lindflbs 32490 | Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023.) |
| β’ π΅ = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β NzRing) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβ1-1βπ΅) β β’ (π β (ran πΉ β (LBasisβπ) β (πΉ LIndF π β§ (πβran πΉ) = π΅))) | ||
| Theorem | islbs5 32491* | An equivalent formulation of the basis predicate in a vector space, using a function πΉ for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ) & β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β NzRing) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβ1-1βπ΅) β β’ (π β (ran πΉ β (LBasisβπ) β (βπ β (πΎ βm πΌ)((π finSupp 0 β§ (π Ξ£g (π βf Β· πΉ)) = π) β π = (πΌ Γ { 0 })) β§ (πβran πΉ) = π΅))) | ||
| Theorem | linds2eq 32492 | Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.) |
| β’ πΉ = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ 0 = (0gβ(Scalarβπ)) & β’ (π β π β LVec) & β’ (π β π΅ β (LIndSβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β πΉ) & β’ (π β πΏ β πΉ) & β’ (π β πΎ β 0 ) & β’ (π β (πΎ Β· π) = (πΏ Β· π)) β β’ (π β (π = π β§ πΎ = πΏ)) | ||
| Theorem | lindfpropd 32493* | Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
| β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΏ))) & β’ (π β (0gβ(ScalarβπΎ)) = (0gβ(ScalarβπΏ))) & β’ ((π β§ (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ))) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) β (BaseβπΎ)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β π β π΄) β β’ (π β (π LIndF πΎ β π LIndF πΏ)) | ||
| Theorem | lindspropd 32494* | Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
| β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΏ))) & β’ (π β (0gβ(ScalarβπΎ)) = (0gβ(ScalarβπΏ))) & β’ ((π β§ (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ))) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) β (BaseβπΎ)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (LIndSβπΎ) = (LIndSβπΏ)) | ||
The sumset (also called the Minkowski sum) of two subsets π΄ and π΅, is defined to be the set of all sums of an element from π΄ with an element from π΅. The sumset operation can be used for both group (additive) operations and ring (multiplicative) operations. | ||
| Theorem | elgrplsmsn 32495* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β πΊ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π΄ β {π}) β βπ₯ β π΄ π = (π₯ + π))) | ||
| Theorem | lsmsnorb 32496* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19170. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π + π₯) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π΄ β {π}) = [π] βΌ ) | ||
| Theorem | lsmsnorb2 32497* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19170. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π₯ + π) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β ({π} β π΄) = [π] βΌ ) | ||
| Theorem | elringlsm 32498* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (π β (πΈ Γ πΉ) β βπ₯ β πΈ βπ¦ β πΉ π = (π₯ Β· π¦))) | ||
| Theorem | elringlsmd 32499 | Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β π β πΈ) & β’ (π β π β πΉ) β β’ (π β (π Β· π) β (πΈ Γ πΉ)) | ||
| Theorem | ringlsmss 32500 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (πΈ Γ πΉ) β π΅) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |