Theorem iblconstmpt

Description: A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	iblconstmpt	$$⊢\left(A\in \mathrm{dom}vol\wedge vol\left(A\right)\in ℝ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
2		iblconst	$$⊢\left(A\in \mathrm{dom}vol\wedge vol\left(A\right)\in ℝ\wedge B\in ℂ\right)\to A\times \left\{B\right\}\in {𝐿}^1$$
3	1 2	eqeltrrid	$$⊢\left(A\in \mathrm{dom}vol\wedge vol\left(A\right)\in ℝ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right)\in {𝐿}^1$$