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 36160
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 36159 . 2 class FinSum
2 vx . . 3 setvar 𝑥
3 vy . . . . . . 7 setvar 𝑦
43cv 1540 . . . . . 6 class 𝑦
5 ccmn 19647 . . . . . 6 class CMnd
64, 5wcel 2106 . . . . 5 wff 𝑦 ∈ CMnd
7 vt . . . . . . . 8 setvar 𝑡
87cv 1540 . . . . . . 7 class 𝑡
9 cbs 17143 . . . . . . . 8 class Base
104, 9cfv 6543 . . . . . . 7 class (Base‘𝑦)
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1540 . . . . . . 7 class 𝑧
138, 10, 12wf 6539 . . . . . 6 wff 𝑧:𝑡⟶(Base‘𝑦)
14 cfn 8938 . . . . . 6 class Fin
1513, 7, 14wrex 3070 . . . . 5 wff 𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)
166, 15wa 396 . . . 4 wff (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))
1716, 3, 11copab 5210 . . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}
18 c1 11110 . . . . . . . . 9 class 1
19 vm . . . . . . . . . 10 setvar 𝑚
2019cv 1540 . . . . . . . . 9 class 𝑚
21 cfz 13483 . . . . . . . . 9 class ...
2218, 20, 21co 7408 . . . . . . . 8 class (1...𝑚)
232cv 1540 . . . . . . . . . 10 class 𝑥
24 c2nd 7973 . . . . . . . . . 10 class 2nd
2523, 24cfv 6543 . . . . . . . . 9 class (2nd𝑥)
2625cdm 5676 . . . . . . . 8 class dom (2nd𝑥)
27 vf . . . . . . . . 9 setvar 𝑓
2827cv 1540 . . . . . . . 8 class 𝑓
2922, 26, 28wf1o 6542 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥)
30 vs . . . . . . . . 9 setvar 𝑠
3130cv 1540 . . . . . . . 8 class 𝑠
32 c1st 7972 . . . . . . . . . . . 12 class 1st
3323, 32cfv 6543 . . . . . . . . . . 11 class (1st𝑥)
34 cplusg 17196 . . . . . . . . . . 11 class +g
3533, 34cfv 6543 . . . . . . . . . 10 class (+g‘(1st𝑥))
36 vn . . . . . . . . . . 11 setvar 𝑛
37 cn 12211 . . . . . . . . . . 11 class
3836cv 1540 . . . . . . . . . . . . 13 class 𝑛
3938, 28cfv 6543 . . . . . . . . . . . 12 class (𝑓𝑛)
4039, 25cfv 6543 . . . . . . . . . . 11 class ((2nd𝑥)‘(𝑓𝑛))
4136, 37, 40cmpt 5231 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛)))
4235, 41, 18cseq 13965 . . . . . . . . 9 class seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))
4320, 42cfv 6543 . . . . . . . 8 class (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4431, 43wceq 1541 . . . . . . 7 wff 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)
4529, 44wa 396 . . . . . 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 12471 . . . . 5 class 0
4846, 19, 47wrex 3070 . . . 4 wff 𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))
4948, 30cio 6493 . . 3 class (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚)))
502, 17, 49cmpt 5231 . 2 class (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠𝑚 ∈ ℕ0𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd𝑥) ∧ 𝑠 = (seq1((+g‘(1st𝑥)), (𝑛 ∈ ℕ ↦ ((2nd𝑥)‘(𝑓𝑛))))‘𝑚))))
511, 50wceq 1541 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  36161
  Copyright terms: Public domain W3C validator