P. 302 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30101-30200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	esumeq2sdv 30101*	Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.)
|- ( ph -> B = C )   =>    |- ( ph -> Σ* k e. A B = Σ* k e. A C )
Theorem	nfesum1 30102	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.)
|- F/_ k A   =>    |- F/_ kΣ* k e. A B
Theorem	nfesum2 30103*	Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ xΣ* k e. A B
Theorem	cbvesum 30104*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
|- ( j = k -> B = C )   &    |- F/_ k A   &    |- F/_ j A   &    |- F/_ k B   &    |- F/_ j C   =>    |- Σ* j e. A B = Σ* k e. A C
Theorem	cbvesumv 30105*	Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.)
|- ( j = k -> B = C )   =>    |- Σ* j e. A B = Σ* k e. A C
Theorem	esumid 30106	Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )   =>    |- ( ph -> Σ* k e. A B = C )
Theorem	esumgsum 30107	A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. A B = ( ( RR*s ↾s ( 0 [,] +oo ) ) gsumg ( k e. A |-> B ) ) )
Theorem	esumval 30108*	Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s ↾s ( 0 [,] +oo ) ) gsumg ( k e. x |-> B ) ) = C )   =>    |- ( ph -> Σ* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> C ) , RR* , < ) )
Theorem	esumel 30109*	The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. A B e. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
Theorem	esumnul 30110	Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.)
|- Σ* x e. (/) A = 0
Theorem	esum0 30111*	Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- F/_ k A   =>    |- ( A e. V -> Σ* k e. A 0 = 0 )
Theorem	esumf1o 30112*	Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.)
|- F/ n ph   &    |- F/_ n B   &    |- F/_ k D   &    |- F/_ n A   &    |- F/_ n C   &    |- F/_ n F   &    |- ( k = G -> B = D )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. A B = Σ* n e. C D )
Theorem	esumc 30113*	Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.)
|- F/_ k D   &    |- F/ k ph   &    |- F/_ k A   &    |- ( y = C -> D = B )   &    |- ( ph -> A e. V )   &    |- ( ph -> Fun `' ( k e. A |-> C ) )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. W )   =>    |- ( ph -> Σ* k e. A B = Σ* y e. { z | E. k e. A z = C } D )
Theorem	esumrnmpt 30114*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020.)
|- F/_ k A   &    |- ( y = B -> C = D )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> B e. ( W \ { (/) } ) )   &    |- ( ph -> Disj k e. A B )   =>    |- ( ph -> Σ* y e. ran ( k e. A |-> B ) C = Σ* k e. A D )
Theorem	esumsplit 30115	Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- F/_ k B   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. ( A u. B ) C = (Σ* k e. A C +eΣ* k e. B C ) )
Theorem	esummono 30116*	Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.)
|- F/ k ph   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ k e. C ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> A C_ C )   =>    |- ( ph -> Σ* k e. A B <_ Σ* k e. C B )
Theorem	esumpad 30117*	Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. B ) -> C = 0 )   =>    |- ( ph -> Σ* k e. ( A u. B ) C = Σ* k e. A C )
Theorem	esumpad2 30118*	Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. B ) -> C = 0 )   =>    |- ( ph -> Σ* k e. ( A \ B ) C = Σ* k e. A C )
Theorem	esumadd 30119*	Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. A ( B +e C ) = (Σ* k e. A B +eΣ* k e. A C ) )
Theorem	esumle 30120*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> B <_ C )   =>    |- ( ph -> Σ* k e. A B <_ Σ* k e. A C )
Theorem	gsumesum 30121*	Relate a group sum on ( RR*s ↾s ( 0 [,] +oo ) ) to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> ( ( RR*s ↾s ( 0 [,] +oo ) ) gsumg ( k e. A |-> B ) ) = Σ* k e. A B )
Theorem	esumlub 30122*	The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> X e. RR* )   &    |- ( ph -> X < Σ* k e. A B )   =>    |- ( ph -> E. a e. ( ~P A i^i Fin ) X < Σ* k e. a B )
Theorem	esumaddf 30123*	Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. A ( B +e C ) = (Σ* k e. A B +eΣ* k e. A C ) )
Theorem	esumlef 30124*	If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> B <_ C )   =>    |- ( ph -> Σ* k e. A B <_ Σ* k e. A C )
Theorem	esumcst 30125*	The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
|- F/_ k A   &    |- F/_ k B   =>    |- ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> Σ* k e. A B = ( ( # ` A ) xe B ) )
Theorem	esumsnf 30126*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 2-May-2020.)
|- F/_ k B   &    |- ( ( ph /\ k = M ) -> A = B )   &    |- ( ph -> M e. V )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. { M } A = B )
Theorem	esumsn 30127*	The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Shortened by Thierry Arnoux, 2-May-2020.)
|- ( ( ph /\ k = M ) -> A = B )   &    |- ( ph -> M e. V )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. { M } A = B )
Theorem	esumpr 30128*	Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.)
|- ( ( ph /\ k = A ) -> C = D )   &    |- ( ( ph /\ k = B ) -> C = E )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. ( 0 [,] +oo ) )   &    |- ( ph -> E e. ( 0 [,] +oo ) )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> Σ* k e. { A , B } C = ( D +e E ) )
Theorem	esumpr2 30129*	Extended sum over a pair, with a relaxed condition compared to esumpr 30128. (Contributed by Thierry Arnoux, 2-Jan-2017.)
|- ( ( ph /\ k = A ) -> C = D )   &    |- ( ( ph /\ k = B ) -> C = E )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. ( 0 [,] +oo ) )   &    |- ( ph -> E e. ( 0 [,] +oo ) )   &    |- ( ph -> ( A = B -> ( D = 0 \/ D = +oo ) ) )   =>    |- ( ph -> Σ* k e. { A , B } C = ( D +e E ) )
Theorem	esumrnmpt2 30130*	Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020.)
|- ( y = B -> C = D )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> B e. W )   &    |- ( ( ( ph /\ k e. A ) /\ B = (/) ) -> D = 0 )   &    |- ( ph -> Disj k e. A B )   =>    |- ( ph -> Σ* y e. ran ( k e. A |-> B ) C = Σ* k e. A D )
Theorem	esumfzf 30131*	Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
|- F/_ k F   =>    |- ( ( F : NN --> ( 0 [,] +oo ) /\ N e. NN ) -> Σ* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) )
Theorem	esumfsup 30132	Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.)
|- F/_ k F   =>    |- ( F : NN --> ( 0 [,] +oo ) -> Σ* k e. NN ( F ` k ) = sup ( ran seq 1 ( +e , F ) , RR* , < ) )
Theorem	esumfsupre 30133	Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017.)
|- F/_ k F   =>    |- ( F : NN --> ( 0 [,) +oo ) -> Σ* k e. NN ( F ` k ) = sup ( ran seq 1 ( + , F ) , RR* , < ) )
Theorem	esumss 30134	Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- F/_ k B   &    |- ( ph -> A C_ B )   &    |- ( ph -> B e. V )   &    |- ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   =>    |- ( ph -> Σ* k e. A C = Σ* k e. B C )
Theorem	esumpinfval 30135*	The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> E. k e. A B = +oo )   =>    |- ( ph -> Σ* k e. A B = +oo )
Theorem	esumpfinvallem 30136	Lemma for esumpfinval 30137. (Contributed by Thierry Arnoux, 28-Jun-2017.)
|- ( ( A e. V /\ F : A --> ( 0 [,) +oo ) ) -> (ℂfld gsumg F ) = ( ( RR*s ↾s ( 0 [,] +oo ) ) gsumg F ) )
Theorem	esumpfinval 30137*	The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017.) (Proof shortened by AV, 25-Jul-2019.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> Σ* k e. A B = sum_ k e. A B )
Theorem	esumpfinvalf 30138	Same as esumpfinval 30137, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.)
|- F/_ k A   &    |- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> Σ* k e. A B = sum_ k e. A B )
Theorem	esumpinfsum 30139*	The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k A   &    |- ( ph -> A e. V )   &    |- ( ph -> -. A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> M <_ B )   &    |- ( ph -> M e. RR* )   &    |- ( ph -> 0 < M )   =>    |- ( ph -> Σ* k e. A B = +oo )
Theorem	esumpcvgval 30140*	The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )   &    |- ( k = l -> A = B )   &    |- ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> )   =>    |- ( ph -> Σ* k e. NN A = sum_ k e. NN A )
Theorem	esumpmono 30141*	The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )   =>    |- ( ph -> Σ* k e. ( 1 ... M ) A <_ Σ* k e. ( 1 ... N ) A )
Theorem	esumcocn 30142*	Lemma for esummulc2 30144 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|- J = ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. ( J Cn J ) )   &    |- ( ph -> ( C ` 0 ) = 0 )   &    |- ( ( ph /\ x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( C ` ( x +e y ) ) = ( ( C ` x ) +e ( C ` y ) ) )   =>    |- ( ph -> ( C ` Σ* k e. A B ) = Σ* k e. A ( C ` B ) )
Theorem	esummulc1 30143*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ* k e. A B xe C ) = Σ* k e. A ( B xe C ) )
Theorem	esummulc2 30144*	An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   =>    |- ( ph -> ( C xeΣ* k e. A B ) = Σ* k e. A ( C xe B ) )
Theorem	esumdivc 30145*	An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> (Σ* k e. A B /𝑒 C ) = Σ* k e. A ( B /𝑒 C ) )
Theorem	hashf2 30146	Lemma for hasheuni 30147. (Contributed by Thierry Arnoux, 19-Nov-2016.)
|- # : _V --> ( 0 [,] +oo )
Theorem	hasheuni 30147*	The cardinality of a disjoint union, not necessarily finite. cf. hashuni 14558. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.)
|- ( ( A e. V /\ Disj x e. A x ) -> ( # ` U. A ) = Σ* x e. A ( # ` x ) )
Theorem	esumcvg 30148*	The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 14458. (Contributed by Thierry Arnoux, 5-Sep-2017.)
|- J = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )   &    |- F = ( n e. NN |-> Σ* k e. ( 1 ... n ) A )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )   &    |- ( k = m -> A = B )   =>    |- ( ph -> F ( ~~> t ` J )Σ* k e. NN A )
Theorem	esumcvg2 30149*	Simpler version of esumcvg 30148. (Contributed by Thierry Arnoux, 5-Sep-2017.)
|- J = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )   &    |- ( k = l -> A = B )   &    |- ( k = m -> A = C )   =>    |- ( ph -> ( n e. NN |-> Σ* k e. ( 1 ... n ) A ) ( ~~> t ` J )Σ* k e. NN A )
Theorem	esumcvgsum 30150*	The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.)
|- ( k = i -> A = B )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) = A )   &    |- ( ph -> seq 1 ( + , F ) ~~> L )   &    |- ( ph -> L e. RR )   =>    |- ( ph -> Σ* k e. NN A = sum_ k e. NN A )
Theorem	esumsup 30151*	Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.)
|- ( ph -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. NN A = sup ( ran ( n e. NN |-> Σ* k e. ( 1 ... n ) A ) , RR* , < ) )
Theorem	esumgect 30152*	"Send n to +oo " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.)
|- ( ph -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ n e. NN ) -> Σ* k e. ( 1 ... n ) A <_ B )   =>    |- ( ph -> Σ* k e. NN A <_ B )
Theorem	esumcvgre 30153*	All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> Σ* k e. A B e. RR )   =>    |- ( ( ph /\ k e. A ) -> B e. RR )
Theorem	esum2dlem 30154*	Lemma for esum2d 30155 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.)
|- F/_ k F   &    |- ( z = <. j , k >. -> F = C )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> B e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> Σ* j e. AΣ* k e. B C = Σ* z e. U_ j e. A ( { j } X. B ) F )
Theorem	esum2d 30155*	Write a double extended sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j. This can be seen as "slicing" the relation A. (Contributed by Thierry Arnoux, 17-May-2020.)
|- F/_ k F   &    |- ( z = <. j , k >. -> F = C )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> B e. W )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* j e. AΣ* k e. B C = Σ* z e. U_ j e. A ( { j } X. B ) F )
Theorem	esumiun 30156*	Sum over a non necessarily disjoint indexed union. The inegality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ j e. A ) -> B e. W )   &    |- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> Σ* k e. U_ j e. A B C <_ Σ* j e. AΣ* k e. B C )
20.3.15  Mixed Function/Constant operation
Syntax	cofc 30157	Extend class notation to include mapping of an operation to an operation for a function and a constant.
class ∘𝑓/𝑐 R
Definition	df-ofc 30158*	Define the function/constant operation map. The definition is designed so that if R is a binary operation, then ∘𝑓/𝑐 R is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)
|- ∘𝑓/𝑐 R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )
Theorem	ofceq 30159	Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( R = S -> ∘𝑓/𝑐 R = ∘𝑓/𝑐 S )
Theorem	ofcfval 30160*	Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofcval 30161	Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = B )   =>    |- ( ( ph /\ X e. A ) -> ( ( F∘𝑓/𝑐 R C ) ` X ) = ( B R C ) )
Theorem	ofcfn 30162	The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) Fn A )
Theorem	ofcfeqd2 30163*	Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )   &    |- ( ( ph /\ y e. B ) -> ( y R C ) = ( y P C ) )   &    |- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) = ( F∘𝑓/𝑐 P C ) )
Theorem	ofcfval3 30164*	General value of ( F∘𝑓/𝑐 R C ) with no assumptions on functionality of F. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( F e. V /\ C e. W ) -> ( F∘𝑓/𝑐 R C ) = ( x e. dom F |-> ( ( F ` x ) R C ) ) )
Theorem	ofcf 30165*	The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. T )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) : A --> U )
Theorem	ofcfval2 30166*	The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ph -> A e. V )   &    |- ( ph -> C e. W )   &    |- ( ( ph /\ x e. A ) -> B e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofcfval4 30167*	The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ph -> F : A --> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) = ( ( x e. B |-> ( x R C ) ) o. F ) )
Theorem	ofcc 30168	Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( ( A X. { B } )∘𝑓/𝑐 R C ) = ( A X. { ( B R C ) } ) )
Theorem	ofcof 30169	Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.)
|- ( ph -> F : A --> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> ( F∘𝑓/𝑐 R C ) = ( F oF R ( A X. { C } ) ) )
20.3.16  Abstract measure
20.3.16.1  Sigma-Algebra
Syntax	csiga 30170	Extend class notation to include the function giving the sigma-algebras on a given base set.
class sigAlgebra
Definition	df-siga 30171*	Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using S and O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.)
|- sigAlgebra = ( o e. _V |-> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) } )
Theorem	sigaex 30172*	Lemma for issiga 30174 and isrnsiga 30176. The class of sigma-algebras with base set o is a set. Note: a more generic version with ( O e. _V -> ... ) could be useful for sigaval 30173. (Contributed by Thierry Arnoux, 24-Oct-2016.)
|- { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) } e. _V
Theorem	sigaval 30173*	The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.)
|- ( O e. _V -> (sigAlgebra ` O ) = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) } )
Theorem	issiga 30174*	An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.)
|- ( S e. _V -> ( S e. (sigAlgebra ` O ) <-> ( S C_ ~P O /\ ( O e. S /\ A. x e. S ( O \ x ) e. S /\ A. x e. ~P S ( x ~<_ om -> U. x e. S ) ) ) ) )
Theorem	isrnsigaOLD 30175*	The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. o ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ om -> U. x e. S ) ) ) ) )
Theorem	isrnsiga 30176*	The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (Proof shortened by Thierry Arnoux, 23-Oct-2016.)
|- ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. o ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ om -> U. x e. S ) ) ) ) )
Theorem	0elsiga 30177	A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.)
|- ( S e. U. ran sigAlgebra -> (/) e. S )
Theorem	baselsiga 30178	A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.)
|- ( S e. (sigAlgebra ` A ) -> A e. S )
Theorem	sigasspw 30179	A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.)
|- ( S e. (sigAlgebra ` A ) -> S C_ ~P A )
Theorem	sigaclcu 30180	A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ om ) -> U. A e. S )
Theorem	sigaclcuni 30181*	A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.)
|- F/_ k A   =>    |- ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ om ) -> U_ k e. A B e. S )
Theorem	sigaclfu 30182	A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A e. Fin ) -> U. A e. S )
Theorem	sigaclcu2 30183*	A sigma-algebra is closed under countable union - indexing on NN (Contributed by Thierry Arnoux, 29-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A e. S )
Theorem	sigaclfu2 30184*	A sigma-algebra is closed under finite union - indexing on ( 1..^ N ). (Contributed by Thierry Arnoux, 28-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1..^ N ) A e. S ) -> U_ k e. ( 1..^ N ) A e. S )
Theorem	sigaclcu3 30185*	A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.)
|- ( ph -> S e. U. ran sigAlgebra )   &    |- ( ph -> ( N = NN \/ N = ( 1..^ M ) ) )   &    |- ( ( ph /\ k e. N ) -> A e. S )   =>    |- ( ph -> U_ k e. N A e. S )
Theorem	issgon 30186	Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016.) (Revised by Thierry Arnoux, 23-Oct-2016.)
|- ( S e. (sigAlgebra ` O ) <-> ( S e. U. ran sigAlgebra /\ O = U. S ) )
Theorem	sgon 30187	A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
|- ( S e. U. ran sigAlgebra -> S e. (sigAlgebra ` U. S ) )
Theorem	elsigass 30188	An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.)
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A C_ U. S )
Theorem	elrnsiga 30189	Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
|- ( S e. (sigAlgebra ` O ) -> S e. U. ran sigAlgebra )
Theorem	isrnsigau 30190*	The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.)
|- ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ om -> U. x e. S ) ) ) )
Theorem	unielsiga 30191	A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017.) (Shortened by Thierry Arnoux, 6-Jun-2017.)
|- ( S e. U. ran sigAlgebra -> U. S e. S )
Theorem	dmvlsiga 30192	Lebesgue-measurable subsets of RR form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
|- dom vol e. (sigAlgebra ` RR )
Theorem	pwsiga 30193	Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.)
|- ( O e. V -> ~P O e. (sigAlgebra ` O ) )
Theorem	prsiga 30194	The smallest possible sigma-algebra containing O. (Contributed by Thierry Arnoux, 13-Sep-2016.)
|- ( O e. V -> { (/) , O } e. (sigAlgebra ` O ) )
Theorem	sigaclci 30195	A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.)
|- ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ om /\ A =/= (/) ) ) -> |^| A e. S )
Theorem	difelsiga 30196	A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )
Theorem	unelsiga 30197	A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )
Theorem	inelsiga 30198	A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )
Theorem	sigainb 30199	Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.)
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. (sigAlgebra ` A ) )
Theorem	insiga 30200	The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )