![]() |
Metamath
Proof Explorer Theorem List (p. 176 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 | f1ocpbl 17501 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 17502 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 17503 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlem 17504* | The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasaddvallem 17505* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflem 17506* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 17507* | The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasaddval 17508* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 17509* | The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasmulfn 17510* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 17511* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 17512* | The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasvscafn 17513* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ (π β β Fn (πΎ Γ π΅)) | ||
Theorem | imasvscaval 17514* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasvscaf 17515* | The image structure's scalar multiplication is closed in the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ ((π β§ (π β πΎ β§ π β π)) β (π Β· π) β π) β β’ (π β β :(πΎ Γ π΅)βΆπ΅) | ||
Theorem | imasless 17516 | The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ β€ = (leβπ) β β’ (π β β€ β (π΅ Γ π΅)) | ||
Theorem | imasleval 17517* | The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ β€ = (leβπ) & β’ π = (leβπ ) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ))) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β€ (πΉβπ) β πππ)) | ||
Theorem | qusval 17518* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 17519* | The function in qusval 17518 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 17520 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 17521 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | quss 17522 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ πΎ = (Scalarβπ ) β β’ (π β πΎ = (Scalarβπ)) | ||
Theorem | divsfval 17523* | Value of the function in qusval 17518. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllem 17524* | Lemma for ercpbl 17525. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 17525* | Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ ((π β§ (π β π β§ π β π)) β (π + π) β π) & β’ (π β ((π΄ βΌ πΆ β§ π΅ βΌ π·) β (π΄ + π΅) βΌ (πΆ + π·))) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | erlecpbl 17526* | Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β ((π΄ βΌ πΆ β§ π΅ βΌ π·) β (π΄ππ΅ β πΆππ·))) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | qusaddvallem 17527* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddflem 17528* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusaddval 17529* | The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddf 17530* | The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusmulval 17531* | The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusmulf 17532* | The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | fnpr2o 17533 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fnpr2ob 17534 | Biconditional version of fnpr2o 17533. (Contributed by Jim Kingdon, 27-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fvpr0o 17535 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΄ β π β ({β¨β , π΄β©, β¨1o, π΅β©}ββ ) = π΄) | ||
Theorem | fvpr1o 17536 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΅ β π β ({β¨β , π΄β©, β¨1o, π΅β©}β1o) = π΅) | ||
Theorem | fvprif 17537 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β 2o) β ({β¨β , π΄β©, β¨1o, π΅β©}βπΆ) = if(πΆ = β , π΄, π΅)) | ||
Theorem | xpsfrnel 17538* | Elementhood in the target space of the function πΉ appearing in xpsval 17546. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (πΊ β Xπ β 2o if(π = β , π΄, π΅) β (πΊ Fn 2o β§ (πΊββ ) β π΄ β§ (πΊβ1o) β π΅)) | ||
Theorem | xpsfeq 17539 | A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (πΊ Fn 2o β {β¨β , (πΊββ )β©, β¨1o, (πΊβ1o)β©} = πΊ) | ||
Theorem | xpsfrnel2 17540* | Elementhood in the target space of the function πΉ appearing in xpsval 17546. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©} β Xπ β 2o if(π = β , π΄, π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | xpscf 17541 | Equivalent condition for the pair function to be a proper function on π΄. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©}:2oβΆπ΄ β (π β π΄ β§ π β π΄)) | ||
Theorem | xpsfval 17542* | The value of the function appearing in xpsval 17546. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ((π β π΄ β§ π β π΅) β (ππΉπ) = {β¨β , πβ©, β¨1o, πβ©}) | ||
Theorem | xpsff1o 17543* | The function appearing in xpsval 17546 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {β , 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ πΉ:(π΄ Γ π΅)β1-1-ontoβXπ β 2o if(π = β , π΄, π΅) | ||
Theorem | xpsfrn 17544* | A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ran πΉ = Xπ β 2o if(π = β , π΄, π΅) | ||
Theorem | xpsff1o2 17545* | The function appearing in xpsval 17546 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {β , 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ πΉ:(π΄ Γ π΅)β1-1-ontoβran πΉ | ||
Theorem | xpsval 17546* | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β , π₯β©, β¨1o, π¦β©}) & β’ πΊ = (Scalarβπ ) & β’ π = (πΊXs{β¨β , π β©, β¨1o, πβ©}) β β’ (π β π = (β‘πΉ βs π)) | ||
Theorem | xpsrnbas 17547* | The indexed structure product that appears in xpsval 17546 has the same base as the target of the function πΉ. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β , π₯β©, β¨1o, π¦β©}) & β’ πΊ = (Scalarβπ ) & β’ π = (πΊXs{β¨β , π β©, β¨1o, πβ©}) β β’ (π β ran πΉ = (Baseβπ)) | ||
Theorem | xpsbas 17548 | The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π Γ π) = (Baseβπ)) | ||
Theorem | xpsaddlem 17549* | Lemma for xpsadd 17550 and xpsmul 17551. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ Β· πΆ) β π) & β’ (π β (π΅ Γ π·) β π) & β’ Β· = (πΈβπ ) & β’ Γ = (πΈβπ) & β’ β = (πΈβπ) & β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β , π₯β©, β¨1o, π¦β©}) & β’ π = ((Scalarβπ )Xs{β¨β , π β©, β¨1o, πβ©}) & β’ ((π β§ {β¨β , π΄β©, β¨1o, π΅β©} β ran πΉ β§ {β¨β , πΆβ©, β¨1o, π·β©} β ran πΉ) β ((β‘πΉβ{β¨β , π΄β©, β¨1o, π΅β©}) β (β‘πΉβ{β¨β , πΆβ©, β¨1o, π·β©})) = (β‘πΉβ({β¨β , π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β , πΆβ©, β¨1o, π·β©}))) & β’ (({β¨β , π β©, β¨1o, πβ©} Fn 2o β§ {β¨β , π΄β©, β¨1o, π΅β©} β (Baseβπ) β§ {β¨β , πΆβ©, β¨1o, π·β©} β (Baseβπ)) β ({β¨β , π΄β©, β¨1o, π΅β©} (πΈβπ){β¨β , πΆβ©, β¨1o, π·β©}) = (π β 2o β¦ (({β¨β , π΄β©, β¨1o, π΅β©}βπ)(πΈβ({β¨β , π β©, β¨1o, πβ©}βπ))({β¨β , πΆβ©, β¨1o, π·β©}βπ)))) β β’ (π β (β¨π΄, π΅β© β β¨πΆ, π·β©) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) | ||
Theorem | xpsadd 17550 | Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ Β· πΆ) β π) & β’ (π β (π΅ Γ π·) β π) & β’ Β· = (+gβπ ) & β’ Γ = (+gβπ) & β’ β = (+gβπ) β β’ (π β (β¨π΄, π΅β© β β¨πΆ, π·β©) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) | ||
Theorem | xpsmul 17551 | Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β (π΄ Β· πΆ) β π) & β’ (π β (π΅ Γ π·) β π) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ β = (.rβπ) β β’ (π β (β¨π΄, π΅β© β β¨πΆ, π·β©) = β¨(π΄ Β· πΆ), (π΅ Γ π·)β©) | ||
Theorem | xpssca 17552 | Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ πΊ = (Scalarβπ ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β πΊ = (Scalarβπ)) | ||
Theorem | xpsvsca 17553 | Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ πΊ = (Scalarβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ Γ = ( Β·π βπ) & β’ β = ( Β·π βπ) & β’ (π β π΄ β πΎ) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π΄ Β· π΅) β π) & β’ (π β (π΄ Γ πΆ) β π) β β’ (π β (π΄ β β¨π΅, πΆβ©) = β¨(π΄ Β· π΅), (π΄ Γ πΆ)β©) | ||
Theorem | xpsless 17554 | Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ β€ = (leβπ) β β’ (π β β€ β ((π Γ π) Γ (π Γ π))) | ||
Theorem | xpsle 17555 | Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ β€ = (leβπ) & β’ π = (leβπ ) & β’ π = (leβπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β© β€ β¨πΆ, π·β© β (π΄ππΆ β§ π΅ππ·))) | ||
Syntax | cmre 17556 | The class of Moore systems. |
class Moore | ||
Syntax | cmrc 17557 | The class function generating Moore closures. |
class mrCls | ||
Syntax | cmri 17558 | mrInd is a class function which takes a Moore system to its set of independent sets. |
class mrInd | ||
Syntax | cacs 17559 | The class of algebraic closure (Moore) systems. |
class ACS | ||
Definition | df-mre 17560* |
Define a Moore collection, which is a family of subsets of a base set
which preserve arbitrary intersection. Elements of a Moore collection
are termed closed; Moore collections generalize the notion of
closedness from topologies (cldmre 22995) and vector spaces (lssmre 20849)
to the most general setting in which such concepts make sense.
Definition of Moore collection of sets in [Schechter] p. 78. A Moore
collection may also be called a closure system (Section 0.6 in
[Gratzer] p. 23.) The name Moore
collection is after Eliakim Hastings
Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.
See ismre 17564, mresspw 17566, mre1cl 17568 and mreintcl 17569 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17574); as such the disjoint union of all Moore collections is sometimes considered as βͺ ran Moore, justified by mreunirn 17575. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
β’ Moore = (π₯ β V β¦ {π β π« π« π₯ β£ (π₯ β π β§ βπ β π« π(π β β β β© π β π))}) | ||
Definition | df-mrc 17561* |
Define the Moore closure of a generating set, which is the smallest
closed set containing all generating elements. Definition of Moore
closure in [Schechter] p. 79. This
generalizes topological closure
(mrccls 22996) and linear span (mrclsp 20872).
A Moore closure operation π is (1) extensive, i.e., π₯ β (πβπ₯) for all subsets π₯ of the base set (mrcssid 17591), (2) isotone, i.e., π₯ β π¦ implies that (πβπ₯) β (πβπ¦) for all subsets π₯ and π¦ of the base set (mrcss 17590), and (3) idempotent, i.e., (πβ(πβπ₯)) = (πβπ₯) for all subsets π₯ of the base set (mrcidm 17593.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation π on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
β’ mrCls = (π β βͺ ran Moore β¦ (π₯ β π« βͺ π β¦ β© {π β π β£ π₯ β π })) | ||
Definition | df-mri 17562* | In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.) |
β’ mrInd = (π β βͺ ran Moore β¦ {π β π« βͺ π β£ βπ₯ β π Β¬ π₯ β ((mrClsβπ)β(π β {π₯}))}) | ||
Definition | df-acs 17563* | An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 9661 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ACS = (π₯ β V β¦ {π β (Mooreβπ₯) β£ βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π ))}) | ||
Theorem | ismre 17564* | Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΆ β (Mooreβπ) β (πΆ β π« π β§ π β πΆ β§ βπ β π« πΆ(π β β β β© π β πΆ))) | ||
Theorem | fnmre 17565 | The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22839 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ Moore Fn V | ||
Theorem | mresspw 17566 | A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΆ β (Mooreβπ) β πΆ β π« π) | ||
Theorem | mress 17567 | A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β π β π) | ||
Theorem | mre1cl 17568 | In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΆ β (Mooreβπ) β π β πΆ) | ||
Theorem | mreintcl 17569 | A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ ((πΆ β (Mooreβπ) β§ π β πΆ β§ π β β ) β β© π β πΆ) | ||
Theorem | mreiincl 17570* | A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ ((πΆ β (Mooreβπ) β§ πΌ β β β§ βπ¦ β πΌ π β πΆ) β β© π¦ β πΌ π β πΆ) | ||
Theorem | mrerintcl 17571 | The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (π β© β© π) β πΆ) | ||
Theorem | mreriincl 17572* | The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ ((πΆ β (Mooreβπ) β§ βπ¦ β πΌ π β πΆ) β (π β© β© π¦ β πΌ π) β πΆ) | ||
Theorem | mreincl 17573 | Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ ((πΆ β (Mooreβπ) β§ π΄ β πΆ β§ π΅ β πΆ) β (π΄ β© π΅) β πΆ) | ||
Theorem | mreuni 17574 | Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΆ β (Mooreβπ) β βͺ πΆ = π) | ||
Theorem | mreunirn 17575 | Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (πΆ β βͺ ran Moore β πΆ β (Mooreββͺ πΆ)) | ||
Theorem | ismred 17576* | Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (π β πΆ β π« π) & β’ (π β π β πΆ) & β’ ((π β§ π β πΆ β§ π β β ) β β© π β πΆ) β β’ (π β πΆ β (Mooreβπ)) | ||
Theorem | ismred2 17577* | Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
β’ (π β πΆ β π« π) & β’ ((π β§ π β πΆ) β (π β© β© π ) β πΆ) β β’ (π β πΆ β (Mooreβπ)) | ||
Theorem | mremre 17578 | The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ (π β π β (Mooreβπ) β (Mooreβπ« π)) | ||
Theorem | submre 17579 | The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
β’ ((πΆ β (Mooreβπ) β§ π΄ β πΆ) β (πΆ β© π« π΄) β (Mooreβπ΄)) | ||
Theorem | mrcflem 17580* | The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ (πΆ β (Mooreβπ) β (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π }):π« πβΆπΆ) | ||
Theorem | fnmrc 17581 | Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ mrCls Fn βͺ ran Moore | ||
Theorem | mrcfval 17582* | Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) | ||
Theorem | mrcf 17583 | The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) | ||
Theorem | mrcval 17584* | Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβπ) = β© {π β πΆ β£ π β π }) | ||
Theorem | mrccl 17585 | The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβπ) β πΆ) | ||
Theorem | mrcsncl 17586 | The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβ{π}) β πΆ) | ||
Theorem | mrcid 17587 | The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (πΉβπ) = π) | ||
Theorem | mrcssv 17588 | The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β (πΉβπ) β π) | ||
Theorem | mrcidb 17589 | A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β (π β πΆ β (πΉβπ) = π)) | ||
Theorem | mrcss 17590 | Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉβπ) β (πΉβπ)) | ||
Theorem | mrcssid 17591 | The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β π β (πΉβπ)) | ||
Theorem | mrcidb2 17592 | A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β (π β πΆ β (πΉβπ) β π)) | ||
Theorem | mrcidm 17593 | The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβ(πΉβπ)) = (πΉβπ)) | ||
Theorem | mrcsscl 17594 | The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β π) | ||
Theorem | mrcuni 17595 | Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ π) = (πΉββͺ (πΉ β π))) | ||
Theorem | mrcun 17596 | Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉβ(π βͺ π)) = (πΉβ((πΉβπ) βͺ (πΉβπ)))) | ||
Theorem | mrcssvd 17597 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17588. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (Mooreβπ)) & β’ π = (mrClsβπ΄) β β’ (π β (πβπ΅) β π) | ||
Theorem | mrcssd 17598 | Moore closure preserves subset ordering. Deduction form of mrcss 17590. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (Mooreβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβπ) β (πβπ)) | ||
Theorem | mrcssidd 17599 | A set is contained in its Moore closure. Deduction form of mrcssid 17591. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (Mooreβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β π β (πβπ)) | ||
Theorem | mrcidmd 17600 | Moore closure is idempotent. Deduction form of mrcidm 17593. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (Mooreβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β (πβ(πβπ)) = (πβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |