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