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

Definition df-prod3 25406
Description: Definition of a sum or product operator to be used with generic structures defined by extensible structures.  A is the set of indices,  G the operation,  B an expression,  k is normally a free variable in  B.  A must be a total order. Its base set may be infinite provided that the "support" is finite. The support is the set:  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) }. The base set of  A may be empty.  G must be an associative law with a neutral element. (Contributed by FL, 17-Oct-2011.)
Assertion
Ref Expression
df-prod3  |- prod3 k  e.  A G B  =  if ( ( Base `  G )  =  (/) ,  ( 0g `  G
) ,  ( iota
x E. m  e.  NN  E. f ( f  e.  ( ( 1 ... m ) 
OrIso  { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) } )  /\  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) ) ) )
Distinct variable groups:    f, m, n, x, A    B, f, m, n, x    f, k, m, n, x    f, G, m, n, x
Allowed substitution hints:    A( k)    B( k)    G( k)

Detailed syntax breakdown of Definition df-prod3
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, 4cprd3 25404 . 2  class prod3 k  e.  A G B
6 cbs 13164 . . . . 5  class  Base
74, 6cfv 5271 . . . 4  class  ( Base `  G )
8 c0 3468 . . . 4  class  (/)
97, 8wceq 1632 . . 3  wff  ( Base `  G )  =  (/)
10 c0g 13416 . . . 4  class  0g
114, 10cfv 5271 . . 3  class  ( 0g
`  G )
12 vf . . . . . . . . 9  set  f
1312cv 1631 . . . . . . . 8  class  f
14 c1 8754 . . . . . . . . . 10  class  1
15 vm . . . . . . . . . . 11  set  m
1615cv 1631 . . . . . . . . . 10  class  m
17 cfz 10798 . . . . . . . . . 10  class  ...
1814, 16, 17co 5874 . . . . . . . . 9  class  ( 1 ... m )
192, 11wne 2459 . . . . . . . . . 10  wff  B  =/=  ( 0g `  G
)
201, 6cfv 5271 . . . . . . . . . 10  class  ( Base `  A )
2119, 3, 20crab 2560 . . . . . . . . 9  class  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) }
22 coriso 25311 . . . . . . . . 9  class  OrIso
2318, 21, 22co 5874 . . . . . . . 8  class  ( ( 1 ... m ) 
OrIso  { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) } )
2413, 23wcel 1696 . . . . . . 7  wff  f  e.  ( ( 1 ... m )  OrIso  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) } )
25 vx . . . . . . . . 9  set  x
2625cv 1631 . . . . . . . 8  class  x
27 cplusg 13224 . . . . . . . . . . 11  class  +g
284, 27cfv 5271 . . . . . . . . . 10  class  ( +g  `  G )
29 vn . . . . . . . . . . 11  set  n
30 cn 9762 . . . . . . . . . . 11  class  NN
3129cv 1631 . . . . . . . . . . . . 13  class  n
3231, 13cfv 5271 . . . . . . . . . . . 12  class  ( f `
 n )
333, 32, 2csb 3094 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
3429, 30, 33cmpt 4093 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
3528, 34, 14cseq 11062 . . . . . . . . 9  class  seq  1
( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) )
3616, 35cfv 5271 . . . . . . . 8  class  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
3726, 36wceq 1632 . . . . . . 7  wff  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
3824, 37wa 358 . . . . . 6  wff  ( f  e.  ( ( 1 ... m )  OrIso  { k  e.  ( Base `  A )  |  B  =/=  ( 0g `  G
) } )  /\  x  =  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) )
3938, 12wex 1531 . . . . 5  wff  E. f
( f  e.  ( ( 1 ... m
)  OrIso  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) } )  /\  x  =  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) )
4039, 15, 30wrex 2557 . . . 4  wff  E. m  e.  NN  E. f ( f  e.  ( ( 1 ... m ) 
OrIso  { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) } )  /\  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
4140, 25cio 5233 . . 3  class  ( iota
x E. m  e.  NN  E. f ( f  e.  ( ( 1 ... m ) 
OrIso  { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) } )  /\  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) ) )
429, 11, 41cif 3578 . 2  class  if ( ( Base `  G
)  =  (/) ,  ( 0g `  G ) ,  ( iota x E. m  e.  NN  E. f ( f  e.  ( ( 1 ... m )  OrIso  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) } )  /\  x  =  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m ) ) ) )
435, 42wceq 1632 1  wff prod3 k  e.  A G B  =  if ( ( Base `  G )  =  (/) ,  ( 0g `  G
) ,  ( iota
x E. m  e.  NN  E. f ( f  e.  ( ( 1 ... m ) 
OrIso  { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) } )  /\  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator