P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2strop1g 12801	The other slot of a constructed two-slot structure. Version of 2stropg 12798 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 12802	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 12803	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 12804	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 12805	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	ressplusgd 12806	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝜑 → 𝐻 = (𝐺 ↾s 𝐴))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → + = (+g‘𝐻))
Theorem	mulrndx 12807	Index value of the df-mulr 12769 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (.r‘ndx) = 3
Theorem	mulridx 12808	Utility theorem: index-independent form of df-mulr 12769. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	mulrslid 12809	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
Theorem	plusgndxnmulrndx 12810	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 12811	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 12812	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 12813	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 12814	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 12815	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 12816	Index value of the df-starv 12770 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 12817	Utility theorem: index-independent form of df-starv 12770. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvslid 12818	Slot property of *𝑟. (Contributed by Jim Kingdon, 4-Feb-2023.)
⊢ (*𝑟 = Slot (*𝑟‘ndx) ∧ (*𝑟‘ndx) ∈ ℕ)
Theorem	starvndxnbasendx 12819	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (Base‘ndx)
Theorem	starvndxnplusgndx 12820	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (+g‘ndx)
Theorem	starvndxnmulrndx 12821	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (.r‘ndx)
Theorem	ressmulrg 12822	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → · = (.r‘𝑆))
Theorem	srngstrd 12823	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 12824	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 12825	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 12826	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 12827	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 12828	Index value of the df-sca 12771 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 12829	Utility theorem: index-independent form of scalar df-sca 12771. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scaslid 12830	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
Theorem	scandxnbasendx 12831	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 12832	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 12833	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 12834	Index value of the df-vsca 12772 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 12835	Utility theorem: index-independent form of scalar product df-vsca 12772. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscandxnbasendx 12836	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 12837	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 12838	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 12839	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 12840	Slot property of ·𝑠. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
Theorem	lmodstrd 12841	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 12842	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 12843	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 12844	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 12845	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 12846	Index value of the df-ip 12773 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 12847	Utility theorem: index-independent form of df-ip 12773. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipslid 12848	Slot property of ·𝑖. (Contributed by Jim Kingdon, 7-Feb-2023.)
⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ)
Theorem	ipndxnbasendx 12849	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 12850	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 12851	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 12852	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 12853	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 12854	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 12855	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 12856	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 12857	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 12858	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 12859	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 12860	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → 𝐹 = (Scalar‘𝐻))
Theorem	ressvscag 12861	·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → · = ( ·𝑠 ‘𝐻))
Theorem	ressipg 12862	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → , = (·𝑖‘𝐻))
Theorem	tsetndx 12863	Index value of the df-tset 12774 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 12864	Utility theorem: index-independent form of df-tset 12774. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetslid 12865	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (TopSet = Slot (TopSet‘ndx) ∧ (TopSet‘ndx) ∈ ℕ)
Theorem	tsetndxnn 12866	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 12867	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 12868	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 12869	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 12870	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 12871	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 12872	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 12873	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 12874	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 12875	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 12876	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 12877	Index value of the df-ple 12775 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ (le‘ndx) = ;10
Theorem	pleid 12878	Utility theorem: self-referencing, index-independent form of df-ple 12775. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	pleslid 12879	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ)
Theorem	plendxnn 12880	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 12881	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 12882	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 12883	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 12884	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 12885	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 12886	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 12887	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	dsndx 12888	Index value of the df-ds 12777 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 12889	Utility theorem: index-independent form of df-ds 12777. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsslid 12890	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ)
Theorem	dsndxnn 12891	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 12892	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 12893	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 12894	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 12895	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 12896	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 12897	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 12898	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 12899	Index value of the df-unif 12778 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 12900	Utility theorem: index-independent form of df-unif 12778. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)