Theorem List for Intuitionistic Logic Explorer - 11601-11700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | strslssd 11601 |
Deduction version of strslss 11602. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by
Jim Kingdon, 31-Jan-2023.)
|
 Slot            
                       |
|
Theorem | strslss 11602 |
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 11603 |
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 11604 |
The base set of the empty structure. (Contributed by David A. Wheeler,
7-Jul-2016.)
|
     |
|
Theorem | setsslid 11605 |
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 11606 |
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 11607 |
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 11608 |
Utility theorem: index-independent form of df-base 11561. (Contributed by
NM, 20-Oct-2012.)
|
Slot      |
|
Theorem | basendx 11609 |
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 11610 |
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 11611 |
The base set extractor is a slot. (Contributed by Jim Kingdon,
31-Jan-2023.)
|

Slot           |
|
Theorem | basfn 11612 |
The base set extractor is a function on . (Contributed by Stefan
O'Rear, 8-Jul-2015.)
|
 |
|
Theorem | reldmress 11613 |
The structure restriction is a proper operator, so it can be used with
ovprc1 5699. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
↾s |
|
Theorem | ressid2 11614 |
General behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.)
|
 ↾s        
  |
|
Theorem | ressval2 11615 |
Value of nontrivial structure restriction. (Contributed by Stefan
O'Rear, 29-Nov-2014.)
|
 ↾s       
  sSet             |
|
Theorem | ressid 11616 |
Behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.)
|
     
↾s    |
|
5.1.2 Slot definitions
|
|
Syntax | cplusg 11617 |
Extend class notation with group (addition) operation.
|
 |
|
Syntax | cmulr 11618 |
Extend class notation with ring multiplication.
|
 |
|
Syntax | cstv 11619 |
Extend class notation with involution.
|
  |
|
Syntax | csca 11620 |
Extend class notation with scalar field.
|
Scalar |
|
Syntax | cvsca 11621 |
Extend class notation with scalar product.
|
 |
|
Syntax | cip 11622 |
Extend class notation with Hermitian form (inner product).
|
 |
|
Syntax | cts 11623 |
Extend class notation with the topology component of a topological
space.
|
TopSet |
|
Syntax | cple 11624 |
Extend class notation with "less than or equal to" for posets.
|
 |
|
Syntax | coc 11625 |
Extend class notation with the class of orthocomplementation
extractors.
|
 |
|
Syntax | cds 11626 |
Extend class notation with the metric space distance function.
|
 |
|
Syntax | cunif 11627 |
Extend class notation with the uniform structure.
|
 |
|
Syntax | chom 11628 |
Extend class notation with the hom-set structure.
|
 |
|
Syntax | cco 11629 |
Extend class notation with the composition operation.
|
comp |
|
Definition | df-plusg 11630 |
Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
 |
|
Definition | df-mulr 11631 |
Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
 |
|
Definition | df-starv 11632 |
Define the involution function of a *-ring. (Contributed by NM,
4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
 Slot  |
|
Definition | df-sca 11633 |
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 11634 |
Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by
Mario Carneiro, 14-Aug-2015.)
|
Slot
 |
|
Definition | df-ip 11635 |
Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
Slot
 |
|
Definition | df-tset 11636 |
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 11637 |
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 11638 |
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 11639 |
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 11640 |
Define the uniform structure component of a uniform space. (Contributed
by Mario Carneiro, 14-Aug-2015.)
|
Slot ;  |
|
Definition | df-hom 11641 |
Define the hom-set component of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
Slot ;  |
|
Definition | df-cco 11642 |
Define the composition operation of a category. (Contributed by Mario
Carneiro, 2-Jan-2017.)
|
comp Slot ;  |
|
Theorem | strleund 11643 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
 Struct  
  
Struct          Struct      |
|
Theorem | strleun 11644 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
Struct    Struct      Struct     |
|
Theorem | strle1g 11645 |
Make a structure from a singleton. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
      Struct      |
|
Theorem | strle2g 11646 |
Make a structure from a pair. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
            Struct      |
|
Theorem | strle3g 11647 |
Make a structure from a triple. (Contributed by Mario Carneiro,
29-Aug-2015.)
|
                Struct      |
|
Theorem | plusgndx 11648 |
Index value of the df-plusg 11630 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
  
 |
|
Theorem | plusgid 11649 |
Utility theorem: index-independent form of df-plusg 11630. (Contributed by
NM, 20-Oct-2012.)
|
Slot
    |
|
Theorem | plusgslid 11650 |
Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.)
|
 Slot         |
