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 36468
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 36467 . 2 class FinSum
2 vx . . 3 setvar 𝑥
3 vy . . . . . . 7 setvar 𝑦
43cv 1538 . . . . . 6 class 𝑦
5 ccmn 19689 . . . . . 6 class CMnd
64, 5wcel 2104 . . . . 5 wff 𝑦 ∈ CMnd
7 vt . . . . . . . 8 setvar 𝑡
87cv 1538 . . . . . . 7 class 𝑡
9 cbs 17148 . . . . . . . 8 class Base
104, 9cfv 6542 . . . . . . 7 class (Base‘𝑦)
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1538 . . . . . . 7 class 𝑧
138, 10, 12wf 6538 . . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14 cfn 8941 . . . . . 6 class Fin
1513, 7, 14wrex 3068 . . . . 5 wff 𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
166, 15wa 394 . . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
1716, 3, 11copab 5209 . . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18 c1 11113 . . . . . . . . 9 class 1
19 vm . . . . . . . . . 10 setvar 𝑚
2019cv 1538 . . . . . . . . 9 class 𝑚
21 cfz 13488 . . . . . . . . 9 class ...
2218, 20, 21co 7411 . . . . . . . 8 class (1...𝑚)
232cv 1538 . . . . . . . . . 10 class 𝑥
24 c2nd 7976 . . . . . . . . . 10 class 2nd
2523, 24cfv 6542 . . . . . . . . 9 class (2nd𝑥)
2625cdm 5675 . . . . . . . 8 class dom (2nd𝑥)
27 vf . . . . . . . . 9 setvar 𝑓
2827cv 1538 . . . . . . . 8 class 𝑓
2922, 26, 28wf1o 6541 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥)
30 vs . . . . . . . . 9 setvar 𝑠
3130cv 1538 . . . . . . . 8 class 𝑠
32 c1st 7975 . . . . . . . . . . . 12 class 1st
3323, 32cfv 6542 . . . . . . . . . . 11 class (1st𝑥)
34 cplusg 17201 . . . . . . . . . . 11 class +g
3533, 34cfv 6542 . . . . . . . . . 10 class (+g‘(1st𝑥))
36 vn . . . . . . . . . . 11 setvar 𝑛
37 cn 12216 . . . . . . . . . . 11 class
3836cv 1538 . . . . . . . . . . . . 13 class 𝑛
3938, 28cfv 6542 . . . . . . . . . . . 12 class (𝑓𝑛)
4039, 25cfv 6542 . . . . . . . . . . 11 class ((2nd𝑥)‘(𝑓𝑛))
4136, 37, 40cmpt 5230 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛)))
4235, 41, 18cseq 13970 . . . . . . . . 9 class seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))
4320, 42cfv 6542 . . . . . . . 8 class (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4431, 43wceq 1539 . . . . . . 7 wff 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4529, 44wa 394 . . . . . 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 12476 . . . . 5 class 0
4846, 19, 47wrex 3068 . . . 4 wff 𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4948, 30cio 6492 . . 3 class (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)))
502, 17, 49cmpt 5230 . 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
511, 50wceq 1539 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  36469
  Copyright terms: Public domain W3C validator