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 34979
 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 34978 . 2 class FinSum
2 vx . . 3 setvar 𝑥
3 vy . . . . . . 7 setvar 𝑦
43cv 1537 . . . . . 6 class 𝑦
5 ccmn 18973 . . . . . 6 class CMnd
64, 5wcel 2111 . . . . 5 wff 𝑦 ∈ CMnd
7 vt . . . . . . . 8 setvar 𝑡
87cv 1537 . . . . . . 7 class 𝑡
9 cbs 16541 . . . . . . . 8 class Base
104, 9cfv 6335 . . . . . . 7 class (Base‘𝑦)
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1537 . . . . . . 7 class 𝑧
138, 10, 12wf 6331 . . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14 cfn 8527 . . . . . 6 class Fin
1513, 7, 14wrex 3071 . . . . 5 wff 𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
166, 15wa 399 . . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
1716, 3, 11copab 5094 . . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18 c1 10576 . . . . . . . . 9 class 1
19 vm . . . . . . . . . 10 setvar 𝑚
2019cv 1537 . . . . . . . . 9 class 𝑚
21 cfz 12939 . . . . . . . . 9 class ...
2218, 20, 21co 7150 . . . . . . . 8 class (1...𝑚)
232cv 1537 . . . . . . . . . 10 class 𝑥
24 c2nd 7692 . . . . . . . . . 10 class 2nd
2523, 24cfv 6335 . . . . . . . . 9 class (2nd𝑥)
2625cdm 5524 . . . . . . . 8 class dom (2nd𝑥)
27 vf . . . . . . . . 9 setvar 𝑓
2827cv 1537 . . . . . . . 8 class 𝑓
2922, 26, 28wf1o 6334 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥)
30 vs . . . . . . . . 9 setvar 𝑠
3130cv 1537 . . . . . . . 8 class 𝑠
32 c1st 7691 . . . . . . . . . . . 12 class 1st
3323, 32cfv 6335 . . . . . . . . . . 11 class (1st𝑥)
34 cplusg 16623 . . . . . . . . . . 11 class +g
3533, 34cfv 6335 . . . . . . . . . 10 class (+g‘(1st𝑥))
36 vn . . . . . . . . . . 11 setvar 𝑛
37 cn 11674 . . . . . . . . . . 11 class
3836cv 1537 . . . . . . . . . . . . 13 class 𝑛
3938, 28cfv 6335 . . . . . . . . . . . 12 class (𝑓𝑛)
4039, 25cfv 6335 . . . . . . . . . . 11 class ((2nd𝑥)‘(𝑓𝑛))
4136, 37, 40cmpt 5112 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛)))
4235, 41, 18cseq 13418 . . . . . . . . 9 class seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))
4320, 42cfv 6335 . . . . . . . 8 class (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4431, 43wceq 1538 . . . . . . 7 wff 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4529, 44wa 399 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4645, 27wex 1781 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
47 cn0 11934 . . . . 5 class 0
4846, 19, 47wrex 3071 . . . 4 wff 𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4948, 30cio 6292 . . 3 class (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)))
502, 17, 49cmpt 5112 . 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
511, 50wceq 1538 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  34980
 Copyright terms: Public domain W3C validator