Proof of Maps Given by Integrals of Vector- and Matrix-Valued Maps

Proof of (i). For $k\in[q]$, let $x_{k}:E\to\mathbb{R}$ be the $k$-th component map of $x$, with $x_{k}(u)=x(u)_{k}$ for $u\in E$, and let $\chi:[q]\to\mathbb{R}^{E}$, $k\mapsto x_{k}$, be the map of Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (i), with $E$ in place of its $S$; its value at $k$ is the component map $x_{k}$, the two maps $E\to\mathbb{R}$ having the same values (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). As a function whose domain $[q]$ is a set, $\chi$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set (ii).

Let $\Omega(g,u,v,z)$ be the predicative formula of A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) for this $E$; it expresses the condition "$g$ is a map $g:E\to\mathbb{R}$, $u,v\in E$, $\int_{u}^{v}g$ is defined and $z=\int_{u}^{v}g$". By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) we put the parameter $c$ for its variable $u$ and the set variable $t$ for its variable $v$, its bound variables being distinct from the set variables $w$, $t$, $y$, $k$, $g$ and $z$ used here. With $c$, $\chi$, $[q]$, $S$ and $\mathbb{R}^{q}$ as further parameters, let

$$\Gamma=\Bigl\{w\in S\times\mathbb{R}^{q}:\exists t\,\exists y\,\Bigl(w=(t,y)\wedge\forall k\,\forall g\,\forall z\,\bigl((k\in[q]\wedge(k,g)\in\chi\wedge(k,z)\in y)\Rightarrow\Omega(g,c,t,z)\bigr)\Bigr)\Bigr\}.$$

Its formula is built from $\Omega$, memberships, the pair memberships of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and the equation $w=(t,y)$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii) by connectives and by quantifiers over set variables only, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); as $S\times\mathbb{R}^{q}$ is a set (Sets and Maps: Ordinary Notation (iv)), $\Gamma$ is a set by Sets and Maps: Ordinary Notation (iii).

Let $t\in S$ and $y\in\mathbb{R}^{q}$, so that $y$ is a map $y:[q]\to\mathbb{R}$ with components $y_{k}=y(k)$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii)). For $k\in[q]$ and sets $g$ and $z$, $(k,g)\in\chi$ if and only if $g=x_{k}$, and $(k,z)\in y$ if and only if $z=y_{k}$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i). As $x_{k}:E\to\mathbb{R}$ and $c,t\in E$, $\Omega(x_{k},c,t,y_{k})$ holds if and only if $\int_{c}^{t}x_{k}$ is defined and $y_{k}=\int_{c}^{t}x_{k}$. Since $\int_{c}^{t}x$ is defined, $\int_{c}^{t}x_{k}$ is defined and equals $\bigl(\int_{c}^{t}x\bigr)_{k}$ for every $k\in[q]$, by Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii). So the universally quantified condition holds for $t$ and $y$ if and only if $y_{k}=\bigl(\int_{c}^{t}x\bigr)_{k}$ for every $k\in[q]$, that is, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii), if and only if $y=\int_{c}^{t}x$. Hence the elements of $\Gamma$ are exactly the pairs $\bigl(t,\int_{c}^{t}x\bigr)$ with $t\in S$, and, as $\int_{c}^{t}x\in\mathbb{R}^{q}$, $\Gamma$ is a map $\Gamma:S\to\mathbb{R}^{q}$ with $\Gamma(t)=\int_{c}^{t}x$ for every $t\in S$, by Functions, Values of a Function, and Functions from One Class to Another (iii) and Functions, Values of a Function, and Functions from One Class to Another (ii). Every map $X:S\to\mathbb{R}^{q}$ with $X(t)=\int_{c}^{t}x$ for every $t\in S$ has the values of $\Gamma$, so $X=\Gamma$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Proof of (ii). The argument is the same, with the entry maps $A_{ij}:E\to\mathbb{R}$ ($i\in[p]$, $j\in[q]$) of $A$ and the map $(i,j)\mapsto A_{ij}$ from $[p]\times[q]$ to $\mathbb{R}^{E}$ of Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (ii) in place of the component maps and $\chi$, this map being a set as a function whose domain $[p]\times[q]$ is a set (Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set (ii)); with $[p]\times[q]$ and $\mathcal{M}_{p\times q}(\mathbb{R})$ in place of $[q]$ and $\mathbb{R}^{q}$, the variable $k$ now ranging over $[p]\times[q]$; with a matrix $y\in\mathcal{M}_{p\times q}(\mathbb{R})$ being a map $y:[p]\times[q]\to\mathbb{R}$ with entries $y_{ij}=y(i,j)$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii); and with Riemann Integral of a Vector-Valued or Matrix-Valued Map (iv) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii) in place of Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii).

