![]() |
Metamath
Proof Explorer Theorem List (p. 175 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prdssca 17401 | Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (Scalarβπ)) | ||
Theorem | prdsbas 17402* | Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) β β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π βπ₯))) | ||
Theorem | prdsplusg 17403* | Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ + = (+gβπ) β β’ (π β + = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π βπ₯))(πβπ₯))))) | ||
Theorem | prdsmulr 17404* | Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ Β· = (.rβπ) β β’ (π β Β· = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π βπ₯))(πβπ₯))))) | ||
Theorem | prdsvsca 17405* | Scalar multiplication in a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) β β’ (π β Β· = (π β πΎ, π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π β(π βπ₯))(πβπ₯))))) | ||
Theorem | prdsip 17406* | Inner product in a structure product. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ , = (Β·πβπ) β β’ (π β , = (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π βπ₯))(πβπ₯)))))) | ||
Theorem | prdsle 17407* | Structure product weak ordering. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ β€ = (leβπ) β β’ (π β β€ = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π βπ₯))(πβπ₯))}) | ||
Theorem | prdsless 17408 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ β€ = (leβπ) β β’ (π β β€ β (π΅ Γ π΅)) | ||
Theorem | prdsds 17409* | Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π· = (distβπ) β β’ (π β π· = (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π βπ₯))(πβπ₯))) βͺ {0}), β*, < ))) | ||
Theorem | prdsdsfn 17410 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π· = (distβπ) β β’ (π β π· Fn (π΅ Γ π΅)) | ||
Theorem | prdstset 17411 | Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π = (TopSetβπ) β β’ (π β π = (βtβ(TopOpen β π ))) | ||
Theorem | prdshom 17412* | Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π» = (Hom βπ) β β’ (π β π» = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π βπ₯))(πβπ₯)))) | ||
Theorem | prdsco 17413* | Structure product composition operation. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π» = (Hom βπ) & β’ β = (compβπ) β β’ (π β β = (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)π»π), π β (π»βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π βπ₯))(πβπ₯))(πβπ₯)))))) | ||
Theorem | prdsbas2 17414* | The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) β β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π βπ₯))) | ||
Theorem | prdsbasmpt 17415* | A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) β β’ (π β ((π₯ β πΌ β¦ π) β π΅ β βπ₯ β πΌ π β (Baseβ(π βπ₯)))) | ||
Theorem | prdsbasfn 17416 | Points in the structure product are functions; use this with dffn5 6950 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β π β π΅) β β’ (π β π Fn πΌ) | ||
Theorem | prdsbasprj 17417 | Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β π β π΅) & β’ (π β π½ β πΌ) β β’ (π β (πβπ½) β (Baseβ(π βπ½))) | ||
Theorem | prdsplusgval 17418* | Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ + = (+gβπ) β β’ (π β (πΉ + πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯)(+gβ(π βπ₯))(πΊβπ₯)))) | ||
Theorem | prdsplusgfval 17419 | Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ + = (+gβπ) & β’ (π β π½ β πΌ) β β’ (π β ((πΉ + πΊ)βπ½) = ((πΉβπ½)(+gβ(π βπ½))(πΊβπ½))) | ||
Theorem | prdsmulrval 17420* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ) β β’ (π β (πΉ Β· πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯)(.rβ(π βπ₯))(πΊβπ₯)))) | ||
Theorem | prdsmulrfval 17421 | Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ) & β’ (π β π½ β πΌ) β β’ (π β ((πΉ Β· πΊ)βπ½) = ((πΉβπ½)(.rβ(π βπ½))(πΊβπ½))) | ||
Theorem | prdsleval 17422* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ β€ = (leβπ) β β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)(leβ(π βπ₯))(πΊβπ₯))) | ||
Theorem | prdsdsval 17423* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ π· = (distβπ) β β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)(distβ(π βπ₯))(πΊβπ₯))) βͺ {0}), β*, < )) | ||
Theorem | prdsvscaval 17424* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (πΉ Β· πΊ) = (π₯ β πΌ β¦ (πΉ( Β·π β(π βπ₯))(πΊβπ₯)))) | ||
Theorem | prdsvscafval 17425 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) & β’ (π β π½ β πΌ) β β’ (π β ((πΉ Β· πΊ)βπ½) = (πΉ( Β·π β(π βπ½))(πΊβπ½))) | ||
Theorem | prdsbas3 17426* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ πΎ = (Baseβπ ) β β’ (π β π΅ = Xπ₯ β πΌ πΎ) | ||
Theorem | prdsbasmpt2 17427* | A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ πΎ = (Baseβπ ) β β’ (π β ((π₯ β πΌ β¦ π) β π΅ β βπ₯ β πΌ π β πΎ)) | ||
Theorem | prdsbascl 17428* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ πΎ = (Baseβπ ) & β’ (π β πΉ β π΅) β β’ (π β βπ₯ β πΌ (πΉβπ₯) β πΎ) | ||
Theorem | prdsdsval2 17429* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) β β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, < )) | ||
Theorem | prdsdsval3 17430* | 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 17431 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ πΉ = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (πΉXs(πΌ Γ {π }))) | ||
Theorem | pwsbas 17432 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) β β’ ((π β π β§ πΌ β π) β (π΅ βm πΌ) = (Baseβπ)) | ||
Theorem | pwselbasb 17433 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) β β’ ((π β π β§ πΌ β π) β (π β π β π:πΌβΆπ΅)) | ||
Theorem | pwselbas 17434 | 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 17435 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf + πΊ)) | ||
Theorem | pwsmulrval 17436 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf Β· πΊ)) | ||
Theorem | pwsle 17437 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ ((π β π β§ πΌ β π) β β€ = ( βr π β© (π΅ Γ π΅))) | ||
Theorem | pwsleval 17438* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)π(πΊβπ₯))) | ||
Theorem | pwsvscafval 17439 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) β β’ (π β (π΄ β π) = ((πΌ Γ {π΄}) βf Β· π)) | ||
Theorem | pwsvscaval 17440 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) & β’ (π β π½ β πΌ) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | pwssca 17441 | The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (Scalarβπ)) | ||
Theorem | pwsdiagel 17442 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (((π β π β§ πΌ β π) β§ π΄ β π΅) β (πΌ Γ {π΄}) β πΆ) | ||
Theorem | pwssnf1o 17443* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {πΌ}) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ ({πΌ} Γ {π₯})) & β’ πΆ = (Baseβπ) β β’ ((π β π β§ πΌ β π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Syntax | cordt 17444 | Extend class notation with the order topology. |
class ordTop | ||
Syntax | cxrs 17445 | Extend class notation with the extended real number structure. |
class β*π | ||
Definition | df-ordt 17446* | 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 17447* | The extended real number structure. Unlike df-cnfld 20944, 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 20944. 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 17448 | Extend class notation with the quotient topology function. |
class qTop | ||
Syntax | cimas 17449 | Image structure function. |
class βs | ||
Syntax | cqus 17450 | Quotient structure function. |
class /s | ||
Syntax | cxps 17451 | Binary product structure function. |
class Γs | ||
Definition | df-qtop 17452* | 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 17453* |
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 5689, 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 5688) and/or π ( with df-ress 17173) 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 17454* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 17453 where the image function is π₯ β¦ [π₯]π. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) | ||
Definition | df-xps 17455* | 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 17456* | 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 17457 | 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 17458* | 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 17459 | 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 17460* | 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 17461* | 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 17462* | 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 17463* | 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 17464 | 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 17465* | 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 17466* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ , = (Β·πβπ ) & β’ πΌ = (Β·πβπ) β β’ (π β πΌ = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π , π)β©}) | ||
Theorem | imastset 17467 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π½ = (TopOpenβπ ) & β’ π = (TopSetβπ) β β’ (π β π = (π½ qTop πΉ)) | ||
Theorem | imasle 17468 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ (π β β€ = ((πΉ β π) β β‘πΉ)) | ||
Theorem | f1ocpbllem 17469 | Lemma for f1ocpbl 17470. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | f1ocpbl 17470 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 17471 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 17472 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlem 17473* | 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 17474* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflem 17475* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 17476* | 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 17477* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 17478* | 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 17479* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 17480* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 17481* | 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 17482* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ (π β β Fn (πΎ Γ π΅)) | ||
Theorem | imasvscaval 17483* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasvscaf 17484* | 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 17485 | 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 17486* | 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 17487* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 17488* | The function in qusval 17487 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 17489 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 17490 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | quss 17491 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ πΎ = (Scalarβπ ) β β’ (π β πΎ = (Scalarβπ)) | ||
Theorem | divsfval 17492* | Value of the function in qusval 17487. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllem 17493* | Lemma for ercpbl 17494. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 17494* | 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 17495* | 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 17496* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddflem 17497* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusaddval 17498* | The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddf 17499* | The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusmulval 17500* | The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |