P. 174 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17301-17400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	phlip 17301	The inner product (Hermitian form) operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐻 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑇⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})    ⇒   ⊢ ( , ∈ 𝑋 → , = (·𝑖‘𝐻))
Theorem	tsetndx 17302	Index value of the df-tset 17221 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 17303	Utility theorem: index-independent form of df-tset 17221. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetndxnn 17304	The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.)
⊢ (TopSet‘ndx) ∈ ℕ
Theorem	basendxlttsetndx 17305	The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
⊢ (Base‘ndx) < (TopSet‘ndx)
Theorem	tsetndxnbasendx 17306	The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.)
⊢ (TopSet‘ndx) ≠ (Base‘ndx)
Theorem	tsetndxnplusgndx 17307	The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19260. (Contributed by AV, 18-Oct-2024.)
⊢ (TopSet‘ndx) ≠ (+g‘ndx)
Theorem	tsetndxnmulrndx 17308	The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
⊢ (TopSet‘ndx) ≠ (.r‘ndx)
Theorem	tsetndxnstarvndx 17309	The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 21158. (Contributed by AV, 11-Nov-2024.)
⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx)
Theorem	slotstnscsi 17310	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 20936 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx))
Theorem	topgrpstr 17311	A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ 𝑊 Struct ⟨1, 9⟩
Theorem	topgrpbas 17312	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊))
Theorem	topgrpplusg 17313	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊))
Theorem	topgrptset 17314	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊))
Theorem	resstset 17315	TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐽 = (TopSet‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻))
Theorem	plendx 17316	Index value of the df-ple 17222 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.)
⊢ (le‘ndx) = ;10
Theorem	pleid 17317	Utility theorem: self-referencing, index-independent form of df-ple 17222. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	plendxnn 17318	The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.)
⊢ (le‘ndx) ∈ ℕ
Theorem	basendxltplendx 17319	The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.)
⊢ (Base‘ndx) < (le‘ndx)
Theorem	plendxnbasendx 17320	The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.)
⊢ (le‘ndx) ≠ (Base‘ndx)
Theorem	plendxnplusgndx 17321	The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgle 32394. (Contributed by AV, 18-Oct-2024.)
⊢ (le‘ndx) ≠ (+g‘ndx)
Theorem	plendxnmulrndx 17322	The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. Formerly part of proof for opsrmulr 21830. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (.r‘ndx)
Theorem	plendxnscandx 17323	The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. Formerly part of proof for opsrsca 21834. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (Scalar‘ndx)
Theorem	plendxnvscandx 17324	The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. Formerly part of proof for opsrvsca 21832. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx)
Theorem	slotsdifplendx 17325	The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21158. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx))
Theorem	otpsstr 17326	Functionality of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}    ⇒   ⊢ 𝐾 Struct ⟨1, ;10⟩
Theorem	otpsbas 17327	The base set of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾))
Theorem	otpstset 17328	The open sets of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}    ⇒   ⊢ (𝐽 ∈ 𝑉 → 𝐽 = (TopSet‘𝐾))
Theorem	otpsle 17329	The order of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ≤ ⟩}    ⇒   ⊢ ( ≤ ∈ 𝑉 → ≤ = (le‘𝐾))
Theorem	ressle 17330	le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ 𝑊 = (𝐾 ↾s 𝐴)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊))
Theorem	ocndx 17331	Index value of the df-ocomp 17223 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
⊢ (oc‘ndx) = ;11
Theorem	ocid 17332	Utility theorem: index-independent form of df-ocomp 17223. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ oc = Slot (oc‘ndx)
Theorem	basendxnocndx 17333	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21469. (Contributed by AV, 11-Nov-2024.)
⊢ (Base‘ndx) ≠ (oc‘ndx)
Theorem	plendxnocndx 17334	The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21471. (Contributed by AV, 11-Nov-2024.)
⊢ (le‘ndx) ≠ (oc‘ndx)
Theorem	dsndx 17335	Index value of the df-ds 17224 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 17336	Utility theorem: index-independent form of df-ds 17224. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsndxnn 17337	The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 24211. (Contributed by AV, 28-Oct-2024.)
⊢ (dist‘ndx) ∈ ℕ
Theorem	basendxltdsndx 17338	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 24211. (Contributed by AV, 28-Oct-2024.)
⊢ (Base‘ndx) < (dist‘ndx)
Theorem	dsndxnbasendx 17339	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 17340	The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 20042. (Contributed by AV, 18-Oct-2024.)
⊢ (dist‘ndx) ≠ (+g‘ndx)
Theorem	dsndxnmulrndx 17341	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 17342	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 20936 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx))
Theorem	dsndxntsetndx 17343	The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 24385. (Contributed by AV, 29-Oct-2024.)
⊢ (dist‘ndx) ≠ (TopSet‘ndx)
Theorem	slotsdifdsndx 17344	The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21158. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx))
Theorem	unifndx 17345	Index value of the df-unif 17225 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 17346	Utility theorem: index-independent form of df-unif 17225. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)
Theorem	unifndxnn 17347	The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem 23992. (Contributed by AV, 28-Oct-2024.)
⊢ (UnifSet‘ndx) ∈ ℕ
Theorem	basendxltunifndx 17348	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 23992. (Contributed by AV, 28-Oct-2024.)
⊢ (Base‘ndx) < (UnifSet‘ndx)
Theorem	unifndxnbasendx 17349	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 17350	The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem 23992. (Contributed by AV, 28-Oct-2024.)
⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx)
Theorem	slotsdifunifndx 17351	The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT 21158. (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 17352	UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑈 = (UnifSet‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻))
Theorem	odrngstr 17353	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 17354	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 17355	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 17356	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 17357	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 17358	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 17359	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 17360	dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐷 = (dist‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻))
Theorem	homndx 17361	Index value of the df-hom 17226 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (Hom ‘ndx) = ;14
Theorem	homid 17362	Utility theorem: index-independent form of df-hom 17226. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ Hom = Slot (Hom ‘ndx)
Theorem	ccondx 17363	Index value of the df-cco 17227 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (comp‘ndx) = ;15
Theorem	ccoid 17364	Utility theorem: index-independent form of df-cco 17227. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ comp = Slot (comp‘ndx)
Theorem	slotsbhcdif 17365	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 17366	Obsolete proof of slotsbhcdif 17365 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 17367	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 47777. (Contributed by AV, 12-Nov-2024.)
⊢ ((le‘ndx) ≠ (comp‘ndx) ∧ (le‘ndx) ≠ (Hom ‘ndx))
Theorem	slotsdifocndx 17368	The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval 47780. (Contributed by AV, 12-Nov-2024.)
⊢ ((oc‘ndx) ≠ (comp‘ndx) ∧ (oc‘ndx) ≠ (Hom ‘ndx))
Theorem	resshom 17369	Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾s 𝐴)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷))
Theorem	ressco 17370	comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ 𝐷 = (𝐶 ↾s 𝐴)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷))
7.1.3  Definition of the structure product
Syntax	crest 17371	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 17372	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 17373*	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 17374	Define the topology extractor function. This differs from df-tset 17221 when a structure has been restricted using df-ress 17179; 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 17375	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
⊢ ↾t Fn (V × V)
Theorem	topnfn 17376	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ TopOpen Fn V
Theorem	restval 17377*	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 17378*	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 17379	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 17380	Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	restid2 17381	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽)
Theorem	restsspw 17382	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴
Theorem	firest 17383	The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴)
Theorem	restid 17384	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 17385	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopSet‘𝑊)    ⇒   ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊)
Theorem	topnid 17386	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 17387	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 17388	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 17389	Extend class notation with a function whose value is a product topology.
class ∏t
Syntax	c0g 17390	Extend class notation with group identity element.
class 0g
Syntax	cgsu 17391	Extend class notation to include finitely supported group sums.
class Σg
Definition	df-0g 17392*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 17393. The related theorems are provided later, see grpidval 18587. (Contributed by NM, 20-Aug-2011.)
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))
Definition	df-gsum 17393*	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 18610. 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 18612 and gsumnunsn 33847. 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 19817. 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 23852. Remark: this definition is required here because the symbol Σg is already used in df-prds 17398 and df-imas 17459. The related theorems are provided later, see gsumvalx 18602. (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 17394*	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 22680). The first use of this definition is tgval 22679 but the token is used in df-pt 17395. See tgval3 22687 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.)
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})
Definition	df-pt 17395*	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 17396	The function constructing structure products.
class Xs
Syntax	cpws 17397	The function constructing structure powers.
class ↑s
Definition	df-prds 17398*	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 17399	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 17400*	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(𝑖 × {𝑟})))