Home | Metamath
Proof Explorer Theorem List (p. 168 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ctg 16701 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 16702 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 16703 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 16704 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 16705* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 16706. The related theorems are provided later, see grpidval 17861. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 16706* |
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 17884. 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 17886 and gsumnunsn 31711. 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 18958. 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 22664. Remark: this definition is required here because the symbol Σg is already used in df-prds 16711 and df-imas 16771. The related theorems are provided later, see gsumvalx 17876. (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 16707* | 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 21494). The first use of this definition is tgval 21493 but the token is used in df-pt 16708. See tgval3 21501 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
Definition | df-pt 16708* | 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 16709 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 16710 | The function constructing structure powers. |
class ↑s | ||
Definition | df-prds 16711* | 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 16712 | 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 16713* | 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 16714* | Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.) |
⊢ 𝐵 = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ⇒ ⊢ 𝐵 ∈ V | ||
Theorem | imasvalstr 16715 | 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 16716 | 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 16717 | Lemma for prdsbas 16720 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (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), ∙ 〉}))) & ⊢ 𝐴 = (𝐸‘𝑈) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑇 ∈ V) & ⊢ {〈(𝐸‘ndx), 𝑇〉} ⊆ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ ({〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), 𝐿〉, 〈(dist‘ndx), 𝐷〉} ∪ {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ∙ 〉})) ⇒ ⊢ (𝜑 → 𝐴 = 𝑇) | ||
Theorem | prdsval 16718* | 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 16719 | 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 16720* | 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 16721* | 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 16722* | 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 16723* | 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 16724* | Inner product in a structure product. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ , = (·𝑖‘𝑃) ⇒ ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))) | ||
Theorem | prdsle 16725* | 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 16726 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ ≤ = (le‘𝑃) ⇒ ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵)) | ||
Theorem | prdsds 16727* | 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 16728 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐷 = (dist‘𝑃) ⇒ ⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) | ||
Theorem | prdstset 16729 | 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 16730* | 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 16731* | 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 16732* | 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 16733* | 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 16734 | Points in the structure product are functions; use this with dffn5 6718 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 Fn 𝐼) | ||
Theorem | prdsbasprj 16735 | 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 16736* | 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 16737 | 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 16738* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ · = (.r‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(.r‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsmulrfval 16739 | 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 16740* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)(le‘(𝑅‘𝑥))(𝐺‘𝑥))) | ||
Theorem | prdsdsval 16741* | 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 16742* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ (𝐹( ·𝑠 ‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsvscafval 16743 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = (𝐹( ·𝑠 ‘(𝑅‘𝐽))(𝐺‘𝐽))) | ||
Theorem | prdsbas3 16744* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝐾) | ||
Theorem | prdsbasmpt2 16745* | 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 16746* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ 𝐾) | ||
Theorem | prdsdsval2 16747* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ 𝐸 = (dist‘𝑅) & ⊢ 𝐷 = (dist‘𝑌) ⇒ ⊢ (𝜑 → (𝐹𝐷𝐺) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝐸(𝐺‘𝑥))) ∪ {0}), ℝ*, < )) | ||
Theorem | prdsdsval3 16748* | 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 16749 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐹 = (Scalar‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅}))) | ||
Theorem | pwsbas 16750 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑m 𝐼) = (Base‘𝑌)) | ||
Theorem | pwselbasb 16751 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑉 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍) → (𝑋 ∈ 𝑉 ↔ 𝑋:𝐼⟶𝐵)) | ||
Theorem | pwselbas 16752 | 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 16753 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = (+g‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ✚ 𝐺) = (𝐹 ∘f + 𝐺)) | ||
Theorem | pwsmulrval 16754 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝐹 ∘f · 𝐺)) | ||
Theorem | pwsle 16755 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑂 = (le‘𝑅) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r 𝑂 ∩ (𝐵 × 𝐵))) | ||
Theorem | pwsleval 16756* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑂 = (le‘𝑅) & ⊢ ≤ = (le‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)𝑂(𝐺‘𝑥))) | ||
Theorem | pwsvscafval 16757 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑌) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∙ 𝑋) = ((𝐼 × {𝐴}) ∘f · 𝑋)) | ||
Theorem | pwsvscaval 16758 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑌) & ⊢ 𝐹 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽))) | ||
Theorem | pwssca 16759 | The ring of scalars of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑆 = (Scalar‘𝑌)) | ||
Theorem | pwsdiagel 16760 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑌) ⇒ ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝐴 ∈ 𝐵) → (𝐼 × {𝐴}) ∈ 𝐶) | ||
Theorem | pwssnf1o 16761* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s {𝐼}) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ({𝐼} × {𝑥})) & ⊢ 𝐶 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Syntax | cordt 16762 | Extend class notation with the order topology. |
class ordTop | ||
Syntax | cxrs 16763 | Extend class notation with the extended real number structure. |
class ℝ*𝑠 | ||
Definition | df-ordt 16764* | 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 16765* | The extended real number structure. Unlike df-cnfld 20476, 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 20476. 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 16766 | Extend class notation with the quotient topology function. |
class qTop | ||
Syntax | cimas 16767 | Image structure function. |
class “s | ||
Syntax | cqus 16768 | Quotient structure function. |
class /s | ||
Syntax | cxps 16769 | Binary product structure function. |
class ×s | ||
Definition | df-qtop 16770* | 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 16771* |
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 5562, 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 5561) and/or 𝑅 ( with df-ress 16481) 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 16772* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 16771 where the image function is 𝑥 ↦ [𝑥]𝑒. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟)) | ||
Definition | df-xps 16773* | 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 16774* | 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 16775 | 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 16776* | 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 16777 | 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 16778* | 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 16779* | 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 16780* | 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 16781* | 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 16782 | 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 16783* | 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 16784* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ , = (·𝑖‘𝑅) & ⊢ 𝐼 = (·𝑖‘𝑈) ⇒ ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝 , 𝑞)〉}) | ||
Theorem | imastset 16785 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝑂 = (TopSet‘𝑈) ⇒ ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) | ||
Theorem | imasle 16786 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝑁 = (le‘𝑅) & ⊢ ≤ = (le‘𝑈) ⇒ ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹)) | ||
Theorem | f1ocpbllem 16787 | Lemma for f1ocpbl 16788. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | f1ocpbl 16788 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷)))) | ||
Theorem | f1ovscpbl 16789 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐹‘𝐵) = (𝐹‘𝐶) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐴 + 𝐶)))) | ||
Theorem | f1olecpbl 16790 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷))) | ||
Theorem | imasaddfnlem 16791* | 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 16792* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasaddflem 16793* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) ⇒ ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | imasaddfn 16794* | 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 16795* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (+g‘𝑅) & ⊢ ∙ = (+g‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasaddf 16796* | 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 16797* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵)) | ||
Theorem | imasmulval 16798* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasmulf 16799* | 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 16800* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑈) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) ⇒ ⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |