Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prod Unicode version

Definition df-prod 25402
Description: Define the composite for the law  G of a finite sequence of elements whose values are defined by the expression  B and whose set of indices is  A.  A may be empty. It may be thougt as a product (if  G is a multiplication), a sum (if  G is an addition) or whatever. The variable  k is normally a free variable in  B ( i.e.  B can be thought of as  B ( k )). The definition is meaningful when  A is a finite set of sequential integers and  G is an internal operation. Our definition corresponds to the first part of the definition of df-sum 12175. The operation  + has been replaced by the generic operation  G. The reference to the concept of limit has been removed because one wants to use the product in contexts where limits are irrelevant. I could be still more generic and replace  ( m ... n ) by a finite totally ordered set. I would then get the definition given by Bourbaki in the first chapter of the algebra book of his treatise ( A I.3 def.4 ). I don't because the present definition is easier to deal with and because there exists an order isomorphism between any finite totally ordered set and any finite sets of integers. I don't specify anything about  G because nothing is required of  g in the definition of  seq. I hope it will be ok. Otherwise, one could add  G  e.  Magma. (Contributed by FL, 5-Sep-2010.)
Assertion
Ref Expression
df-prod  |-  prod_ k  e.  A G B  =  if ( A  =  (/) ,  (GId `  G
) ,  { x  |  E. m E. n  e.  ( ZZ>= `  m )
( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e. 
_V  |->  B ) ) `
 n ) ) } )
Distinct variable groups:    x, m, n, k    x, A, m, n    x, G, m, n    x, B, m, n
Allowed substitution hints:    A( k)    B( k)    G( k)

Detailed syntax breakdown of Definition df-prod
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  set  k
4 cG . . 3  class  G
51, 2, 3, 4cprd 25401 . 2  class  prod_ k  e.  A G B
6 c0 3468 . . . 4  class  (/)
71, 6wceq 1632 . . 3  wff  A  =  (/)
8 cgi 20870 . . . 4  class GId
94, 8cfv 5271 . . 3  class  (GId `  G )
10 vm . . . . . . . . . 10  set  m
1110cv 1631 . . . . . . . . 9  class  m
12 vn . . . . . . . . . 10  set  n
1312cv 1631 . . . . . . . . 9  class  n
14 cfz 10798 . . . . . . . . 9  class  ...
1511, 13, 14co 5874 . . . . . . . 8  class  ( m ... n )
161, 15wceq 1632 . . . . . . 7  wff  A  =  ( m ... n
)
17 vx . . . . . . . . 9  set  x
1817cv 1631 . . . . . . . 8  class  x
19 cvv 2801 . . . . . . . . . . 11  class  _V
203, 19, 2cmpt 4093 . . . . . . . . . 10  class  ( k  e.  _V  |->  B )
214, 20, 11cseq 11062 . . . . . . . . 9  class  seq  m
( G ,  ( k  e.  _V  |->  B ) )
2213, 21cfv 5271 . . . . . . . 8  class  (  seq  m ( G , 
( k  e.  _V  |->  B ) ) `  n )
2318, 22wcel 1696 . . . . . . 7  wff  x  e.  (  seq  m ( G ,  ( k  e.  _V  |->  B ) ) `  n )
2416, 23wa 358 . . . . . 6  wff  ( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e.  _V  |->  B ) ) `  n ) )
25 cuz 10246 . . . . . . 7  class  ZZ>=
2611, 25cfv 5271 . . . . . 6  class  ( ZZ>= `  m )
2724, 12, 26wrex 2557 . . . . 5  wff  E. n  e.  ( ZZ>= `  m )
( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e. 
_V  |->  B ) ) `
 n ) )
2827, 10wex 1531 . . . 4  wff  E. m E. n  e.  ( ZZ>=
`  m ) ( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G , 
( k  e.  _V  |->  B ) ) `  n ) )
2928, 17cab 2282 . . 3  class  { x  |  E. m E. n  e.  ( ZZ>= `  m )
( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e. 
_V  |->  B ) ) `
 n ) ) }
307, 9, 29cif 3578 . 2  class  if ( A  =  (/) ,  (GId
`  G ) ,  { x  |  E. m E. n  e.  (
ZZ>= `  m ) ( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G , 
( k  e.  _V  |->  B ) ) `  n ) ) } )
315, 30wceq 1632 1  wff  prod_ k  e.  A G B  =  if ( A  =  (/) ,  (GId `  G
) ,  { x  |  E. m E. n  e.  ( ZZ>= `  m )
( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e. 
_V  |->  B ) ) `
 n ) ) } )
Colors of variables: wff set class
This definition is referenced by:  prodex  25407  prod0  25408  prodeq1  25409  prodeq2  25410  prodeq3ii  25411  nfprod1  25413  nfprod  25414  cbvprodi  25415  dffprod  25422
  Copyright terms: Public domain W3C validator