P. 135 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmodscad 13401	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 13402	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 13403	Index value of the df-ip 13329 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 13404	Utility theorem: index-independent form of df-ip 13329. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipslid 13405	Slot property of ·𝑖. (Contributed by Jim Kingdon, 7-Feb-2023.)
⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ)
Theorem	ipndxnbasendx 13406	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 13407	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 13408	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 13409	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 13410	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 13411	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 13412	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 13413	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 13414	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 13415	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 13416	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 13417	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → 𝐹 = (Scalar‘𝐻))
Theorem	ressvscag 13418	·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → · = ( ·𝑠 ‘𝐻))
Theorem	ressipg 13419	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉) → , = (·𝑖‘𝐻))
Theorem	tsetndx 13420	Index value of the df-tset 13330 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 13421	Utility theorem: index-independent form of df-tset 13330. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetslid 13422	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (TopSet = Slot (TopSet‘ndx) ∧ (TopSet‘ndx) ∈ ℕ)
Theorem	tsetndxnn 13423	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 13424	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 13425	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 13426	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 13427	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 13428	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 13429	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 13430	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 13431	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 13432	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 13433	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 13434	Index value of the df-ple 13331 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ (le‘ndx) = ;10
Theorem	pleid 13435	Utility theorem: self-referencing, index-independent form of df-ple 13331. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	pleslid 13436	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ)
Theorem	plendxnn 13437	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 13438	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 13439	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 13440	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 13441	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 13442	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 13443	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 13444	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 13445	Index value of the df-ocomp 13332 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
⊢ (oc‘ndx) = ;11
Theorem	ocid 13446	Utility theorem: index-independent form of df-ocomp 13332. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ oc = Slot (oc‘ndx)
Theorem	basendxnocndx 13447	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 13448	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 13449	Index value of the df-ds 13333 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 13450	Utility theorem: index-independent form of df-ds 13333. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsslid 13451	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ)
Theorem	dsndxnn 13452	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 13453	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 13454	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 13455	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 13456	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 13457	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 13458	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 13459	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 13460	Index value of the df-unif 13334 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 13461	Utility theorem: index-independent form of df-unif 13334. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)
Theorem	unifndxnn 13462	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 13463	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 13464	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 13465	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 13466	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 13467	Index value of the df-hom 13335 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (Hom ‘ndx) = ;14
Theorem	homid 13468	Utility theorem: index-independent form of df-hom 13335. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ Hom = Slot (Hom ‘ndx)
Theorem	homslid 13469	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
Theorem	ccondx 13470	Index value of the df-cco 13336 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (comp‘ndx) = ;15
Theorem	ccoid 13471	Utility theorem: index-independent form of df-cco 13336. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ comp = Slot (comp‘ndx)
Theorem	ccoslid 13472	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (comp = Slot (comp‘ndx) ∧ (comp‘ndx) ∈ ℕ)
6.1.3  Definition of the structure product
Syntax	crest 13473	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13474	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13475*	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 13476	Define the topology extractor function. This differs from df-tset 13330 when a structure has been restricted using df-iress 13241; 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 13477	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
⊢ ↾t Fn (V × V)
Theorem	topnfn 13478	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ TopOpen Fn V
Theorem	restval 13479*	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 13480*	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 13481	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	restid2 13482	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽)
Theorem	restsspw 13483	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴
Theorem	restid 13484	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	topnvalg 13485	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopSet‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (𝐽 ↾t 𝐵) = (TopOpen‘𝑊))
Theorem	topnidg 13486	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	topnpropgd 13487	The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
Syntax	ctg 13488	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 13489	Extend class notation with a function whose value is a product topology.
class ∏t
Syntax	c0g 13490	Extend class notation with group identity element.
class 0g
Syntax	cgsu 13491	Extend class notation to include finitely supported group sums.
class Σg
Definition	df-0g 13492*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 13493. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.)
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))
Definition	df-igsum 13493*	Define a finite group sum (also called "iterated sum") of a structure. Given 𝐺 Σg 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. 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. 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. 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))
Definition	df-topgen 13494*	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. (Contributed by NM, 16-Jul-2006.)
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})
Definition	df-pt 13495*	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 𝑓(𝑔‘𝑦))}))
Theorem	tgval 13496*	The topology generated by a basis. See also tgval2 14965 and tgval3 14972. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)})
Theorem	tgvalex 13497	The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ∈ V)
Theorem	ptex 13498	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
⊢ (𝐹 ∈ 𝑉 → (∏t‘𝐹) ∈ V)
Syntax	cprds 13499	The function constructing structure products.
class Xs
Syntax	cpws 13500	The function constructing structure powers.
class ↑s