Home | Metamath
Proof Explorer Theorem List (p. 168 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | topnid 16701 | Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ⊆ 𝒫 𝐵 → 𝐽 = (TopOpen‘𝑊)) | ||
Theorem | topnpropd 16702 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) ⇒ ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) | ||
Syntax | ctg 16703 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 16704 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 16705 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 16706 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 16707* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 16708. The related theorems are provided later, see grpidval 17863. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 16708* |
Define the group sum (also called "iterated sum") for the structure
𝐺 of a finite sequence of elements
whose values are defined by the
expression 𝐵 and whose set of indices is 𝐴. It
may be viewed
as a product (if 𝐺 is a multiplication), a sum (if
𝐺
is an
addition) or any other operation. The variable 𝑘 is normally a free
variable in 𝐵 (i.e., 𝐵 can be thought of as
𝐵(𝑘)). The
definition is meaningful in different contexts, depending on the size of
the index set 𝐴 and each demanding different
properties of 𝐺.
1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity. See gsum0 17886. 2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e. (𝐵(1) + 𝐵(2)) + 𝐵(3) etc. See gsumval2 17888 and gsumnunsn 31921. 3. If 𝐴 is a finite set (or is nonzero for finitely many indices) and 𝐺 is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. See gsumval3 19020. 4. If 𝐴 is an infinite set and 𝐺 is a Hausdorff topological group, then there is a meaningful sum, but Σg cannot handle this case. See df-tsms 22732. Remark: this definition is required here because the symbol Σg is already used in df-prds 16713 and df-imas 16773. The related theorems are provided later, see gsumvalx 17878. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))) | ||
Definition | df-topgen 16709* | Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 21561). The first use of this definition is tgval 21560 but the token is used in df-pt 16710. See tgval3 21568 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
Definition | df-pt 16710* | Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) | ||
Syntax | cprds 16711 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 16712 | The function constructing structure powers. |
class ↑s | ||
Definition | df-prds 16713* | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({〈(Base‘ndx), 𝑣〉, 〈(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx), 𝑠〉, 〈( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))〉} ∪ {〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ (𝑐ℎ(2nd ‘𝑎)), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) | ||
Theorem | reldmprds 16714 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
⊢ Rel dom Xs | ||
Definition | df-pws 16715* | Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))) | ||
Theorem | prdsbasex 16716* | Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.) |
⊢ 𝐵 = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ⇒ ⊢ 𝐵 ∈ V | ||
Theorem | imasvalstr 16717 | 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), 𝐷〉}) ⇒ ⊢ 𝑈 Struct 〈1, ;12〉 | ||
Theorem | prdsvalstr 16718 | 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 | prdsvallem 16719 | Lemma for prdsbas 16722 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 | prdsval 16720* | 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.) |
⊢ 𝑃 = (𝑆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 16721 | 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.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑆 = (Scalar‘𝑃)) | ||
Theorem | prdsbas 16722* | 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.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) ⇒ ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) | ||
Theorem | prdsplusg 16723* | 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.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ + = (+g‘𝑃) ⇒ ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))) | ||
Theorem | prdsmulr 16724* | 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.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ · = (.r‘𝑃) ⇒ ⊢ (𝜑 → · = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))) | ||
Theorem | prdsvsca 16725* | 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.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))) | ||
Theorem | prdsip 16726* | Inner product in a structure product. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ , = (·𝑖‘𝑃) ⇒ ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))) | ||
Theorem | prdsle 16727* | Structure product weak ordering. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ ≤ = (le‘𝑃) ⇒ ⊢ (𝜑 → ≤ = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}) | ||
Theorem | prdsless 16728 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ ≤ = (le‘𝑃) ⇒ ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵)) | ||
Theorem | prdsds 16729* | Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐷 = (dist‘𝑃) ⇒ ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))) | ||
Theorem | prdsdsfn 16730 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐷 = (dist‘𝑃) ⇒ ⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) | ||
Theorem | prdstset 16731 | Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝑂 = (TopSet‘𝑃) ⇒ ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅))) | ||
Theorem | prdshom 16732* | Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐻 = (Hom ‘𝑃) ⇒ ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))) | ||
Theorem | prdsco 16733* | Structure product composition operation. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐻 = (Hom ‘𝑃) & ⊢ ∙ = (comp‘𝑃) ⇒ ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd ‘𝑎)), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))) | ||
Theorem | prdsbas2 16734* | 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 16735* | 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 16736 | Points in the structure product are functions; use this with dffn5 6699 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 Fn 𝐼) | ||
Theorem | prdsbasprj 16737 | 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 16738* | 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 16739 | 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 16740* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ · = (.r‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(.r‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsmulrfval 16741 | 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 16742* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)(le‘(𝑅‘𝑥))(𝐺‘𝑥))) | ||
Theorem | prdsdsval 16743* | 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 16744* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ (𝐹( ·𝑠 ‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsvscafval 16745 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = (𝐹( ·𝑠 ‘(𝑅‘𝐽))(𝐺‘𝐽))) | ||
Theorem | prdsbas3 16746* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝐾) | ||
Theorem | prdsbasmpt2 16747* | 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 16748* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ 𝐾) | ||
Theorem | prdsdsval2 16749* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ 𝐸 = (dist‘𝑅) & ⊢ 𝐷 = (dist‘𝑌) ⇒ ⊢ (𝜑 → (𝐹𝐷𝐺) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝐸(𝐺‘𝑥))) ∪ {0}), ℝ*, < )) | ||
Theorem | prdsdsval3 16750* | 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 16751 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐹 = (Scalar‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅}))) | ||
Theorem | pwsbas 16752 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑m 𝐼) = (Base‘𝑌)) | ||
Theorem | pwselbasb 16753 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑉 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍) → (𝑋 ∈ 𝑉 ↔ 𝑋:𝐼⟶𝐵)) | ||
Theorem | pwselbas 16754 | 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 16755 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ✚ 𝐺) = (𝐹 ∘f + 𝐺)) | ||
Theorem | pwsmulrval 16756 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝐹 ∘f · 𝐺)) | ||
Theorem | pwsle 16757 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑂 = (le‘𝑅) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r 𝑂 ∩ (𝐵 × 𝐵))) | ||
Theorem | pwsleval 16758* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑂 = (le‘𝑅) & ⊢ ≤ = (le‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)𝑂(𝐺‘𝑥))) | ||
Theorem | pwsvscafval 16759 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑌) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∙ 𝑋) = ((𝐼 × {𝐴}) ∘f · 𝑋)) | ||
Theorem | pwsvscaval 16760 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑌) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽))) | ||
Theorem | pwssca 16761 | The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑆 = (Scalar‘𝑌)) | ||
Theorem | pwsdiagel 16762 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑌) ⇒ ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝐴 ∈ 𝐵) → (𝐼 × {𝐴}) ∈ 𝐶) | ||
Theorem | pwssnf1o 16763* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s {𝐼}) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ({𝐼} × {𝑥})) & ⊢ 𝐶 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Syntax | cordt 16764 | Extend class notation with the order topology. |
class ordTop | ||
Syntax | cxrs 16765 | Extend class notation with the extended real number structure. |
class ℝ*𝑠 | ||
Definition | df-ordt 16766* | 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 16767* | The extended real number structure. Unlike df-cnfld 20092, 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 20092. 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 16768 | Extend class notation with the quotient topology function. |
class qTop | ||
Syntax | cimas 16769 | Image structure function. |
class “s | ||
Syntax | cqus 16770 | Quotient structure function. |
class /s | ||
Syntax | cxps 16771 | Binary product structure function. |
class ×s | ||
Definition | df-qtop 16772* | 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 16773* |
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 5532, 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 5531) and/or 𝑅 ( with df-ress 16483) 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 16774* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 16773 where the image function is 𝑥 ↦ [𝑥]𝑒. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟)) | ||
Definition | df-xps 16775* | 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 16776* | 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 16777 | 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 16778* | 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 16779 | 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 16780* | 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 16781* | 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 16782* | 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 16783* | 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 16784 | 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 16785* | 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 16786* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ , = (·𝑖‘𝑅) & ⊢ 𝐼 = (·𝑖‘𝑈) ⇒ ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝 , 𝑞)〉}) | ||
Theorem | imastset 16787 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝑂 = (TopSet‘𝑈) ⇒ ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) | ||
Theorem | imasle 16788 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝑁 = (le‘𝑅) & ⊢ ≤ = (le‘𝑈) ⇒ ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹)) | ||
Theorem | f1ocpbllem 16789 | Lemma for f1ocpbl 16790. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | f1ocpbl 16790 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷)))) | ||
Theorem | f1ovscpbl 16791 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐹‘𝐵) = (𝐹‘𝐶) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐴 + 𝐶)))) | ||
Theorem | f1olecpbl 16792 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷))) | ||
Theorem | imasaddfnlem 16793* | 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 16794* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasaddflem 16795* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) ⇒ ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | imasaddfn 16796* | 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 16797* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (+g‘𝑅) & ⊢ ∙ = (+g‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasaddf 16798* | 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 16799* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) | ||
Theorem | imasmulval 16800* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |