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

Definition df-prod2 25405
 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 . 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: . The base set of may be empty. 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
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   ()   ()   ()

Detailed syntax breakdown of Definition df-prod2
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
4 cG . . 3
51, 2, 3, 4cprd2 25403 . 2 prod2
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 c1 8754 . . . . . . . . 9
13 vm . . . . . . . . . 10
1413cv 1631 . . . . . . . . 9
15 cfz 10798 . . . . . . . . 9
1612, 14, 15co 5874 . . . . . . . 8
172, 11wne 2459 . . . . . . . . 9
181, 6cfv 5271 . . . . . . . . 9
1917, 3, 18crab 2560 . . . . . . . 8
20 vf . . . . . . . . 9
2120cv 1631 . . . . . . . 8
2216, 19, 21wf1o 5270 . . . . . . 7
23 vx . . . . . . . . 9
2423cv 1631 . . . . . . . 8
25 cplusg 13224 . . . . . . . . . . 11
264, 25cfv 5271 . . . . . . . . . 10
27 vn . . . . . . . . . . 11
28 cn 9762 . . . . . . . . . . 11
2927cv 1631 . . . . . . . . . . . . 13
3029, 21cfv 5271 . . . . . . . . . . . 12
313, 30, 2csb 3094 . . . . . . . . . . 11
3227, 28, 31cmpt 4093 . . . . . . . . . 10
3326, 32, 12cseq 11062 . . . . . . . . 9
3414, 33cfv 5271 . . . . . . . 8
3524, 34wceq 1632 . . . . . . 7
3622, 35wa 358 . . . . . 6
3736, 20wex 1531 . . . . 5
3837, 13, 28wrex 2557 . . . 4
3938, 23cio 5233 . . 3
409, 11, 39cif 3578 . 2
415, 40wceq 1632 1 prod2
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator