![]() |
Metamath
Proof Explorer Theorem List (p. 175 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasvalstr 17401 | An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ π = (({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©}) βͺ {β¨(TopSetβndx), πβ©, β¨(leβndx), πΏβ©, β¨(distβndx), π·β©}) β β’ π Struct β¨1, ;12β© | ||
Theorem | prdsvalstr 17402 | Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©}) βͺ ({β¨(TopSetβndx), πβ©, β¨(leβndx), πΏβ©, β¨(distβndx), π·β©} βͺ {β¨(Hom βndx), π»β©, β¨(compβndx), β β©})) Struct β¨1, ;15β© | ||
Theorem | prdsbaslem 17403 | Lemma for prdsbas 17407 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 12-Jul-2024.) |
β’ (π β π = (({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©}) βͺ ({β¨(TopSetβndx), πβ©, β¨(leβndx), πΏβ©, β¨(distβndx), π·β©} βͺ {β¨(Hom βndx), π»β©, β¨(compβndx), β β©}))) & β’ π΄ = (πΈβπ) & β’ πΈ = Slot (πΈβndx) & β’ (π β π β π) & β’ {β¨(πΈβndx), πβ©} β (({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©}) βͺ ({β¨(TopSetβndx), πβ©, β¨(leβndx), πΏβ©, β¨(distβndx), π·β©} βͺ {β¨(Hom βndx), π»β©, β¨(compβndx), β β©})) β β’ (π β π΄ = π) | ||
Theorem | prdsvallem 17404* | Lemma for prdsval 17405. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 17405, dependency on df-hom 17225 removed. (Revised by AV, 13-Oct-2024.) |
β’ (π β π£, π β π£ β¦ Xπ₯ β dom π((πβπ₯)(Hom β(πβπ₯))(πβπ₯))) β V | ||
Theorem | prdsval 17405* | Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
β’ π = (πXsπ ) & β’ πΎ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π βπ₯))) & β’ (π β + = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π βπ₯))(πβπ₯))))) & β’ (π β Γ = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π βπ₯))(πβπ₯))))) & β’ (π β Β· = (π β πΎ, π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π β(π βπ₯))(πβπ₯))))) & β’ (π β , = (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π βπ₯))(πβπ₯)))))) & β’ (π β π = (βtβ(TopOpen β π ))) & β’ (π β β€ = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π βπ₯))(πβπ₯))}) & β’ (π β π· = (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π βπ₯))(πβπ₯))) βͺ {0}), β*, < ))) & β’ (π β π» = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π βπ₯))(πβπ₯)))) & β’ (π β β = (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)π»π), π β (π»βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π βπ₯))(πβπ₯))(πβπ₯)))))) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©}) βͺ ({β¨(TopSetβndx), πβ©, β¨(leβndx), β€ β©, β¨(distβndx), π·β©} βͺ {β¨(Hom βndx), π»β©, β¨(compβndx), β β©}))) | ||
Theorem | prdssca 17406 | 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 17407* | 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 17408* | 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 17409* | 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 17410* | 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 17411* | 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 17412* | 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 17413 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ β€ = (leβπ) β β’ (π β β€ β (π΅ Γ π΅)) | ||
Theorem | prdsds 17414* | 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 17415 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ π΅ = (Baseβπ) & β’ (π β dom π = πΌ) & β’ π· = (distβπ) β β’ (π β π· Fn (π΅ Γ π΅)) | ||
Theorem | prdstset 17416 | 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 17417* | 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 17418* | 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 17419* | 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 17420* | 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 17421 | Points in the structure product are functions; use this with dffn5 6949 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β π β π΅) β β’ (π β π Fn πΌ) | ||
Theorem | prdsbasprj 17422 | 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 17423* | 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 17424 | 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 17425* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ) β β’ (π β (πΉ Β· πΊ) = (π₯ β πΌ β¦ ((πΉβπ₯)(.rβ(π βπ₯))(πΊβπ₯)))) | ||
Theorem | prdsmulrfval 17426 | 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 17427* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ β€ = (leβπ) β β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)(leβ(π βπ₯))(πΊβπ₯))) | ||
Theorem | prdsdsval 17428* | 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 17429* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (πΉ Β· πΊ) = (π₯ β πΌ β¦ (πΉ( Β·π β(π βπ₯))(πΊβπ₯)))) | ||
Theorem | prdsvscafval 17430 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) & β’ (π β π½ β πΌ) β β’ (π β ((πΉ Β· πΊ)βπ½) = (πΉ( Β·π β(π βπ½))(πΊβπ½))) | ||
Theorem | prdsbas3 17431* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ πΎ = (Baseβπ ) β β’ (π β π΅ = Xπ₯ β πΌ πΎ) | ||
Theorem | prdsbasmpt2 17432* | 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 17433* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ πΎ = (Baseβπ ) & β’ (π β πΉ β π΅) β β’ (π β βπ₯ β πΌ (πΉβπ₯) β πΎ) | ||
Theorem | prdsdsval2 17434* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β βπ₯ β πΌ π β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ πΈ = (distβπ ) & β’ π· = (distβπ) β β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, < )) | ||
Theorem | prdsdsval3 17435* | 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 17436 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ πΉ = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (πΉXs(πΌ Γ {π }))) | ||
Theorem | pwsbas 17437 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) β β’ ((π β π β§ πΌ β π) β (π΅ βm πΌ) = (Baseβπ)) | ||
Theorem | pwselbasb 17438 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβπ) β β’ ((π β π β§ πΌ β π) β (π β π β π:πΌβΆπ΅)) | ||
Theorem | pwselbas 17439 | 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 17440 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf + πΊ)) | ||
Theorem | pwsmulrval 17441 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β (πΉ β πΊ) = (πΉ βf Β· πΊ)) | ||
Theorem | pwsle 17442 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ ((π β π β§ πΌ β π) β β€ = ( βr π β© (π΅ Γ π΅))) | ||
Theorem | pwsleval 17443* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (leβπ ) & β’ β€ = (leβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ β€ πΊ β βπ₯ β πΌ (πΉβπ₯)π(πΊβπ₯))) | ||
Theorem | pwsvscafval 17444 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) β β’ (π β (π΄ β π) = ((πΌ Γ {π΄}) βf Β· π)) | ||
Theorem | pwsvscaval 17445 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ πΉ = (Scalarβπ ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π΄ β πΎ) & β’ (π β π β π΅) & β’ (π β π½ β πΌ) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | pwssca 17446 | The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π = (Scalarβπ ) β β’ ((π β π β§ πΌ β π) β π = (Scalarβπ)) | ||
Theorem | pwsdiagel 17447 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (((π β π β§ πΌ β π) β§ π΄ β π΅) β (πΌ Γ {π΄}) β πΆ) | ||
Theorem | pwssnf1o 17448* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {πΌ}) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ ({πΌ} Γ {π₯})) & β’ πΆ = (Baseβπ) β β’ ((π β π β§ πΌ β π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Syntax | cordt 17449 | Extend class notation with the order topology. |
class ordTop | ||
Syntax | cxrs 17450 | Extend class notation with the extended real number structure. |
class β*π | ||
Definition | df-ordt 17451* | 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 17452* | The extended real number structure. Unlike df-cnfld 21145, 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 21145. 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 17453 | Extend class notation with the quotient topology function. |
class qTop | ||
Syntax | cimas 17454 | Image structure function. |
class βs | ||
Syntax | cqus 17455 | Quotient structure function. |
class /s | ||
Syntax | cxps 17456 | Binary product structure function. |
class Γs | ||
Definition | df-qtop 17457* | 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 17458* |
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 5688, 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 5687) and/or π ( with df-ress 17178) 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 17459* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 17458 where the image function is π₯ β¦ [π₯]π. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) | ||
Definition | df-xps 17460* | 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 17461* | 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 17462 | 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 17463* | 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 17464 | 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 17465* | 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 17466* | 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 17467* | 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 17468* | 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 17469 | 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 17470* | 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 17471* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ , = (Β·πβπ ) & β’ πΌ = (Β·πβπ) β β’ (π β πΌ = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π , π)β©}) | ||
Theorem | imastset 17472 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π½ = (TopOpenβπ ) & β’ π = (TopSetβπ) β β’ (π β π = (π½ qTop πΉ)) | ||
Theorem | imasle 17473 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π = (leβπ ) & β’ β€ = (leβπ) β β’ (π β β€ = ((πΉ β π) β β‘πΉ)) | ||
Theorem | f1ocpbllem 17474 | Lemma for f1ocpbl 17475. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | f1ocpbl 17475 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 17476 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 17477 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlem 17478* | 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 17479* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflem 17480* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 17481* | 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 17482* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 17483* | 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 17484* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 17485* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 17486* | 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 17487* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ (π β β Fn (πΎ Γ π΅)) | ||
Theorem | imasvscaval 17488* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ πΊ = (Scalarβπ ) & β’ πΎ = (BaseβπΊ) & β’ Β· = ( Β·π βπ ) & β’ β = ( Β·π βπ) & β’ ((π β§ (π β πΎ β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) β β’ ((π β§ π β πΎ β§ π β π) β (π β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasvscaf 17489* | 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 17490 | 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 17491* | 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 17492* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 17493* | The function in qusval 17492 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 17494 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 17495 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | quss 17496 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ πΎ = (Scalarβπ ) β β’ (π β πΎ = (Scalarβπ)) | ||
Theorem | divsfval 17497* | Value of the function in qusval 17492. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllem 17498* | Lemma for ercpbl 17499. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 17499* | 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 17500* | 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 π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β ((π΄ βΌ πΆ β§ π΅ βΌ π·) β (π΄ππ΅ β πΆππ·))) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |