Theorem iblempty

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

	Ref	Expression
Assertion	iblempty	|- (/) e. L^1

Proof

Step	Hyp	Ref	Expression
1		mbf0	|- (/) e. MblFn
2		fconstmpt	|- ( RR X. { 0 } ) = ( x e. RR |-> 0 )
3	2	eqcomi	|- ( x e. RR |-> 0 ) = ( RR X. { 0 } )
4	3	fveq2i	|- ( S.2 ` ( x e. RR |-> 0 ) ) = ( S.2 ` ( RR X. { 0 } ) )
5		itg20	|- ( S.2 ` ( RR X. { 0 } ) ) = 0
6	4 5	eqtri	|- ( S.2 ` ( x e. RR |-> 0 ) ) = 0
7		0re	|- 0 e. RR
8	6 7	eqeltri	|- ( S.2 ` ( x e. RR |-> 0 ) ) e. RR
9	8	rgenw	|- A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR
10		noel	|- -. x e. (/)
11	10	intnanr	|- -. ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) )
12	11	iffalsei	|- if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) = 0
13	12	eqcomi	|- 0 = if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 )
14	13	a1i	|- ( ( T. /\ x e. RR ) -> 0 = if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) )
15	14	mpteq2dva	|- ( T. -> ( x e. RR |-> 0 ) = ( x e. RR |-> if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) )
16		eqidd	|- ( ( T. /\ x e. (/) ) -> ( Re ` ( 0 / ( _i ^ k ) ) ) = ( Re ` ( 0 / ( _i ^ k ) ) ) )
17		dm0	|- dom (/) = (/)
18	17	a1i	|- ( T. -> dom (/) = (/) )
19	10	intnan	|- -. ( T. /\ x e. (/) )
20	19	pm2.21i	|- ( ( T. /\ x e. (/) ) -> ( (/) ` x ) = 0 )
21	15 16 18 20	isibl	|- ( T. -> ( (/) e. L^1 <-> ( (/) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR ) ) )
22	21	mptru	|- ( (/) e. L^1 <-> ( (/) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR ) )
23	1 9 22	mpbir2an	|- (/) e. L^1