Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | cstv 12401 |
Extend class notation with involution.
|
|
|
Syntax | csca 12402 |
Extend class notation with scalar field.
|
Scalar |
|
Syntax | cvsca 12403 |
Extend class notation with scalar product.
|
|
|
Syntax | cip 12404 |
Extend class notation with Hermitian form (inner product).
|
|
|
Syntax | cts 12405 |
Extend class notation with the topology component of a topological
space.
|
TopSet |
|
Syntax | cple 12406 |
Extend class notation with "less than or equal to" for posets.
|
|
|
Syntax | coc 12407 |
Extend class notation with the class of orthocomplementation
extractors.
|
|
|
Syntax | cds 12408 |
Extend class notation with the metric space distance function.
|
|
|
Syntax | cunif 12409 |
Extend class notation with the uniform structure.
|
|
|
Syntax | chom 12410 |
Extend class notation with the hom-set structure.
|
|
|
Syntax | cco 12411 |
Extend class notation with the composition operation.
|
comp |
|
Definition | df-plusg 12412 |
Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-mulr 12413 |
Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-starv 12414 |
Define the involution function of a *-ring. (Contributed by NM,
4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
Slot |
|
Definition | df-sca 12415 |
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 12416 |
Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-ip 12417 |
Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
Slot
|
|
Definition | df-tset 12418 |
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 12419 |
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 12420 |
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 12421 |
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 12422 |
Define the uniform structure component of a uniform space. (Contributed
by Mario Carneiro, 14-Aug-2015.)
|
Slot ; |
|
Definition | df-hom 12423 |
Define the hom-set component of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
Slot ; |
|
Definition | df-cco 12424 |
Define the composition operation of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
comp Slot ; |
|
Theorem | strleund 12425 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct
Struct Struct |
|
Theorem | strleun 12426 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
Struct Struct Struct |
|
Theorem | strle1g 12427 |
Make a structure from a singleton. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct |
|
Theorem | strle2g 12428 |
Make a structure from a pair. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
Struct |
|
Theorem | strle3g 12429 |
Make a structure from a triple. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
Struct |
|
Theorem | plusgndx 12430 |
Index value of the df-plusg 12412 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | plusgid 12431 |
Utility theorem: index-independent form of df-plusg 12412. (Contributed by
NM, 20-Oct-2012.)
|
Slot
|
|
Theorem | plusgslid 12432 |
Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.)
|
Slot |
|
Theorem | opelstrsl 12433 |
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
Slot Struct |
|
Theorem | opelstrbas 12434 |
The base set of a structure with a base set. (Contributed by AV,
10-Nov-2021.)
|
Struct
|
|
Theorem | 1strstrg 12435 |
A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
(Revised by Jim Kingdon, 28-Jan-2023.)
|
Struct |
|
Theorem | 1strbas 12436 |
The base set of a constructed one-slot structure. (Contributed by AV,
27-Mar-2020.)
|
|
|
Theorem | 2strstrg 12437 |
A constructed two-slot structure. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
Slot Struct |
|
Theorem | 2strbasg 12438 |
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 12439 |
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 12440 |
A constructed two-slot structure. Version of 2strstrg 12437 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 12441 |
The base set of a constructed two-slot structure. Version of 2strbasg 12438
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 12442 |
The other slot of a constructed two-slot structure. Version of
2stropg 12439 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 12443 |
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 12444 |
A constructed group is a structure on .
(Contributed by
Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
Struct |
|
Theorem | grpbaseg 12445 |
The base set of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | grpplusgg 12446 |
The operation of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | mulrndx 12447 |
Index value of the df-mulr 12413 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | mulrid 12448 |
Utility theorem: index-independent form of df-mulr 12413. (Contributed by
Mario Carneiro, 8-Jun-2013.)
|
Slot
|
|
Theorem | mulrslid 12449 |
Slot property of .
(Contributed by Jim Kingdon, 3-Feb-2023.)
|
Slot |
|
Theorem | plusgndxnmulrndx 12450 |
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 12451 |
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 12452 |
A constructed ring is a structure. (Contributed by Mario Carneiro,
28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
Struct |
|
Theorem | rngbaseg 12453 |
The base set of a constructed ring. (Contributed by Mario Carneiro,
2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
|
|
Theorem | rngplusgg 12454 |
The additive operation of a constructed ring. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | rngmulrg 12455 |
The multiplicative operation of a constructed ring. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
|
|
Theorem | starvndx 12456 |
Index value of the df-starv 12414 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | starvid 12457 |
Utility theorem: index-independent form of df-starv 12414. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
Slot |
|
Theorem | starvslid 12458 |
Slot property of . (Contributed by Jim
Kingdon, 4-Feb-2023.)
|
Slot
|
|
Theorem | srngstrd 12459 |
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
Struct |
|
Theorem | srngbased 12460 |
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
|
|
Theorem | srngplusgd 12461 |
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
|
|
Theorem | srngmulrd 12462 |
The multiplication operation of a constructed star ring. (Contributed
by Mario Carneiro, 20-Jun-2015.)
|
|
|
Theorem | srnginvld 12463 |
The involution function of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.)
|
|
|
Theorem | scandx 12464 |
Index value of the df-sca 12415 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
Scalar |
|
Theorem | scaid 12465 |
Utility theorem: index-independent form of scalar df-sca 12415. (Contributed
by Mario Carneiro, 19-Jun-2014.)
|
Scalar Slot Scalar |
|
Theorem | scaslid 12466 |
Slot property of Scalar. (Contributed by Jim Kingdon,
5-Feb-2023.)
|
Scalar Slot
Scalar Scalar
|
|
Theorem | vscandx 12467 |
Index value of the df-vsca 12416 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | vscaid 12468 |
Utility theorem: index-independent form of scalar product df-vsca 12416.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
Slot
|
|
Theorem | vscaslid 12469 |
Slot property of .
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
Slot |
|
Theorem | lmodstrd 12470 |
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 12471 |
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 12472 |
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 12473 |
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 12474 |
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 12475 |
Index value of the df-ip 12417 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
|
|
Theorem | ipid 12476 |
Utility theorem: index-independent form of df-ip 12417. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
Slot
|
|
Theorem | ipslid 12477 |
Slot property of .
(Contributed by Jim Kingdon, 7-Feb-2023.)
|
Slot |
|
Theorem | ipsstrd 12478 |
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 |
|
Theorem | ipsbased 12479 |
The base set of a constructed inner product space. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
Scalar
|
|
Theorem | ipsaddgd 12480 |
The additive operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
Scalar
|
|
Theorem | ipsmulrd 12481 |
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
Scalar
|
|
Theorem | ipsscad 12482 |
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.)
|
Scalar
Scalar |
|
Theorem | ipsvscad 12483 |
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.)
|
Scalar
|
|
Theorem | ipsipd 12484 |
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
8-Feb-2023.)
|
Scalar
|
|
Theorem | tsetndx 12485 |
Index value of the df-tset 12418 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
TopSet |
|
Theorem | tsetid 12486 |
Utility theorem: index-independent form of df-tset 12418. (Contributed by
NM, 20-Oct-2012.)
|
TopSet Slot TopSet |
|
Theorem | tsetslid 12487 |
Slot property of TopSet. (Contributed by Jim Kingdon,
9-Feb-2023.)
|
TopSet Slot
TopSet TopSet
|
|
Theorem | topgrpstrd 12488 |
A constructed topological group is a structure. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
TopSet
Struct |
|
Theorem | topgrpbasd 12489 |
The base set of a constructed topological group. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
TopSet
|
|
Theorem | topgrpplusgd 12490 |
The additive operation of a constructed topological group. (Contributed
by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon,
9-Feb-2023.)
|
TopSet
|
|
Theorem | topgrptsetd 12491 |
The topology of a constructed topological group. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
TopSet
TopSet |
|
Theorem | plendx 12492 |
Index value of the df-ple 12419 slot. (Contributed by Mario Carneiro,
14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|
; |
|
Theorem | pleid 12493 |
Utility theorem: self-referencing, index-independent form of df-ple 12419.
(Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|
Slot
|
|
Theorem | pleslid 12494 |
Slot property of .
(Contributed by Jim Kingdon, 9-Feb-2023.)
|
Slot |
|
Theorem | dsndx 12495 |
Index value of the df-ds 12421 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
; |
|
Theorem | dsid 12496 |
Utility theorem: index-independent form of df-ds 12421. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
Slot |
|
Theorem | dsslid 12497 |
Slot property of . (Contributed by Jim Kingdon, 6-May-2023.)
|
Slot |
|
6.1.3 Definition of the structure
product
|
|
Syntax | crest 12498 |
Extend class notation with the function returning a subspace topology.
|
↾t |
|
Syntax | ctopn 12499 |
Extend class notation with the topology extractor function.
|
|
|
Definition | df-rest 12500* |
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
|