Theorem extoimad

Description: If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	extoimad.1	$$⊢\phi \to F:ℝ⟶ℝ$$
	extoimad.2	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le C$$
Assertion	extoimad	$$⊢\phi \to \forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le C$$

Proof

Step	Hyp	Ref	Expression
1		extoimad.1	$$⊢\phi \to F:ℝ⟶ℝ$$
2		extoimad.2	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le C$$
3	1	ffvelrnda	$$⊢\left(\phi \wedge y\in ℝ\right)\to F\left(y\right)\in ℝ$$
4	3	recnd	$$⊢\left(\phi \wedge y\in ℝ\right)\to F\left(y\right)\in ℂ$$
5	4	abscld	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left|F\left(y\right)\right|\in ℝ$$
6		imaco	$$⊢\left(\mathrm{abs}\circ F\right)\left[ℝ\right]=\mathrm{abs}\left[F\left[ℝ\right]\right]$$
7	6	a1i	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]=\mathrm{abs}\left[F\left[ℝ\right]\right]$$
8	7	eleq2d	$$⊢\phi \to \left(x\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\leftrightarrow x\in \mathrm{abs}\left[F\left[ℝ\right]\right]\right)$$
9		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
10	9	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℝ$$
11		ax-resscn	$$⊢ℝ\subseteq ℂ$$
12	11	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
13	10 12	fssresd	$$⊢\phi \to \left({\mathrm{abs}\upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
14	1 13	fco2d	$$⊢\phi \to \left(\mathrm{abs}\circ F\right):ℝ⟶ℝ$$
15	14	ffnd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)Fnℝ$$
16		ssidd	$$⊢\phi \to ℝ\subseteq ℝ$$
17	15 16	fvelimabd	$$⊢\phi \to \left(x\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\leftrightarrow \exists y\in ℝ\left(\mathrm{abs}\circ F\right)\left(y\right)=x\right)$$
18		eqcom	$$⊢\left(\mathrm{abs}\circ F\right)\left(y\right)=x\leftrightarrow x=\left(\mathrm{abs}\circ F\right)\left(y\right)$$
19	18	a1i	$$⊢\phi \to \left(\left(\mathrm{abs}\circ F\right)\left(y\right)=x\leftrightarrow x=\left(\mathrm{abs}\circ F\right)\left(y\right)\right)$$
20	19	rexbidv	$$⊢\phi \to \left(\exists y\in ℝ\left(\mathrm{abs}\circ F\right)\left(y\right)=x\leftrightarrow \exists y\in ℝx=\left(\mathrm{abs}\circ F\right)\left(y\right)\right)$$
21	17 20	bitrd	$$⊢\phi \to \left(x\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\leftrightarrow \exists y\in ℝx=\left(\mathrm{abs}\circ F\right)\left(y\right)\right)$$
22	1	adantr	$$⊢\left(\phi \wedge y\in ℝ\right)\to F:ℝ⟶ℝ$$
23		simpr	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℝ$$
24	22 23	fvco3d	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(\mathrm{abs}\circ F\right)\left(y\right)=\left|F\left(y\right)\right|$$
25	24	eqcomd	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left|F\left(y\right)\right|=\left(\mathrm{abs}\circ F\right)\left(y\right)$$
26	25	eqeq2d	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(x=\left|F\left(y\right)\right|\leftrightarrow x=\left(\mathrm{abs}\circ F\right)\left(y\right)\right)$$
27	26	rexbidva	$$⊢\phi \to \left(\exists y\in ℝx=\left|F\left(y\right)\right|\leftrightarrow \exists y\in ℝx=\left(\mathrm{abs}\circ F\right)\left(y\right)\right)$$
28	21 27	bitr4d	$$⊢\phi \to \left(x\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\leftrightarrow \exists y\in ℝx=\left|F\left(y\right)\right|\right)$$
29	8 28	bitr3d	$$⊢\phi \to \left(x\in \mathrm{abs}\left[F\left[ℝ\right]\right]\leftrightarrow \exists y\in ℝx=\left|F\left(y\right)\right|\right)$$
30		simpr	$$⊢\left(\phi \wedge x=\left|F\left(y\right)\right|\right)\to x=\left|F\left(y\right)\right|$$
31	30	breq1d	$$⊢\left(\phi \wedge x=\left|F\left(y\right)\right|\right)\to \left(x\le C\leftrightarrow \left|F\left(y\right)\right|\le C\right)$$
32	5 29 31	ralxfr2d	$$⊢\phi \to \left(\forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le C\leftrightarrow \forall y\in ℝ\left|F\left(y\right)\right|\le C\right)$$
33	2 32	mpbird	$$⊢\phi \to \forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le C$$