|
Theorem | opelstrsl 11651 |
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
 Slot           Struct                    |
|
Theorem | opelstrbas 11652 |
The base set of a structure with a base set. (Contributed by AV,
10-Nov-2021.)
|
 Struct          
         |
|
Theorem | 1strstrg 11653 |
A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
(Revised by Jim Kingdon, 28-Jan-2023.)
|
          Struct      |
|
Theorem | 1strbas 11654 |
The base set of a constructed one-slot structure. (Contributed by AV,
27-Mar-2020.)
|
                |
|
Theorem | 2strstrg 11655 |
A constructed two-slot structure. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
                Slot    Struct      |
|
Theorem | 2strbasg 11656 |
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 11657 |
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 11658 |
A constructed two-slot structure. Version of 2strstrg 11655 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 11659 |
The base set of a constructed two-slot structure. Version of 2strbasg 11656
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 11660 |
The other slot of a constructed two-slot structure. Version of
2stropg 11657 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 11661 |
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 11662 |
A constructed group is a structure on   .
(Contributed by
Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
                

Struct      |
|
Theorem | grpbaseg 11663 |
The base set of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
                
       |
|
Theorem | grpplusgg 11664 |
The operation of a constructed group. (Contributed by Mario Carneiro,
2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
                

     |
|
Theorem | mulrndx 11665 |
Index value of the df-mulr 11631 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
   
 |
|
Theorem | mulrid 11666 |
Utility theorem: index-independent form of df-mulr 11631. (Contributed by
Mario Carneiro, 8-Jun-2013.)
|
Slot
     |
|
Theorem | mulrslid 11667 |
Slot property of .
(Contributed by Jim Kingdon, 3-Feb-2023.)
|
 Slot           |
|
Theorem | plusgndxnmulrndx 11668 |
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 11669 |
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 11670 |
A constructed ring is a structure. (Contributed by Mario Carneiro,
28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
                        
Struct      |
|
Theorem | rngbaseg 11671 |
The base set of a constructed ring. (Contributed by Mario Carneiro,
2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
                        
      |
|
Theorem | rngplusgg 11672 |
The additive operation of a constructed ring. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
                        
     |
|
Theorem | rngmulrg 11673 |
The multiplicative operation of a constructed ring. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
                        
      |
|
Theorem | starvndx 11674 |
Index value of the df-starv 11632 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
    
 |
|
Theorem | starvid 11675 |
Utility theorem: index-independent form of df-starv 11632. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
 Slot       |
|
Theorem | starvslid 11676 |
Slot property of  . (Contributed by Jim
Kingdon, 4-Feb-2023.)
|
  Slot     
       |
|
Theorem | srngstrd 11677 |
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
      Struct      |
|
Theorem | srngbased 11678 |
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
            |
|
Theorem | srngplusgd 11679 |
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
           |
|
Theorem | srngmulrd 11680 |
The multiplication operation of a constructed star ring. (Contributed
by Mario Carneiro, 20-Jun-2015.)
|
                                   
            |
|
Theorem | srnginvld 11681 |
The involution function of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.)
|
                                   
             |
|
Theorem | scandx 11682 |
Index value of the df-sca 11633 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
Scalar   |
|
Theorem | scaid 11683 |
Utility theorem: index-independent form of scalar df-sca 11633. (Contributed
by Mario Carneiro, 19-Jun-2014.)
|
Scalar Slot Scalar   |
|
Theorem | scaslid 11684 |
Slot property of Scalar. (Contributed by Jim Kingdon,
5-Feb-2023.)
|
Scalar Slot
Scalar  Scalar 
  |
|
Theorem | vscandx 11685 |
Index value of the df-vsca 11634 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
   
 |
|
Theorem | vscaid 11686 |
Utility theorem: index-independent form of scalar product df-vsca 11634.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro,
19-Jun-2014.)
|
Slot
     |
|
Theorem | vscaslid 11687 |
Slot property of .
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
 Slot           |
|
Theorem | lmodstrd 11688 |
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 11689 |
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 11690 |
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 11691 |
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 11692 |
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 11693 |
Index value of the df-ip 11635 slot. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
   
 |
|
Theorem | ipid 11694 |
Utility theorem: index-independent form of df-ip 11635. (Contributed by
Mario Carneiro, 6-Oct-2013.)
|
Slot
     |
|
Theorem | ipslid 11695 |
Slot property of .
(Contributed by Jim Kingdon, 7-Feb-2023.)
|
 Slot           |
|
Theorem | ipsstrd 11696 |
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 11697 |
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 11698 |
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 11699 |
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 11700 |
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    |