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 25299
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 12159. 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 25298 . 2  class  prod_ k  e.  A G B
6 c0 3455 . . . 4  class  (/)
71, 6wceq 1623 . . 3  wff  A  =  (/)
8 cgi 20854 . . . 4  class GId
94, 8cfv 5255 . . 3  class  (GId `  G )
10 vm . . . . . . . . . 10  set  m
1110cv 1622 . . . . . . . . 9  class  m
12 vn . . . . . . . . . 10  set  n
1312cv 1622 . . . . . . . . 9  class  n
14 cfz 10782 . . . . . . . . 9  class  ...
1511, 13, 14co 5858 . . . . . . . 8  class  ( m ... n )
161, 15wceq 1623 . . . . . . 7  wff  A  =  ( m ... n
)
17 vx . . . . . . . . 9  set  x
1817cv 1622 . . . . . . . 8  class  x
19 cvv 2788 . . . . . . . . . . 11  class  _V
203, 19, 2cmpt 4077 . . . . . . . . . 10  class  ( k  e.  _V  |->  B )
214, 20, 11cseq 11046 . . . . . . . . 9  class  seq  m
( G ,  ( k  e.  _V  |->  B ) )
2213, 21cfv 5255 . . . . . . . 8  class  (  seq  m ( G , 
( k  e.  _V  |->  B ) ) `  n )
2318, 22wcel 1684 . . . . . . 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 10230 . . . . . . 7  class  ZZ>=
2611, 25cfv 5255 . . . . . 6  class  ( ZZ>= `  m )
2724, 12, 26wrex 2544 . . . . 5  wff  E. n  e.  ( ZZ>= `  m )
( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G ,  ( k  e. 
_V  |->  B ) ) `
 n ) )
2827, 10wex 1528 . . . 4  wff  E. m E. n  e.  ( ZZ>=
`  m ) ( A  =  ( m ... n )  /\  x  e.  (  seq  m ( G , 
( k  e.  _V  |->  B ) ) `  n ) )
2928, 17cab 2269 . . 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 3565 . 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 1623 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  25304  prod0  25305  prodeq1  25306  prodeq2  25307  prodeq3ii  25308  nfprod1  25310  nfprod  25311  cbvprodi  25312  dffprod  25319
  Copyright terms: Public domain W3C validator