Theorem iblconstmpt

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

	Ref	Expression
Assertion	iblconstmpt	|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )
2		iblconst	|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. L^1 )
3	1 2	eqeltrrid	|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. L^1 )