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. is the set of indices, the operation, an expression, is normally a free variable in . must be a total order. Its base set may be infinite provided that the "support" is finite. The support is the set: . The base set of may be empty. must be an associative law with a neutral element. (Contributed by FL, 17-Oct-2011.)
Assertion
Ref Expression
df-prod3 prod3
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   ()   ()   ()

Detailed syntax breakdown of Definition df-prod3
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
4 cG . . 3
51, 2, 3, 4cprd3 25404 . 2 prod3
6 cbs 13164 . . . . 5
74, 6cfv 5271 . . . 4
8 c0 3468 . . . 4
97, 8wceq 1632 . . 3
10 c0g 13416 . . . 4
114, 10cfv 5271 . . 3
12 vf . . . . . . . . 9
1312cv 1631 . . . . . . . 8
14 c1 8754 . . . . . . . . . 10
15 vm . . . . . . . . . . 11
1615cv 1631 . . . . . . . . . 10
17 cfz 10798 . . . . . . . . . 10
1814, 16, 17co 5874 . . . . . . . . 9
192, 11wne 2459 . . . . . . . . . 10
201, 6cfv 5271 . . . . . . . . . 10
2119, 3, 20crab 2560 . . . . . . . . 9
22 coriso 25311 . . . . . . . . 9
2318, 21, 22co 5874 . . . . . . . 8
2413, 23wcel 1696 . . . . . . 7
25 vx . . . . . . . . 9
2625cv 1631 . . . . . . . 8
27 cplusg 13224 . . . . . . . . . . 11
284, 27cfv 5271 . . . . . . . . . 10
29 vn . . . . . . . . . . 11
30 cn 9762 . . . . . . . . . . 11
3129cv 1631 . . . . . . . . . . . . 13
3231, 13cfv 5271 . . . . . . . . . . . 12
333, 32, 2csb 3094 . . . . . . . . . . 11
3429, 30, 33cmpt 4093 . . . . . . . . . 10
3528, 34, 14cseq 11062 . . . . . . . . 9
3616, 35cfv 5271 . . . . . . . 8
3726, 36wceq 1632 . . . . . . 7
3824, 37wa 358 . . . . . 6
3938, 12wex 1531 . . . . 5
4039, 15, 30wrex 2557 . . . 4
4140, 25cio 5233 . . 3
429, 11, 41cif 3578 . 2
435, 42wceq 1632 1 prod3
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator