Theorem liminfresre

Description: The inferior limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	liminfresre.1	|- ( ph -> F e. V )
Assertion	liminfresre	|- ( ph -> ( liminf ` ( F |` RR ) ) = ( liminf ` F ) )

Proof

Step	Hyp	Ref	Expression
1		liminfresre.1	|- ( ph -> F e. V )
2		rge0ssre	|- ( 0 [,) +oo ) C_ RR
3	2	resabs1i	|- ( ( F |` RR ) |` ( 0 [,) +oo ) ) = ( F |` ( 0 [,) +oo ) )
4	3	fveq2i	|- ( liminf ` ( ( F |` RR ) |` ( 0 [,) +oo ) ) ) = ( liminf ` ( F |` ( 0 [,) +oo ) ) )
5	4	a1i	|- ( ph -> ( liminf ` ( ( F |` RR ) |` ( 0 [,) +oo ) ) ) = ( liminf ` ( F |` ( 0 [,) +oo ) ) ) )
6		0red	|- ( ph -> 0 e. RR )
7		eqid	|- ( 0 [,) +oo ) = ( 0 [,) +oo )
8	1	resexd	|- ( ph -> ( F |` RR ) e. _V )
9	6 7 8	liminfresico	|- ( ph -> ( liminf ` ( ( F |` RR ) |` ( 0 [,) +oo ) ) ) = ( liminf ` ( F |` RR ) ) )
10	6 7 1	liminfresico	|- ( ph -> ( liminf ` ( F |` ( 0 [,) +oo ) ) ) = ( liminf ` F ) )
11	5 9 10	3eqtr3d	|- ( ph -> ( liminf ` ( F |` RR ) ) = ( liminf ` F ) )