Home | Metamath
Proof Explorer Theorem List (p. 174 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prdsdsval2 17301* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) β β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, < )) | ||
Theorem | prdsdsval3 17302* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ πΎ = (Baseβπ ) & β’ πΈ = ((distβπ ) βΎ (πΎ Γ πΎ)) & β’ π· = (distβπ) β β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, < )) | ||
Theorem | pwsval 17303 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ πΉ = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (πΉXs(πΌ Γ {π }))) | ||
Theorem | pwsbas 17304 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) β β’ ((π β π β§ πΌ β π) β (π΅ βm πΌ) = (Baseβπ)) | ||
Theorem | pwselbasb 17305 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) β β’ ((π β π β§ πΌ β π) β (π β π β π:πΌβΆπ΅)) | ||
Theorem | pwselbas 17306 | An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π:πΌβΆπ΅) | ||
Theorem | pwsplusgval 17307 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf + πΊ)) | ||
Theorem | pwsmulrval 17308 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf Β· πΊ)) | ||
Theorem | pwsle 17309 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ ((π β π β§ πΌ β π) β β€ = ( βr π β© (π΅ Γ π΅))) | ||
Theorem | pwsleval 17310* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)π(πΊβπ₯))) | ||
Theorem | pwsvscafval 17311 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) β β’ (π β (π΄ β π) = ((πΌ Γ {π΄}) βf Β· π)) | ||
Theorem | pwsvscaval 17312 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) & β’ (π β π½ β πΌ) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | pwssca 17313 | The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (Scalarβπ)) | ||
Theorem | pwsdiagel 17314 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (((π β π β§ πΌ β π) β§ π΄ β π΅) β (πΌ Γ {π΄}) β πΆ) | ||
Theorem | pwssnf1o 17315* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {πΌ}) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ ({πΌ} Γ {π₯})) & β’ πΆ = (Baseβπ) β β’ ((π β π β§ πΌ β π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Syntax | cordt 17316 | Extend class notation with the order topology. |
class ordTop | ||
Syntax | cxrs 17317 | Extend class notation with the extended real number structure. |
class β*π | ||
Definition | df-ordt 17318* | Define the order topology, given an order β€, written as π below. A closed subbasis for the order topology is given by the closed rays [π¦, +β) = {π§ β π β£ π¦ β€ π§} and (-β, π¦] = {π§ β π β£ π§ β€ π¦}, along with (-β, +β) = π itself. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ordTop = (π β V β¦ (topGenβ(fiβ({dom π} βͺ ran ((π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π¦ππ₯}) βͺ (π₯ β dom π β¦ {π¦ β dom π β£ Β¬ π₯ππ¦})))))) | ||
Definition | df-xrs 17319* | The extended real number structure. Unlike df-cnfld 20720, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 20720. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because +β is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +β an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with βfld when restricted to β. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ β*π = ({β¨(Baseβndx), β*β©, β¨(+gβndx), +π β©, β¨(.rβndx), Β·e β©} βͺ {β¨(TopSetβndx), (ordTopβ β€ )β©, β¨(leβndx), β€ β©, β¨(distβndx), (π₯ β β*, π¦ β β* β¦ if(π₯ β€ π¦, (π¦ +π -ππ₯), (π₯ +π -ππ¦)))β©}) | ||
Syntax | cqtop 17320 | Extend class notation with the quotient topology function. |
class qTop | ||
Syntax | cimas 17321 | Image structure function. |
class βs | ||
Syntax | cqus 17322 | Quotient structure function. |
class /s | ||
Syntax | cxps 17323 | Binary product structure function. |
class Γs | ||
Definition | df-qtop 17324* | Define the quotient topology given a function π and topology π on the domain of π. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ qTop = (π β V, π β V β¦ {π β π« (π β βͺ π) β£ ((β‘π β π ) β© βͺ π) β π}) | ||
Definition | df-imas 17325* |
Define an image structure, which takes a structure and a function on the
base set, and maps all the operations via the function. For this to
work properly π must either be injective or satisfy
the
well-definedness condition π(π) = π(π) β§ π(π) = π(π) β
π(π + π) = π(π + π) for each relevant operation.
Note that although we call this an "image" by association to df-ima 5644, in order to keep the definition simple we consider only the case when the domain of πΉ is equal to the base set of π . Other cases can be achieved by restricting πΉ (with df-res 5643) and/or π ( with df-ress 17048) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.) |
β’ βs = (π β V, π β V β¦ β¦(Baseβπ) / π£β¦(({β¨(Baseβndx), ran πβ©, β¨(+gβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(+gβπ)π))β©}β©, β¨(.rβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(.rβπ)π))β©}β©} βͺ {β¨(Scalarβndx), (Scalarβπ)β©, β¨( Β·π βndx), βͺ π β π£ (π β (Baseβ(Scalarβπ)), π₯ β {(πβπ)} β¦ (πβ(π( Β·π βπ)π)))β©, β¨(Β·πβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (π(Β·πβπ)π)β©}β©}) βͺ {β¨(TopSetβndx), ((TopOpenβπ) qTop π)β©, β¨(leβndx), ((π β (leβπ)) β β‘π)β©, β¨(distβndx), (π₯ β ran π, π¦ β ran π β¦ inf(βͺ π β β ran (π β {β β ((π£ Γ π£) βm (1...π)) β£ ((πβ(1st β(ββ1))) = π₯ β§ (πβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πβ(2nd β(ββπ))) = (πβ(1st β(ββ(π + 1)))))} β¦ (β*π Ξ£g ((distβπ) β π))), β*, < ))β©})) | ||
Definition | df-qus 17326* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 17325 where the image function is π₯ β¦ [π₯]π. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) | ||
Definition | df-xps 17327* | Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
β’ Γs = (π β V, π β V β¦ (β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β , π₯β©, β¨1o, π¦β©}) βs ((Scalarβπ)Xs{β¨β , πβ©, β¨1o, π β©}))) | ||
Theorem | imasval 17328* | Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ , = (Β·πβπ ) & β’ π½ = (TopOpenβπ ) & β’ πΈ = (distβπ ) & β’ π = (leβπ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Γ π))β©}) & β’ (π β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) & β’ (π β πΌ = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π , π)β©}) & β’ (π β π = (π½ qTop πΉ)) & β’ (π β π· = (π₯ β π΅, π¦ β π΅ β¦ inf(βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦ (β*π Ξ£g (πΈ β π))), β*, < ))) & β’ (π β β€ = ((πΉ β π) β β‘πΉ)) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) β β’ (π β π = (({β¨(Baseβndx), π΅β©, β¨(+gβndx), β β©, β¨(.rβndx), β β©} βͺ {β¨(Scalarβndx), πΊβ©, β¨( Β·π βndx), β β©, β¨(Β·πβndx), πΌβ©}) βͺ {β¨(TopSetβndx), πβ©, β¨(leβndx), β€ β©, β¨(distβndx), π·β©})) | ||
Theorem | imasbas 17329 | The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | imasds 17330* | The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) β β’ (π β π· = (π₯ β π΅, π¦ β π΅ β¦ inf(βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦ (β*π Ξ£g (πΈ β π))), β*, < ))) | ||
Theorem | imasdsfn 17331 | The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) β β’ (π β π· Fn (π΅ Γ π΅)) | ||
Theorem | imasdsval 17332* | The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π β§ (πΉβ(2nd β(ββπ))) = π β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β β’ (π β (ππ·π) = inf(βͺ π β β ran (π β π β¦ (β*π Ξ£g (πΈ β π))), β*, < )) | ||
Theorem | imasdsval2 17333* | The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π β§ (πΉβ(2nd β(ββπ))) = π β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} & β’ π = (πΈ βΎ (π Γ π)) β β’ (π β (ππ·π) = inf(βͺ π β β ran (π β π β¦ (β*π Ξ£g (π β π))), β*, < )) | ||
Theorem | imasplusg 17334* | The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) | ||
Theorem | imasmulr 17335* | The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) | ||
Theorem | imassca 17336 | The scalar field of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) β β’ (π β πΊ = (Scalarβπ)) | ||
Theorem | imasvsca 17337* | The scalar multiplication operation of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) β β’ (π β β = βͺ π β π (π β πΎ, π₯ β {(πΉβπ)} β¦ (πΉβ(π Β· π)))) | ||
Theorem | imasip 17338* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ , = (Β·πβπ ) & β’ πΌ = (Β·πβπ) β β’ (π β πΌ = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π , π)β©}) | ||
Theorem | imastset 17339 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π½ = (TopOpenβπ ) & β’ π = (TopSetβπ) β β’ (π β π = (π½ qTop πΉ)) | ||
Theorem | imasle 17340 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ (π β β€ = ((πΉ β π) β β‘πΉ)) | ||
Theorem | f1ocpbllem 17341 | Lemma for f1ocpbl 17342. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | f1ocpbl 17342 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 17343 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 17344 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlem 17345* | 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 17346* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflem 17347* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 17348* | 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 17349* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 17350* | 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 17351* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 17352* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 17353* | 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 17354* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ (π β β Fn (πΎ Γ π΅)) | ||
Theorem | imasvscaval 17355* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasvscaf 17356* | 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 17357 | 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 17358* | 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 17359* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 17360* | The function in qusval 17359 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 17361 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 17362 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | quss 17363 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ πΎ = (Scalarβπ ) β β’ (π β πΎ = (Scalarβπ)) | ||
Theorem | divsfval 17364* | Value of the function in qusval 17359. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllem 17365* | Lemma for ercpbl 17366. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 17366* | 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 17367* | 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 17368* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddflem 17369* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusaddval 17370* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddf 17371* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusmulval 17372* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusmulf 17373* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | fnpr2o 17374 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fnpr2ob 17375 | Biconditional version of fnpr2o 17374. (Contributed by Jim Kingdon, 27-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fvpr0o 17376 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΄ β π β ({β¨β , π΄β©, β¨1o, π΅β©}ββ ) = π΄) | ||
Theorem | fvpr1o 17377 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΅ β π β ({β¨β , π΄β©, β¨1o, π΅β©}β1o) = π΅) | ||
Theorem | fvprif 17378 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β 2o) β ({β¨β , π΄β©, β¨1o, π΅β©}βπΆ) = if(πΆ = β , π΄, π΅)) | ||
Theorem | xpsfrnel 17379* | Elementhood in the target space of the function πΉ appearing in xpsval 17387. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (πΊ β Xπ β 2o if(π = β , π΄, π΅) β (πΊ Fn 2o β§ (πΊββ ) β π΄ β§ (πΊβ1o) β π΅)) | ||
Theorem | xpsfeq 17380 | 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 17381* | Elementhood in the target space of the function πΉ appearing in xpsval 17387. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©} β Xπ β 2o if(π = β , π΄, π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | xpscf 17382 | Equivalent condition for the pair function to be a proper function on π΄. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©}:2oβΆπ΄ β (π β π΄ β§ π β π΄)) | ||
Theorem | xpsfval 17383* | The value of the function appearing in xpsval 17387. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ((π β π΄ β§ π β π΅) β (ππΉπ) = {β¨β , πβ©, β¨1o, πβ©}) | ||
Theorem | xpsff1o 17384* | The function appearing in xpsval 17387 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 17385* | 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 17386* | The function appearing in xpsval 17387 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 17387* | 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 17388* | The indexed structure product that appears in xpsval 17387 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 17389 | The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π Γ π) = (Baseβπ)) | ||
Theorem | xpsaddlem 17390* | Lemma for xpsadd 17391 and xpsmul 17392. (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 17391 | 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 17392 | 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 17393 | 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 17394 | 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 17395 | Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ β€ = (leβπ) β β’ (π β β€ β ((π Γ π) Γ (π Γ π))) | ||
Theorem | xpsle 17396 | Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ β€ = (leβπ) & β’ π = (leβπ ) & β’ π = (leβπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β© β€ β¨πΆ, π·β© β (π΄ππΆ β§ π΅ππ·))) | ||
Syntax | cmre 17397 | The class of Moore systems. |
class Moore | ||
Syntax | cmrc 17398 | The class function generating Moore closures. |
class mrCls | ||
Syntax | cmri 17399 | mrInd is a class function which takes a Moore system to its set of independent sets. |
class mrInd | ||
Syntax | cacs 17400 | The class of algebraic closure (Moore) systems. |
class ACS |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |