P. 173 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17201-17300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	plusgndxnmulrndx 17201	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	rngstr 17202	A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ 𝑅 Struct ⟨1, 3⟩
Theorem	rngbase 17203	The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝑅))
Theorem	rngplusg 17204	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	rngmulr 17205	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 17206	Index value of the df-starv 17176 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 17207	Utility theorem: index-independent form of df-starv 17176. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvndxnbasendx 17208	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17212. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (Base‘ndx)
Theorem	starvndxnplusgndx 17209	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17212. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (+g‘ndx)
Theorem	starvndxnmulrndx 17210	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17212. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (.r‘ndx)
Theorem	ressmulr 17211	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆))
Theorem	ressstarv 17212	*𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ ∗ = (*𝑟‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆))
Theorem	srngstr 17213	A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ 𝑅 Struct ⟨1, 4⟩
Theorem	srngbase 17214	The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑅))
Theorem	srngplusg 17215	The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ ( + ∈ 𝑋 → + = (+g‘𝑅))
Theorem	srngmulr 17216	The multiplication operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ ( · ∈ 𝑋 → · = (.r‘𝑅))
Theorem	srnginvl 17217	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 17218	Index value of the df-sca 17177 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 17219	Utility theorem: index-independent form of scalar df-sca 17177. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scandxnbasendx 17220	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 17221	The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 20064. (Contributed by AV, 18-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (+g‘ndx)
Theorem	scandxnmulrndx 17222	The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 20064. (Contributed by AV, 29-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (.r‘ndx)
Theorem	vscandx 17223	Index value of the df-vsca 17178 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 17224	Utility theorem: index-independent form of scalar product df-vsca 17178. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscandxnbasendx 17225	The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20863. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx)
Theorem	vscandxnplusgndx 17226	The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20863. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx)
Theorem	vscandxnmulrndx 17227	The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for rmodislmod 20863. (Contributed by AV, 29-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx)
Theorem	vscandxnscandx 17228	The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20863. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
Theorem	lmodstr 17229	A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ 𝑊 Struct ⟨1, 6⟩
Theorem	lmodbase 17230	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊))
Theorem	lmodplusg 17231	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊))
Theorem	lmodsca 17232	The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (𝐹 ∈ 𝑋 → 𝐹 = (Scalar‘𝑊))
Theorem	lmodvsca 17233	The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( · ∈ 𝑋 → · = ( ·𝑠 ‘𝑊))
Theorem	ipndx 17234	Index value of the df-ip 17179 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 17235	Utility theorem: index-independent form of df-ip 17179. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipndxnbasendx 17236	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 17237	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 17238	The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 20064. (Contributed by AV, 29-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (.r‘ndx)
Theorem	slotsdifipndx 17239	The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 21114 and sravsca 21115. (Contributed by AV, 12-Nov-2024.)
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx))
Theorem	ipsstr 17240	Lemma to shorten proofs of ipsbase 17241 through ipsvsca 17245. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ 𝐴 Struct ⟨1, 8⟩
Theorem	ipsbase 17241	The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐴))
Theorem	ipsaddg 17242	The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ ( + ∈ 𝑉 → + = (+g‘𝐴))
Theorem	ipsmulr 17243	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ ( × ∈ 𝑉 → × = (.r‘𝐴))
Theorem	ipssca 17244	The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴))
Theorem	ipsvsca 17245	The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴))
Theorem	ipsip 17246	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐼 = (·𝑖‘𝐴))
Theorem	resssca 17247	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻))
Theorem	ressvsca 17248	·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	ressip 17249	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻))
Theorem	phlstr 17250	A constructed pre-Hilbert space is a structure. Starting from lmodstr 17229 (which has 4 members), we chain strleun 17068 once more, adding an ordered pair to the function, to get all 5 members. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐻 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑇⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})    ⇒   ⊢ 𝐻 Struct ⟨1, 8⟩
Theorem	phlbase 17251	The base set 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), , ⟩})    ⇒   ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝐻))
Theorem	phlplusg 17252	The additive 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), , ⟩})    ⇒   ⊢ ( + ∈ 𝑋 → + = (+g‘𝐻))
Theorem	phlsca 17253	The ring of scalars 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), , ⟩})    ⇒   ⊢ (𝑇 ∈ 𝑋 → 𝑇 = (Scalar‘𝐻))
Theorem	phlvsca 17254	The scalar product 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	phlip 17255	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 17256	Index value of the df-tset 17180 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 17257	Utility theorem: index-independent form of df-tset 17180. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetndxnn 17258	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 17259	The index of the slot for the base set is less than the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
⊢ (Base‘ndx) < (TopSet‘ndx)
Theorem	tsetndxnbasendx 17260	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 17261	The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19264. (Contributed by AV, 18-Oct-2024.)
⊢ (TopSet‘ndx) ≠ (+g‘ndx)
Theorem	tsetndxnmulrndx 17262	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 17263	The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 21306. (Contributed by AV, 11-Nov-2024.)
⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx)
Theorem	slotstnscsi 17264	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 21110 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx))
Theorem	topgrpstr 17265	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 17266	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊))
Theorem	topgrpplusg 17267	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊))
Theorem	topgrptset 17268	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊))
Theorem	resstset 17269	TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐽 = (TopSet‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻))
Theorem	plendx 17270	Index value of the df-ple 17181 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.)
⊢ (le‘ndx) = ;10
Theorem	pleid 17271	Utility theorem: self-referencing, index-independent form of df-ple 17181. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	plendxnn 17272	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 17273	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 17274	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 17275	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 19279. (Contributed by AV, 18-Oct-2024.)
⊢ (le‘ndx) ≠ (+g‘ndx)
Theorem	plendxnmulrndx 17276	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 21987. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (.r‘ndx)
Theorem	plendxnscandx 17277	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 21989. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ (Scalar‘ndx)
Theorem	plendxnvscandx 17278	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 21988. (Contributed by AV, 1-Nov-2024.)
⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx)
Theorem	slotsdifplendx 17279	The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21306. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx))
Theorem	otpsstr 17280	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 17281	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 17282	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 17283	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 17284	le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ 𝑊 = (𝐾 ↾s 𝐴)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊))
Theorem	ocndx 17285	Index value of the df-ocomp 17182 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
⊢ (oc‘ndx) = ;11
Theorem	ocid 17286	Utility theorem: index-independent form of df-ocomp 17182. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ oc = Slot (oc‘ndx)
Theorem	basendxnocndx 17287	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21633. (Contributed by AV, 11-Nov-2024.)
⊢ (Base‘ndx) ≠ (oc‘ndx)
Theorem	plendxnocndx 17288	The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21634. (Contributed by AV, 11-Nov-2024.)
⊢ (le‘ndx) ≠ (oc‘ndx)
Theorem	dsndx 17289	Index value of the df-ds 17183 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 17290	Utility theorem: index-independent form of df-ds 17183. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsndxnn 17291	The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 24397. (Contributed by AV, 28-Oct-2024.)
⊢ (dist‘ndx) ∈ ℕ
Theorem	basendxltdsndx 17292	The index of the slot for the base set is less than the index of the slot for the distance in an extensible structure. Formerly part of proof for tmslem 24397. (Contributed by AV, 28-Oct-2024.)
⊢ (Base‘ndx) < (dist‘ndx)
Theorem	dsndxnbasendx 17293	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 17294	The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 20067. (Contributed by AV, 18-Oct-2024.)
⊢ (dist‘ndx) ≠ (+g‘ndx)
Theorem	dsndxnmulrndx 17295	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 17296	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 21110 and proofs using it. (Contributed by AV, 29-Oct-2024.)
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx))
Theorem	dsndxntsetndx 17297	The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 24563. (Contributed by AV, 29-Oct-2024.)
⊢ (dist‘ndx) ≠ (TopSet‘ndx)
Theorem	slotsdifdsndx 17298	The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21306. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx))
Theorem	unifndx 17299	Index value of the df-unif 17184 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 17300	Utility theorem: index-independent form of df-unif 17184. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)