Home | Metamath
Proof Explorer Theorem List (p. 173 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dsndx 17201 | Index value of the df-ds 17090 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 17202 | Utility theorem: index-independent form of df-ds 17090. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | dsndxnn 17203 | The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 23759. (Contributed by AV, 28-Oct-2024.) |
⊢ (dist‘ndx) ∈ ℕ | ||
Theorem | basendxltdsndx 17204 | The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. Formerly part of proof for tmslem 23759. (Contributed by AV, 28-Oct-2024.) |
⊢ (Base‘ndx) < (dist‘ndx) | ||
Theorem | dsndxnbasendx 17205 | The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ (dist‘ndx) ≠ (Base‘ndx) | ||
Theorem | dsndxnplusgndx 17206 | The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 19838. (Contributed by AV, 18-Oct-2024.) |
⊢ (dist‘ndx) ≠ (+g‘ndx) | ||
Theorem | dsndxnmulrndx 17207 | The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
⊢ (dist‘ndx) ≠ (.r‘ndx) | ||
Theorem | slotsdnscsi 17208 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 20561 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | dsndxntsetndx 17209 | The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 23933. (Contributed by AV, 29-Oct-2024.) |
⊢ (dist‘ndx) ≠ (TopSet‘ndx) | ||
Theorem | slotsdifdsndx 17210 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 20732. (Contributed by AV, 11-Nov-2024.) |
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) | ||
Theorem | unifndx 17211 | Index value of the df-unif 17091 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.) |
⊢ (UnifSet‘ndx) = ;13 | ||
Theorem | unifid 17212 | Utility theorem: index-independent form of df-unif 17091. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ UnifSet = Slot (UnifSet‘ndx) | ||
Theorem | unifndxnn 17213 | The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem 23540. (Contributed by AV, 28-Oct-2024.) |
⊢ (UnifSet‘ndx) ∈ ℕ | ||
Theorem | basendxltunifndx 17214 | The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. Formerly part of proof for tuslem 23540. (Contributed by AV, 28-Oct-2024.) |
⊢ (Base‘ndx) < (UnifSet‘ndx) | ||
Theorem | unifndxnbasendx 17215 | The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
⊢ (UnifSet‘ndx) ≠ (Base‘ndx) | ||
Theorem | unifndxntsetndx 17216 | The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem 23540. (Contributed by AV, 28-Oct-2024.) |
⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx) | ||
Theorem | slotsdifunifndx 17217 | The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT 20732. (Contributed by AV, 10-Nov-2024.) |
⊢ (((+g‘ndx) ≠ (UnifSet‘ndx) ∧ (.r‘ndx) ≠ (UnifSet‘ndx) ∧ (*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧ ((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx))) | ||
Theorem | ressunif 17218 | UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑈 = (UnifSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻)) | ||
Theorem | odrngstr 17219 | Functionality of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ 𝑊 Struct ⟨1, ;12⟩ | ||
Theorem | odrngbas 17220 | The base set of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝑊)) | ||
Theorem | odrngplusg 17221 | The addition operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝑊)) | ||
Theorem | odrngmulr 17222 | The multiplication operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ ( · ∈ 𝑉 → · = (.r‘𝑊)) | ||
Theorem | odrngtset 17223 | The open sets of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | odrngle 17224 | The order of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ ( ≤ ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | odrngds 17225 | The metric of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | ressds 17226 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
Theorem | homndx 17227 | Index value of the df-hom 17092 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
⊢ (Hom ‘ndx) = ;14 | ||
Theorem | homid 17228 | Utility theorem: index-independent form of df-hom 17092. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ Hom = Slot (Hom ‘ndx) | ||
Theorem | ccondx 17229 | Index value of the df-cco 17093 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
⊢ (comp‘ndx) = ;15 | ||
Theorem | ccoid 17230 | Utility theorem: index-independent form of df-cco 17093. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ comp = Slot (comp‘ndx) | ||
Theorem | slotsbhcdif 17231 | The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ ((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) | ||
Theorem | slotsbhcdifOLD 17232 | Obsolete proof of slotsbhcdif 17231 as of 28-Oct-2024. The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) | ||
Theorem | slotsdifplendx2 17233 | The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval 46806. (Contributed by AV, 12-Nov-2024.) |
⊢ ((le‘ndx) ≠ (comp‘ndx) ∧ (le‘ndx) ≠ (Hom ‘ndx)) | ||
Theorem | slotsdifocndx 17234 | The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval 46809. (Contributed by AV, 12-Nov-2024.) |
⊢ ((oc‘ndx) ≠ (comp‘ndx) ∧ (oc‘ndx) ≠ (Hom ‘ndx)) | ||
Theorem | resshom 17235 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | ressco 17236 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
Syntax | crest 17237 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 17238 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 17239* | Function returning the subspace topology induced by the topology 𝑦 and the set 𝑥. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))) | ||
Definition | df-topn 17240 | Define the topology extractor function. This differs from df-tset 17087 when a structure has been restricted using df-ress 17048; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤))) | ||
Theorem | restfn 17241 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 17242 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 17243* | The subspace topology induced by the topology 𝐽 on the set 𝐴. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | ||
Theorem | elrest 17244* | The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) | ||
Theorem | elrestr 17245 | Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) | ||
Theorem | 0rest 17246 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | restid2 17247 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 17248 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | firest 17249 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
Theorem | restid 17250 | The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽) | ||
Theorem | topnval 17251 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
Theorem | topnid 17252 | 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 17253 | 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 17254 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 17255 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 17256 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 17257 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 17258* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 17259. The related theorems are provided later, see grpidval 18451. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 17259* |
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 18474. 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 18476 and gsumnunsn 32914. 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 19613. 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 23400. Remark: this definition is required here because the symbol Σg is already used in df-prds 17264 and df-imas 17325. The related theorems are provided later, see gsumvalx 18466. (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 17260* | 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 22228). The first use of this definition is tgval 22227 but the token is used in df-pt 17261. See tgval3 22235 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
Definition | df-pt 17261* | 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 17262 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 17263 | The function constructing structure powers. |
class ↑s | ||
Definition | df-prds 17264* | 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.) (Revised by Zhi Wang, 18-Aug-2024.) |
⊢ 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 17265 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
⊢ Rel dom Xs | ||
Definition | df-pws 17266* | 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 17267* | Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.) |
⊢ 𝐵 = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ⇒ ⊢ 𝐵 ∈ V | ||
Theorem | imasvalstr 17268 | 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 17269 | 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 17270 | Lemma for prdsbas 17274 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 17271* | Lemma for prdsval 17272. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 17272, dependency on df-hom 17092 removed. (Revised by AV, 13-Oct-2024.) |
⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V | ||
Theorem | prdsval 17272* | 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 17273 | 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 17274* | 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 17275* | 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 17276* | 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 17277* | 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 17278* | 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 17279* | 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 17280 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ ≤ = (le‘𝑃) ⇒ ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵)) | ||
Theorem | prdsds 17281* | 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 17282 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ 𝐷 = (dist‘𝑃) ⇒ ⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) | ||
Theorem | prdstset 17283 | 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 17284* | 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 17285* | 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 17286* | 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 17287* | 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 17288 | Points in the structure product are functions; use this with dffn5 6897 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑇 Fn 𝐼) | ||
Theorem | prdsbasprj 17289 | 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 17290* | 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 17291 | 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 17292* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ · = (.r‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(.r‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsmulrfval 17293 | 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 17294* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)(le‘(𝑅‘𝑥))(𝐺‘𝑥))) | ||
Theorem | prdsdsval 17295* | 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 17296* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ (𝐹( ·𝑠 ‘(𝑅‘𝑥))(𝐺‘𝑥)))) | ||
Theorem | prdsvscafval 17297 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = (𝐹( ·𝑠 ‘(𝑅‘𝐽))(𝐺‘𝐽))) | ||
Theorem | prdsbas3 17298* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝐾) | ||
Theorem | prdsbasmpt2 17299* | 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 17300* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ 𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |