Theorem lnfncon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnfncon	$$⊢T\in \mathrm{LinFn}\to \left(T\in \mathrm{ContFn}\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|T\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left(T\in \mathrm{ContFn}\leftrightarrow if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{ContFn}\right)$$
2		fveq1	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to T\left(y\right)=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)$$
3	2	fveq2d	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left|T\left(y\right)\right|=\left|if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)\right|$$
4	3	breq1d	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left(\left|T\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\leftrightarrow \left|if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)$$
5	4	rexralbidv	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left(\exists x\in ℝ\forall y\in \mathscr{H}\left|T\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)$$
6	1 5	bibi12d	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left(\left(T\in \mathrm{ContFn}\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|T\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)\leftrightarrow \left(if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{ContFn}\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)\right)$$
7		0lnfn	$$⊢\mathscr{H}\times \left\{0\right\}\in \mathrm{LinFn}$$
8	7	elimel	$$⊢if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{LinFn}$$
9	8	lnfnconi	$$⊢if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{ContFn}\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)$$
10	6 9	dedth	$$⊢T\in \mathrm{LinFn}\to \left(T\in \mathrm{ContFn}\leftrightarrow \exists x\in ℝ\forall y\in \mathscr{H}\left|T\left(y\right)\right|\le x{norm}_{ℎ}\left(y\right)\right)$$