P. 125 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	coc 12401	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 12402	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 12403	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 12404	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 12405	Extend class notation with the composition operation.
class comp
Definition	df-plusg 12406	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ +g = Slot 2
Definition	df-mulr 12407	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ .r = Slot 3
Definition	df-starv 12408	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ *𝑟 = Slot 4
Definition	df-sca 12409	Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ Scalar = Slot 5
Definition	df-vsca 12410	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 12411	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 12412	Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ TopSet = Slot 9
Definition	df-ple 12413	Define "less than or equal to" ordering extractor for posets and related structures. We use ;10 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot ;10
Definition	df-ocomp 12414	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ oc = Slot ;11
Definition	df-ds 12415	Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ dist = Slot ;12
Definition	df-unif 12416	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ UnifSet = Slot ;13
Definition	df-hom 12417	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ Hom = Slot ;14
Definition	df-cco 12418	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ comp = Slot ;15
Theorem	strleund 12419	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ (𝜑 → 𝐹 Struct ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐺 Struct ⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩)
Theorem	strleun 12420	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strle1g 12421	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ (𝑋 ∈ 𝑉 → {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩)
Theorem	strle2g 12422	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩)
Theorem	strle3g 12423	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩)
Theorem	plusgndx 12424	Index value of the df-plusg 12406 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (+g‘ndx) = 2
Theorem	plusgid 12425	Utility theorem: index-independent form of df-plusg 12406. (Contributed by NM, 20-Oct-2012.)
⊢ +g = Slot (+g‘ndx)
Theorem	plusgslid 12426	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
Theorem	opelstrsl 12427	The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (𝐸‘𝑆))
Theorem	opelstrbas 12428	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (Base‘𝑆))
Theorem	1strstrg 12429	A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐺 Struct ⟨1, 1⟩)
Theorem	1strbas 12430	The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strstrg 12431	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨1, 𝑁⟩)
Theorem	2strbasg 12432	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	2stropg 12433	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺))
Theorem	2strstr1g 12434	A constructed two-slot structure. Version of 2strstrg 12431 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨(Base‘ndx), 𝑁⟩)
Theorem	2strbas1g 12435	The base set of a constructed two-slot structure. Version of 2strbasg 12432 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	2strop1g 12436	The other slot of a constructed two-slot structure. Version of 2stropg 12433 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺))
Theorem	basendxnplusgndx 12437	The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ (Base‘ndx) ≠ (+g‘ndx)
Theorem	grpstrg 12438	A constructed group is a structure on 1...2. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨1, 2⟩)
Theorem	grpbaseg 12439	The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	grpplusgg 12440	The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (+g‘𝐺))
Theorem	mulrndx 12441	Index value of the df-mulr 12407 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (.r‘ndx) = 3
Theorem	mulrid 12442	Utility theorem: index-independent form of df-mulr 12407. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	mulrslid 12443	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
Theorem	plusgndxnmulrndx 12444	The slot for the group (addition) operation is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.)
⊢ (+g‘ndx) ≠ (.r‘ndx)
Theorem	basendxnmulrndx 12445	The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.)
⊢ (Base‘ndx) ≠ (.r‘ndx)
Theorem	rngstrg 12446	A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝑅 Struct ⟨1, 3⟩)
Theorem	rngbaseg 12447	The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝐵 = (Base‘𝑅))
Theorem	rngplusgg 12448	The additive operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → + = (+g‘𝑅))
Theorem	rngmulrg 12449	The multiplicative operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → · = (.r‘𝑅))
Theorem	starvndx 12450	Index value of the df-starv 12408 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 12451	Utility theorem: index-independent form of df-starv 12408. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvslid 12452	Slot property of *𝑟. (Contributed by Jim Kingdon, 4-Feb-2023.)
⊢ (*𝑟 = Slot (*𝑟‘ndx) ∧ (*𝑟‘ndx) ∈ ℕ)
Theorem	srngstrd 12453	A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑅 Struct ⟨1, 4⟩)
Theorem	srngbased 12454	The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))
Theorem	srngplusgd 12455	The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → + = (+g‘𝑅))
Theorem	srngmulrd 12456	The multiplication operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → · = (.r‘𝑅))
Theorem	srnginvld 12457	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 12458	Index value of the df-sca 12409 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 12459	Utility theorem: index-independent form of scalar df-sca 12409. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scaslid 12460	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
Theorem	vscandx 12461	Index value of the df-vsca 12410 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 12462	Utility theorem: index-independent form of scalar product df-vsca 12410. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscaslid 12463	Slot property of ·𝑠. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
Theorem	lmodstrd 12464	A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑊 Struct ⟨1, 6⟩)
Theorem	lmodbased 12465	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))
Theorem	lmodplusgd 12466	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → + = (+g‘𝑊))
Theorem	lmodscad 12467	The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
Theorem	lmodvscad 12468	The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 7-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))
Theorem	ipndx 12469	Index value of the df-ip 12411 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 12470	Utility theorem: index-independent form of df-ip 12411. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipslid 12471	Slot property of ·𝑖. (Contributed by Jim Kingdon, 7-Feb-2023.)
⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ)
Theorem	ipsstrd 12472	A constructed inner product space is a structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 Struct ⟨1, 8⟩)
Theorem	ipsbased 12473	The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝐴))
Theorem	ipsaddgd 12474	The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → + = (+g‘𝐴))
Theorem	ipsmulrd 12475	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → × = (.r‘𝐴))
Theorem	ipsscad 12476	The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑆 = (Scalar‘𝐴))
Theorem	ipsvscad 12477	The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → · = ( ·𝑠 ‘𝐴))
Theorem	ipsipd 12478	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐼 = (·𝑖‘𝐴))
Theorem	tsetndx 12479	Index value of the df-tset 12412 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 12480	Utility theorem: index-independent form of df-tset 12412. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetslid 12481	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (TopSet = Slot (TopSet‘ndx) ∧ (TopSet‘ndx) ∈ ℕ)
Theorem	topgrpstrd 12482	A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑊 Struct ⟨1, 9⟩)
Theorem	topgrpbasd 12483	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))
Theorem	topgrpplusgd 12484	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → + = (+g‘𝑊))
Theorem	topgrptsetd 12485	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐽 = (TopSet‘𝑊))
Theorem	plendx 12486	Index value of the df-ple 12413 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ (le‘ndx) = ;10
Theorem	pleid 12487	Utility theorem: self-referencing, index-independent form of df-ple 12413. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	pleslid 12488	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ)
Theorem	dsndx 12489	Index value of the df-ds 12415 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 12490	Utility theorem: index-independent form of df-ds 12415. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsslid 12491	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ)
6.1.3  Definition of the structure product
Syntax	crest 12492	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 12493	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 12494*	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 12495	Define the topology extractor function. This differs from df-tset 12412 when a structure has been restricted using df-ress 12339; 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 12496	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
⊢ ↾t Fn (V × V)
Theorem	topnfn 12497	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ TopOpen Fn V
Theorem	restval 12498*	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 12499*	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 12500	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 𝑆))