Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-finsum Structured version   Visualization version   GIF version

Definition df-bj-finsum 37285
Description: Finite summation in commutative monoids. This finite summation function can be extended to pairs 𝑦, 𝑧 where 𝑦 is a left-unital magma and 𝑧 is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.)
Assertion
Ref Expression
df-bj-finsum FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑡,𝑠,𝑓,𝑚,𝑛

Detailed syntax breakdown of Definition df-bj-finsum
StepHypRef Expression
1 cfinsum 37284 . 2 class FinSum
2 vx . . 3 setvar 𝑥
3 vy . . . . . . 7 setvar 𝑦
43cv 1539 . . . . . 6 class 𝑦
5 ccmn 19798 . . . . . 6 class CMnd
64, 5wcel 2108 . . . . 5 wff 𝑦 ∈ CMnd
7 vt . . . . . . . 8 setvar 𝑡
87cv 1539 . . . . . . 7 class 𝑡
9 cbs 17247 . . . . . . . 8 class Base
104, 9cfv 6561 . . . . . . 7 class (Base‘𝑦)
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1539 . . . . . . 7 class 𝑧
138, 10, 12wf 6557 . . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14 cfn 8985 . . . . . 6 class Fin
1513, 7, 14wrex 3070 . . . . 5 wff 𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
166, 15wa 395 . . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
1716, 3, 11copab 5205 . . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18 c1 11156 . . . . . . . . 9 class 1
19 vm . . . . . . . . . 10 setvar 𝑚
2019cv 1539 . . . . . . . . 9 class 𝑚
21 cfz 13547 . . . . . . . . 9 class ...
2218, 20, 21co 7431 . . . . . . . 8 class (1...𝑚)
232cv 1539 . . . . . . . . . 10 class 𝑥
24 c2nd 8013 . . . . . . . . . 10 class 2nd
2523, 24cfv 6561 . . . . . . . . 9 class (2nd𝑥)
2625cdm 5685 . . . . . . . 8 class dom (2nd𝑥)
27 vf . . . . . . . . 9 setvar 𝑓
2827cv 1539 . . . . . . . 8 class 𝑓
2922, 26, 28wf1o 6560 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥)
30 vs . . . . . . . . 9 setvar 𝑠
3130cv 1539 . . . . . . . 8 class 𝑠
32 c1st 8012 . . . . . . . . . . . 12 class 1st
3323, 32cfv 6561 . . . . . . . . . . 11 class (1st𝑥)
34 cplusg 17297 . . . . . . . . . . 11 class +g
3533, 34cfv 6561 . . . . . . . . . 10 class (+g‘(1st𝑥))
36 vn . . . . . . . . . . 11 setvar 𝑛
37 cn 12266 . . . . . . . . . . 11 class
3836cv 1539 . . . . . . . . . . . . 13 class 𝑛
3938, 28cfv 6561 . . . . . . . . . . . 12 class (𝑓𝑛)
4039, 25cfv 6561 . . . . . . . . . . 11 class ((2nd𝑥)‘(𝑓𝑛))
4136, 37, 40cmpt 5225 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛)))
4235, 41, 18cseq 14042 . . . . . . . . 9 class seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))
4320, 42cfv 6561 . . . . . . . 8 class (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4431, 43wceq 1540 . . . . . . 7 wff 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4529, 44wa 395 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4645, 27wex 1779 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
47 cn0 12526 . . . . 5 class 0
4846, 19, 47wrex 3070 . . . 4 wff 𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4948, 30cio 6512 . . 3 class (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)))
502, 17, 49cmpt 5225 . 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
511, 50wceq 1540 1 wff FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
Colors of variables: wff setvar class
This definition is referenced by:  bj-finsumval0  37286
  Copyright terms: Public domain W3C validator