Proof of (iii). Let $\Omega(g,u,v,z)$ be the predicative formula of A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) for this $E$; it expresses the condition "$g$ is a map $g:E\to\mathbb{R}$, $u,v\in E$, $\int_{u}^{v}g$ is defined and $z=\int_{u}^{v}g$", its parameters are among those of (iii), and the set variables $x$, $y$, $k$, $s$, $w$ and $r$ used below are distinct from $g$, $u$, $v$ and $z$ and from its parameters. With $\mu$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), its variables replaced as shown by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i), let $\gamma(g,x,k)$ be the formula

$$\mu(g,E,\mathbb{R})\wedge\forall s\,\forall w\,\forall r\,\bigl(((s,w)\in x\wedge(k,r)\in w)\Rightarrow(s,r)\in g\bigr)$$

and let $\psi(x,u,v,y)$ be the formula

$$\mu(x,E,\mathbb{R}^{q})\wedge u\in E\wedge v\in E\wedge y\in\mathbb{R}^{q}\wedge\forall k\,\Bigl(k\in[q]\Rightarrow\exists g\,\exists z\,\bigl(\gamma(g,x,k)\wedge(k,z)\in y\wedge\Omega(g,u,v,z)\bigr)\Bigr).$$

It is built from $\Omega$, $\mu$, memberships and the pair memberships of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) by connectives and by quantifiers over set variables only, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); its free variables are $x$, $u$, $v$, $y$ and parameters of (iii).

Let sets $x$, $u$, $v$ and $y$ be assigned. Both $\psi$ and the condition of (iii) imply that $x$ is a map $x:E\to\mathbb{R}^{q}$, that $u,v\in E$ and that $y\in\mathbb{R}^{q}$: $\psi$ by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), the condition because $\int_{u}^{v}x\in\mathbb{R}^{q}$ by Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii). So assume these; then $y$ is a map $y:[q]\to\mathbb{R}$ with components $y_{k}=y(k)$, and so is $x(s)$ for every $s\in E$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii)). Let $k\in[q]$, and let $x_{k}:E\to\mathbb{R}$ be the $k$-th component map of $x$, with $E$ in place of its $S$. For a set $g$, $\gamma(g,x,k)$ holds if and only if $g=x_{k}$. Indeed, $x_{k}:E\to\mathbb{R}$; and if $(s,w)\in x$ and $(k,r)\in w$, then $s\in E$ by Domains and Restrictions of Maps (i), $w=x(s)$ and $r=x(s)_{k}=x_{k}(s)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), so $(s,r)\in x_{k}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i); thus $\gamma(x_{k},x,k)$ holds. Conversely, if $\gamma(g,x,k)$ holds, then $g:E\to\mathbb{R}$, and for $s\in E$, $(s,x(s))\in x$ and $(k,x(s)_{k})\in x(s)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $(s,x_{k}(s))\in g$ and $g(s)=x_{k}(s)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i); hence $g=x_{k}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). For a set $z$, $(k,z)\in y$ if and only if $z=y_{k}$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i). So the part of $\psi$ quantified over $g$ and $z$ holds if and only if $\Omega(x_{k},u,v,y_{k})$ holds, that is, as $x_{k}:E\to\mathbb{R}$ and $u,v\in E$, if and only if $\int_{u}^{v}x_{k}$ is defined and $y_{k}=\int_{u}^{v}x_{k}$. Hence $\psi$ holds if and only if $\int_{u}^{v}x_{k}$ is defined and $y_{k}=\int_{u}^{v}x_{k}$ for every $k\in[q]$, that is, by Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii), if and only if $\int_{u}^{v}x$ is defined and $y=\int_{u}^{v}x$. So $\psi$ expresses the first condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii).

For the second condition the argument is the same, with $\mathcal{M}_{p\times q}(\mathbb{R})$ and $[p]\times[q]$ in place of $\mathbb{R}^{q}$ and $[q]$, the variable $k$ now ranging over $[p]\times[q]$; with a matrix being a map $[p]\times[q]\to\mathbb{R}$ whose entry in row $i$ and column $j$ is its value at $(i,j)$, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii); with the entry maps $x_{ij}:E\to\mathbb{R}$ of $x$ in place of the component maps; and with Riemann Integral of a Vector-Valued or Matrix-Valued Map (iv) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (iii) in place of Riemann Integral of a Vector-Valued or Matrix-Valued Map (ii) and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii).