P. 136 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13501-13600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressmulrg 13501	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → · = (.r‘𝑆))
Theorem	srngstrd 13502	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 13503	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 13504	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 13505	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 13506	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 13507	Index value of the df-sca 13449 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 13508	Utility theorem: index-independent form of scalar df-sca 13449. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scaslid 13509	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
Theorem	scandxnbasendx 13510	The slot for the scalar is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (Base‘ndx)
Theorem	scandxnplusgndx 13511	The slot for the scalar field is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (+g‘ndx)
Theorem	scandxnmulrndx 13512	The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (.r‘ndx)
Theorem	vscandx 13513	Index value of the df-vsca 13450 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 13514	Utility theorem: index-independent form of scalar product df-vsca 13450. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscandxnbasendx 13515	The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx)
Theorem	vscandxnplusgndx 13516	The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx)
Theorem	vscandxnmulrndx 13517	The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx)
Theorem	vscandxnscandx 13518	The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
Theorem	vscaslid 13519	Slot property of ·𝑠. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
Theorem	lmodstrd 13520	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 13521	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 13522	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 13523	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 13524	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 13525	Index value of the df-ip 13451 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 13526	Utility theorem: index-independent form of df-ip 13451. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipslid 13527	Slot property of ·𝑖. (Contributed by Jim Kingdon, 7-Feb-2023.)
⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ)
Theorem	ipndxnbasendx 13528	The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (Base‘ndx)
Theorem	ipndxnplusgndx 13529	The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (+g‘ndx)
Theorem	ipndxnmulrndx 13530	The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (.r‘ndx)
Theorem	slotsdifipndx 13531	The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.)
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx))
Theorem	ipsstrd 13532	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 13533	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 13534	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 13535	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 13536	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 13537	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 13538	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	ressscag 13539	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → 𝐹 = (Scalar‘𝐻))
Theorem	ressvscag 13540	·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → · = ( ·𝑠 ‘𝐻))
Theorem	ressipg 13541	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → , = (·𝑖‘𝐻))
Theorem	tsetndx 13542	Index value of the df-tset 13452 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 13543	Utility theorem: index-independent form of df-tset 13452. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetslid 13544	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (TopSet = Slot (TopSet‘ndx) ∧ (TopSet‘ndx) ∈ ℕ)
Theorem	tsetndxnn 13545	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 13546	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 13547	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 13548	The slot for the topology is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (TopSet‘ndx) ≠ (+g‘ndx)
Theorem	tsetndxnmulrndx 13549	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 13550	The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.)
⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx)
Theorem	slotstnscsi 13551	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. (Contributed by AV, 29-Oct-2024.)
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx))
Theorem	topgrpstrd 13552	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 13553	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 13554	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 13555	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 13556	Index value of the df-ple 13453 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ (le‘ndx) = ;10
Theorem	pleid 13557	Utility theorem: self-referencing, index-independent form of df-ple 13453. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	pleslid 13558	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ)
Theorem	plendxnn 13559	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 13560	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 13561	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 13562	The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (le‘ndx) ≠ (+g‘ndx)
Theorem	plendxnmulrndx 13563	The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (.r‘ndx)
Theorem	plendxnscandx 13564	The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (Scalar‘ndx)
Theorem	plendxnvscandx 13565	The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx)
Theorem	slotsdifplendx 13566	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx))
Theorem	ocndx 13567	Index value of the df-ocomp 13454 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
⊢ (oc‘ndx) = ;11
Theorem	ocid 13568	Utility theorem: index-independent form of df-ocomp 13454. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ oc = Slot (oc‘ndx)
Theorem	basendxnocndx 13569	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)
⊢ (Base‘ndx) ≠ (oc‘ndx)
Theorem	plendxnocndx 13570	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)
⊢ (le‘ndx) ≠ (oc‘ndx)
Theorem	dsndx 13571	Index value of the df-ds 13455 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 13572	Utility theorem: index-independent form of df-ds 13455. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsslid 13573	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ)
Theorem	dsndxnn 13574	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
⊢ (dist‘ndx) ∈ ℕ
Theorem	basendxltdsndx 13575	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)
⊢ (Base‘ndx) < (dist‘ndx)
Theorem	dsndxnbasendx 13576	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 13577	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (dist‘ndx) ≠ (+g‘ndx)
Theorem	dsndxnmulrndx 13578	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 13579	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx))
Theorem	dsndxntsetndx 13580	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ (dist‘ndx) ≠ (TopSet‘ndx)
Theorem	slotsdifdsndx 13581	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx))
Theorem	unifndx 13582	Index value of the df-unif 13456 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 13583	Utility theorem: index-independent form of df-unif 13456. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)
Theorem	unifndxnn 13584	The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
⊢ (UnifSet‘ndx) ∈ ℕ
Theorem	basendxltunifndx 13585	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. (Contributed by AV, 28-Oct-2024.)
⊢ (Base‘ndx) < (UnifSet‘ndx)
Theorem	unifndxnbasendx 13586	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 13587	The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.)
⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx)
Theorem	slotsdifunifndx 13588	The index of the slot for the uniform set is not the index of other slots. (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	homndx 13589	Index value of the df-hom 13457 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (Hom ‘ndx) = ;14
Theorem	homid 13590	Utility theorem: index-independent form of df-hom 13457. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ Hom = Slot (Hom ‘ndx)
Theorem	homslid 13591	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
Theorem	ccondx 13592	Index value of the df-cco 13458 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (comp‘ndx) = ;15
Theorem	ccoid 13593	Utility theorem: index-independent form of df-cco 13458. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ comp = Slot (comp‘ndx)
Theorem	ccoslid 13594	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (comp = Slot (comp‘ndx) ∧ (comp‘ndx) ∈ ℕ)
6.1.3  Various definitions used by the structure product
Syntax	crest 13595	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13596	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13597*	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 13598	Define the topology extractor function. This differs from df-tset 13452 when a structure has been restricted using df-iress 13362; 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 13599	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
⊢ ↾t Fn (V × V)
Theorem	topnfn 13600	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ TopOpen Fn V