nmblolbii

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmblolbi.1	$⊢ X = BaseSet (U)$
	nmblolbi.4	$⊢ L = {norm}_{CV} (U)$
	nmblolbi.5	$⊢ M = {norm}_{CV} (W)$
	nmblolbi.6	$⊢ N = U {normOp}_{OLD} W$
	nmblolbi.7	$⊢ B = U BLnOp W$
	nmblolbi.u	$⊢ U \in NrmCVec$
	nmblolbi.w	$⊢ W \in NrmCVec$
	nmblolbii.b	$⊢ T \in B$
Assertion	nmblolbii	$⊢ A \in X \to M (T (A)) \leq N (T) L (A)$

Proof

Step	Hyp	Ref	Expression
1		nmblolbi.1	$⊢ X = BaseSet (U)$
2		nmblolbi.4	$⊢ L = {norm}_{CV} (U)$
3		nmblolbi.5	$⊢ M = {norm}_{CV} (W)$
4		nmblolbi.6	$⊢ N = U {normOp}_{OLD} W$
5		nmblolbi.7	$⊢ B = U BLnOp W$
6		nmblolbi.u	$⊢ U \in NrmCVec$
7		nmblolbi.w	$⊢ W \in NrmCVec$
8		nmblolbii.b	$⊢ T \in B$
9		fveq2	$⊢ A = 0_{vec} (U) \to T (A) = T (0_{vec} (U))$
10	9	fveq2d	$⊢ A = 0_{vec} (U) \to M (T (A)) = M (T (0_{vec} (U)))$
11		fveq2	$⊢ A = 0_{vec} (U) \to L (A) = L (0_{vec} (U))$
12	11	oveq2d	$⊢ A = 0_{vec} (U) \to N (T) L (A) = N (T) L (0_{vec} (U))$
13	10 12	breq12d	$⊢ A = 0_{vec} (U) \to (M (T (A)) \leq N (T) L (A) \leftrightarrow M (T (0_{vec} (U))) \leq N (T) L (0_{vec} (U)))$
14	1 2	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to L (A) \in ℝ$
15	6 14	mpan	$⊢ A \in X \to L (A) \in ℝ$
16	15	adantr	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L (A) \in ℝ$
17		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
18	1 17 2	nvz	$⊢ (U \in NrmCVec \land A \in X) \to (L (A) = 0 \leftrightarrow A = 0_{vec} (U))$
19	6 18	mpan	$⊢ A \in X \to (L (A) = 0 \leftrightarrow A = 0_{vec} (U))$
20	19	necon3bid	$⊢ A \in X \to (L (A) \neq 0 \leftrightarrow A \neq 0_{vec} (U))$
21	20	biimpar	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L (A) \neq 0$
22	16 21	rereccld	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to \frac{1}{L (A)} \in ℝ$
23	1 17 2	nvgt0	$⊢ (U \in NrmCVec \land A \in X) \to (A \neq 0_{vec} (U) \leftrightarrow 0 < L (A))$
24	6 23	mpan	$⊢ A \in X \to (A \neq 0_{vec} (U) \leftrightarrow 0 < L (A))$
25	24	biimpa	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to 0 < L (A)$
26	16 25	recgt0d	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to 0 < \frac{1}{L (A)}$
27		0re	$⊢ 0 \in ℝ$
28		ltle	$⊢ (0 \in ℝ \land \frac{1}{L (A)} \in ℝ) \to (0 < \frac{1}{L (A)} \to 0 \leq \frac{1}{L (A)})$
29	27 22 28	sylancr	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to (0 < \frac{1}{L (A)} \to 0 \leq \frac{1}{L (A)})$
30	26 29	mpd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to 0 \leq \frac{1}{L (A)}$
31		eqid	$⊢ BaseSet (W) = BaseSet (W)$
32	1 31 5	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T : X ⟶ BaseSet (W)$
33	6 7 8 32	mp3an	$⊢ T : X ⟶ BaseSet (W)$
34	33	ffvelcdmi	$⊢ A \in X \to T (A) \in BaseSet (W)$
35	34	adantr	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to T (A) \in BaseSet (W)$
36		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
37	31 36 3	nvsge0	$⊢ (W \in NrmCVec \land (\frac{1}{L (A)} \in ℝ \land 0 \leq \frac{1}{L (A)}) \land T (A) \in BaseSet (W)) \to M ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)) = (\frac{1}{L (A)}) M (T (A))$
38	7 37	mp3an1	$⊢ ((\frac{1}{L (A)} \in ℝ \land 0 \leq \frac{1}{L (A)}) \land T (A) \in BaseSet (W)) \to M ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)) = (\frac{1}{L (A)}) M (T (A))$
39	22 30 35 38	syl21anc	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)) = (\frac{1}{L (A)}) M (T (A))$
40	22	recnd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to \frac{1}{L (A)} \in ℂ$
41		simpl	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to A \in X$
42		eqid	$⊢ U LnOp W = U LnOp W$
43	42 5	bloln	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T \in (U LnOp W)$
44	6 7 8 43	mp3an	$⊢ T \in (U LnOp W)$
45	6 7 44	3pm3.2i	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in (U LnOp W))$
46		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
47	1 46 36 42	lnomul	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in (U LnOp W)) \land (\frac{1}{L (A)} \in ℂ \land A \in X)) \to T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = (\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)$
48	45 47	mpan	$⊢ (\frac{1}{L (A)} \in ℂ \land A \in X) \to T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = (\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)$
49	40 41 48	syl2anc	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = (\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A)$
50	49	fveq2d	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M (T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A)) = M ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (W) T (A))$
51	31 3	nvcl	$⊢ (W \in NrmCVec \land T (A) \in BaseSet (W)) \to M (T (A)) \in ℝ$
52	7 34 51	sylancr	$⊢ A \in X \to M (T (A)) \in ℝ$
53	52	adantr	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M (T (A)) \in ℝ$
54	53	recnd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M (T (A)) \in ℂ$
55	16	recnd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L (A) \in ℂ$
56	54 55 21	divrec2d	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to \frac{M (T (A))}{L (A)} = (\frac{1}{L (A)}) M (T (A))$
57	39 50 56	3eqtr4rd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to \frac{M (T (A))}{L (A)} = M (T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A))$
58	1 46	nvscl	$⊢ (U \in NrmCVec \land \frac{1}{L (A)} \in ℂ \land A \in X) \to (\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X$
59	6 58	mp3an1	$⊢ (\frac{1}{L (A)} \in ℂ \land A \in X) \to (\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X$
60	59	ancoms	$⊢ (A \in X \land \frac{1}{L (A)} \in ℂ) \to (\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X$
61	40 60	syldan	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to (\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X$
62	1 2	nvcl	$⊢ (U \in NrmCVec \land (\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \in ℝ$
63	6 61 62	sylancr	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \in ℝ$
64	1 46 17 2	nv1	$⊢ (U \in NrmCVec \land A \in X \land A \neq 0_{vec} (U)) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = 1$
65	6 64	mp3an1	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = 1$
66		eqle	$⊢ (L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \in ℝ \land L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) = 1) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \leq 1$
67	63 65 66	syl2anc	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \leq 1$
68	6 7 33	3pm3.2i	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ BaseSet (W))$
69	1 31 2 3 4	nmoolb	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ BaseSet (W)) \land ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X \land L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \leq 1)) \to M (T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A)) \leq N (T)$
70	68 69	mpan	$⊢ ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A \in X \land L ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A) \leq 1) \to M (T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A)) \leq N (T)$
71	61 67 70	syl2anc	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M (T ((\frac{1}{L (A)}) \cdot_{𝑠OLD} (U) A)) \leq N (T)$
72	57 71	eqbrtrd	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to \frac{M (T (A))}{L (A)} \leq N (T)$
73	1 31 4 5	nmblore	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to N (T) \in ℝ$
74	6 7 8 73	mp3an	$⊢ N (T) \in ℝ$
75	74	a1i	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to N (T) \in ℝ$
76		ledivmul2	$⊢ (M (T (A)) \in ℝ \land N (T) \in ℝ \land (L (A) \in ℝ \land 0 < L (A))) \to (\frac{M (T (A))}{L (A)} \leq N (T) \leftrightarrow M (T (A)) \leq N (T) L (A))$
77	53 75 16 25 76	syl112anc	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to (\frac{M (T (A))}{L (A)} \leq N (T) \leftrightarrow M (T (A)) \leq N (T) L (A))$
78	72 77	mpbid	$⊢ (A \in X \land A \neq 0_{vec} (U)) \to M (T (A)) \leq N (T) L (A)$
79		0le0	$⊢ 0 \leq 0$
80		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
81	1 31 17 80 42	lno0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in (U LnOp W)) \to T (0_{vec} (U)) = 0_{vec} (W)$
82	6 7 44 81	mp3an	$⊢ T (0_{vec} (U)) = 0_{vec} (W)$
83	82	fveq2i	$⊢ M (T (0_{vec} (U))) = M (0_{vec} (W))$
84	80 3	nvz0	$⊢ W \in NrmCVec \to M (0_{vec} (W)) = 0$
85	7 84	ax-mp	$⊢ M (0_{vec} (W)) = 0$
86	83 85	eqtri	$⊢ M (T (0_{vec} (U))) = 0$
87	17 2	nvz0	$⊢ U \in NrmCVec \to L (0_{vec} (U)) = 0$
88	6 87	ax-mp	$⊢ L (0_{vec} (U)) = 0$
89	88	oveq2i	$⊢ N (T) L (0_{vec} (U)) = N (T) \cdot 0$
90	74	recni	$⊢ N (T) \in ℂ$
91	90	mul01i	$⊢ N (T) \cdot 0 = 0$
92	89 91	eqtri	$⊢ N (T) L (0_{vec} (U)) = 0$
93	79 86 92	3brtr4i	$⊢ M (T (0_{vec} (U))) \leq N (T) L (0_{vec} (U))$
94	93	a1i	$⊢ A \in X \to M (T (0_{vec} (U))) \leq N (T) L (0_{vec} (U))$
95	13 78 94	pm2.61ne	$⊢ A \in X \to M (T (A)) \leq N (T) L (A)$

Metamath Proof Explorer

Theorem nmblolbii

Proof