Theorem List for Intuitionistic Logic Explorer - 12001-12100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | strslfv2d 12001 |
Deduction version of strslfv 12003. (Contributed by Mario Carneiro,
30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
Slot
|
|
Theorem | strslfv2 12002 |
A variation on strslfv 12003 to avoid asserting that itself is a
function, which involves sethood of all the ordered pair components of
. (Contributed
by Mario Carneiro, 30-Apr-2015.) (Revised by Jim
Kingdon, 30-Jan-2023.)
|
Slot
|
|
Theorem | strslfv 12003 |
Extract a structure component (such as the base set) from a
structure with
a component extractor
(such as the base set
extractor df-base 11965). By virtue of ndxslid 11984, this can be done
without having to refer to the hard-coded numeric index of .
(Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
Struct Slot
|
|
Theorem | strslfv3 12004 |
Variant on strslfv 12003 for large structures. (Contributed by Mario
Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
Struct
Slot
|
|
Theorem | strslssd 12005 |
Deduction version of strslss 12006. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by
Jim Kingdon, 31-Jan-2023.)
|
Slot
|
|
Theorem | strslss 12006 |
Propagate component extraction to a structure from a subset
structure .
(Contributed by Mario Carneiro, 11-Oct-2013.)
(Revised by Jim Kingdon, 31-Jan-2023.)
|
Slot
|
|
Theorem | strsl0 12007 |
All components of the empty set are empty sets. (Contributed by Stefan
O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|
Slot |
|
Theorem | base0 12008 |
The base set of the empty structure. (Contributed by David A. Wheeler,
7-Jul-2016.)
|
|
|
Theorem | setsslid 12009 |
Value of the structure replacement function at a replaced index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
Slot sSet
|
|
Theorem | setsslnid 12010 |
Value of the structure replacement function at an untouched index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
Slot
sSet |
|
Theorem | baseval 12011 |
Value of the base set extractor. (Normally it is preferred to work with
rather than the hard-coded in order to make
structure theorems portable. This is an example of how to obtain it
when needed.) (New usage is discouraged.) (Contributed by NM,
4-Sep-2011.)
|
|
|
Theorem | baseid 12012 |
Utility theorem: index-independent form of df-base 11965. (Contributed by
NM, 20-Oct-2012.)
|
Slot |
|
Theorem | basendx 12013 |
Index value of the base set extractor. (Normally it is preferred to work
with rather than the hard-coded in order to make
structure theorems portable. This is an example of how to obtain it when
needed.) (New usage is discouraged.) (Contributed by Mario Carneiro,
2-Aug-2013.)
|
|
|
Theorem | basendxnn 12014 |
The index value of the base set extractor 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, 23-Sep-2020.)
|
|
|
Theorem | baseslid 12015 |
The base set extractor is a slot. (Contributed by Jim Kingdon,
31-Jan-2023.)
|
Slot |
|
Theorem | basfn 12016 |
The base set extractor is a function on . (Contributed by Stefan
O'Rear, 8-Jul-2015.)
|
|
|
Theorem | reldmress 12017 |
The structure restriction is a proper operator, so it can be used with
ovprc1 5807. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
↾s |
|
Theorem | ressid2 12018 |
General behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.)
|
↾s
|
|
Theorem | ressval2 12019 |
Value of nontrivial structure restriction. (Contributed by Stefan
O'Rear, 29-Nov-2014.)
|
↾s
sSet |
|
Theorem | ressid 12020 |
Behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
↾s |
|
6.1.2 Slot definitions
|
|
Syntax | cplusg 12021 |
Extend class notation with group (addition) operation.
|
|
|
Syntax | cmulr 12022 |
Extend class notation with ring multiplication.
|
|
|
Syntax | cstv 12023 |
Extend class notation with involution.
|
|
|
Syntax | csca 12024 |
Extend class notation with scalar field.
|
Scalar |
|
Syntax | cvsca 12025 |
Extend class notation with scalar product.
|
|
|
Syntax | cip 12026 |
Extend class notation with Hermitian form (inner product).
|
|
|
Syntax | cts 12027 |
Extend class notation with the topology component of a topological
space.
|
TopSet |
|
Syntax | cple 12028 |
Extend class notation with "less than or equal to" for posets.
|
|
|
Syntax | coc 12029 |
Extend class notation with the class of orthocomplementation
extractors.
|
|
|
Syntax | cds 12030 |
Extend class notation with the metric space distance function.
|
|
|
Syntax | cunif 12031 |
Extend class notation with the uniform structure.
|
|
|
Syntax | chom 12032 |
Extend class notation with the hom-set structure.
|
|
|
Syntax | cco 12033 |
Extend class notation with the composition operation.
|
comp |
|
Definition | df-plusg 12034 |
Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-mulr 12035 |
Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-starv 12036 |
Define the involution function of a *-ring. (Contributed by NM,
4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
Slot |
|
Definition | df-sca 12037 |
Define scalar field component of a vector space . (Contributed by
NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
Scalar Slot |
|
Definition | df-vsca 12038 |
Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-ip 12039 |
Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-tset 12040 |
Define the topology component of a topological space (structure).
(Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
TopSet Slot |
|
Definition | df-ple 12041 |
Define "less than or equal to" ordering extractor for posets and
related
structures. We use ; for the index to avoid conflict with
through used for
other purposes. (Contributed by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|
Slot
; |
|
Definition | df-ocomp 12042 |
Define the orthocomplementation extractor for posets and related
structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
Slot
; |
|
Definition | df-ds 12043 |
Define the distance function component of a metric space (structure).
(Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro,
14-Aug-2015.)
|
Slot ; |
|
Definition | df-unif 12044 |
Define the uniform structure component of a uniform space. (Contributed
by Mario Carneiro, 14-Aug-2015.)
|
Slot ; |
|
Definition | df-hom 12045 |
Define the hom-set component of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
Slot ; |
|
Definition | df-cco 12046 |
Define the composition operation of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
comp Slot ; |
|
Theorem | strleund 12047 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct
Struct Struct |
|
Theorem | strleun 12048 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
Struct Struct Struct |
|
Theorem | strle1g 12049 |
Make a structure from a singleton. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct |
|
Theorem | strle2g 12050 |
Make a structure from a pair. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct |
|
Theorem | strle3g 12051 |
Make a structure from a triple. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
Struct |
|
Theorem | plusgndx 12052 |
Index value of the df-plusg 12034 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | plusgid 12053 |
Utility theorem: index-independent form of df-plusg 12034. (Contributed by
NM, 20-Oct-2012.)
|
Slot
|
|
Theorem | plusgslid 12054 |
Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.)
|
Slot |
|
Theorem | opelstrsl 12055 |
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
Slot Struct |
|
Theorem | opelstrbas 12056 |
The base set of a structure with a base set. (Contributed by AV,
10-Nov-2021.)
|
Struct
|
|
Theorem | 1strstrg 12057 |
A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
(Revised by Jim Kingdon, 28-Jan-2023.)
|
Struct |
|
Theorem | 1strbas 12058 |
The base set of a constructed one-slot structure. (Contributed by AV,
27-Mar-2020.)
|
|
|
Theorem | 2strstrg 12059 |
A constructed two-slot structure. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
Slot Struct |
|
Theorem | 2strbasg 12060 |
The base set of a constructed two-slot structure. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
Slot |
|
Theorem | 2stropg 12061 |
The other slot of a constructed two-slot structure. (Contributed by
Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
Slot |
|
Theorem | 2strstr1g 12062 |
A constructed two-slot structure. Version of 2strstrg 12059 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.)
|
Struct
|
|
Theorem | 2strbas1g 12063 |
The base set of a constructed two-slot structure. Version of 2strbasg 12060
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.)
|
|
|
Theorem | 2strop1g 12064 |
The other slot of a constructed two-slot structure. Version of
2stropg 12061 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.)
|
Slot
|
|
Theorem | basendxnplusgndx 12065 |
The slot for the base set is not the slot for the group operation in an
extensible structure. (Contributed by AV, 14-Nov-2021.)
|
|
|
Theorem | grpstrg 12066 |
A constructed group is a structure on .
(Contributed by
Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
Struct |
|
Theorem | grpbaseg 12067 |
The base set of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | grpplusgg 12068 |
The operation of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | mulrndx 12069 |
Index value of the df-mulr 12035 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | mulrid 12070 |
Utility theorem: index-independent form of df-mulr 12035. (Contributed by
Mario Carneiro, 8-Jun-2013.)
|
Slot
|
|
Theorem | mulrslid 12071 |
Slot property of .
(Contributed by Jim Kingdon, 3-Feb-2023.)
|
Slot |
|
Theorem | plusgndxnmulrndx 12072 |
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.)
|
|
|
Theorem | basendxnmulrndx 12073 |
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.)
|
|
|
Theorem | rngstrg 12074 |
A constructed ring is a structure. (Contributed by Mario Carneiro,
28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
Struct |
|
Theorem | rngbaseg 12075 |
The base set of a constructed ring. (Contributed by Mario Carneiro,
2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
|
|
Theorem | rngplusgg 12076 |
The additive operation of a constructed ring. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | rngmulrg 12077 |
The multiplicative operation of a constructed ring. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | starvndx 12078 |
Index value of the df-starv 12036 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | starvid 12079 |
Utility theorem: index-independent form of df-starv 12036. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
Slot |
|
Theorem | starvslid 12080 |
Slot property of . (Contributed by Jim
Kingdon, 4-Feb-2023.)
|
Slot
|
|
Theorem | srngstrd 12081 |
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
Struct |
|
Theorem | srngbased 12082 |
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
|
|
Theorem | srngplusgd 12083 |
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
|
|
Theorem | srngmulrd 12084 |
The multiplication operation of a constructed star ring. (Contributed
by Mario Carneiro, 20-Jun-2015.)
|
|
|
Theorem | srnginvld 12085 |
The involution function of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.)
|
|
|
Theorem | scandx 12086 |
Index value of the df-sca 12037 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
Scalar |
|
Theorem | scaid 12087 |
Utility theorem: index-independent form of scalar df-sca 12037. (Contributed
by Mario Carneiro, 19-Jun-2014.)
|
Scalar Slot Scalar |
|
Theorem | scaslid 12088 |
Slot property of Scalar. (Contributed by Jim Kingdon,
5-Feb-2023.)
|
Scalar Slot
Scalar Scalar
|
|
Theorem | vscandx 12089 |
Index value of the df-vsca 12038 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | vscaid 12090 |
Utility theorem: index-independent form of scalar product df-vsca 12038.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
Slot
|
|
Theorem | vscaslid 12091 |
Slot property of .
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
Slot |
|
Theorem | lmodstrd 12092 |
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.)
|
Scalar
Struct |
|
Theorem | lmodbased 12093 |
The base set of a constructed left vector space. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
Scalar
|
|
Theorem | lmodplusgd 12094 |
The additive operation of a constructed left vector space. (Contributed
by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
6-Feb-2023.)
|
Scalar
|
|
Theorem | lmodscad 12095 |
The set of scalars of a constructed left vector space. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
Scalar
Scalar |
|
Theorem | lmodvscad 12096 |
The scalar product operation of a constructed left vector space.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
Scalar
|
|
Theorem | ipndx 12097 |
Index value of the df-ip 12039 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | ipid 12098 |
Utility theorem: index-independent form of df-ip 12039. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
Slot
|
|
Theorem | ipslid 12099 |
Slot property of .
(Contributed by Jim Kingdon, 7-Feb-2023.)
|
Slot |
|
Theorem | ipsstrd 12100 |
A constructed inner product space is a structure. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
Scalar
Struct |