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

Definition df-prod2 25302
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 may be any extensible structure with a base set. 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 extensible structure with a law commutative, associative with a neutral element. (Contributed by FL, 17-Oct-2011.)
Assertion
Ref Expression
df-prod2  |- prod2 k  e.  A G B  =  if ( ( Base `  G )  =  (/) ,  ( 0g `  G
) ,  ( iota
x E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> { 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-prod2
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, 4cprd2 25300 . 2  class prod2 k  e.  A G B
6 cbs 13148 . . . . 5  class  Base
74, 6cfv 5255 . . . 4  class  ( Base `  G )
8 c0 3455 . . . 4  class  (/)
97, 8wceq 1623 . . 3  wff  ( Base `  G )  =  (/)
10 c0g 13400 . . . 4  class  0g
114, 10cfv 5255 . . 3  class  ( 0g
`  G )
12 c1 8738 . . . . . . . . 9  class  1
13 vm . . . . . . . . . 10  set  m
1413cv 1622 . . . . . . . . 9  class  m
15 cfz 10782 . . . . . . . . 9  class  ...
1612, 14, 15co 5858 . . . . . . . 8  class  ( 1 ... m )
172, 11wne 2446 . . . . . . . . 9  wff  B  =/=  ( 0g `  G
)
181, 6cfv 5255 . . . . . . . . 9  class  ( Base `  A )
1917, 3, 18crab 2547 . . . . . . . 8  class  { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) }
20 vf . . . . . . . . 9  set  f
2120cv 1622 . . . . . . . 8  class  f
2216, 19, 21wf1o 5254 . . . . . . 7  wff  f : ( 1 ... m
)
-1-1-onto-> { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) }
23 vx . . . . . . . . 9  set  x
2423cv 1622 . . . . . . . 8  class  x
25 cplusg 13208 . . . . . . . . . . 11  class  +g
264, 25cfv 5255 . . . . . . . . . 10  class  ( +g  `  G )
27 vn . . . . . . . . . . 11  set  n
28 cn 9746 . . . . . . . . . . 11  class  NN
2927cv 1622 . . . . . . . . . . . . 13  class  n
3029, 21cfv 5255 . . . . . . . . . . . 12  class  ( f `
 n )
313, 30, 2csb 3081 . . . . . . . . . . 11  class  [_ (
f `  n )  /  k ]_ B
3227, 28, 31cmpt 4077 . . . . . . . . . 10  class  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
)
3326, 32, 12cseq 11046 . . . . . . . . 9  class  seq  1
( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) )
3414, 33cfv 5255 . . . . . . . 8  class  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ) `  m )
3524, 34wceq 1623 . . . . . . 7  wff  x  =  (  seq  1 ( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
)
3622, 35wa 358 . . . . . 6  wff  ( f : ( 1 ... m ) -1-1-onto-> { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) }  /\  x  =  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) )
3736, 20wex 1528 . . . . 5  wff  E. f
( f : ( 1 ... m ) -1-1-onto-> { k  e.  ( Base `  A )  |  B  =/=  ( 0g `  G
) }  /\  x  =  (  seq  1
( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
3837, 13, 28wrex 2544 . . . 4  wff  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) }  /\  x  =  (  seq  1
( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) )
3938, 23cio 5217 . . 3  class  ( iota
x E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> { k  e.  ( Base `  A
)  |  B  =/=  ( 0g `  G
) }  /\  x  =  (  seq  1
( ( +g  `  G
) ,  ( n  e.  NN  |->  [_ (
f `  n )  /  k ]_ B
) ) `  m
) ) )
409, 11, 39cif 3565 . 2  class  if ( ( Base `  G
)  =  (/) ,  ( 0g `  G ) ,  ( iota x E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> { k  e.  (
Base `  A )  |  B  =/=  ( 0g `  G ) }  /\  x  =  (  seq  1 ( ( +g  `  G ) ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) ) ) )
415, 40wceq 1623 1  wff prod2 k  e.  A G B  =  if ( ( Base `  G )  =  (/) ,  ( 0g `  G
) ,  ( iota
x E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> { 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