nmlnoubi

Description: An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlnoubi.1	$⊢ X = BaseSet (U)$
	nmlnoubi.z	$⊢ Z = 0_{vec} (U)$
	nmlnoubi.k	$⊢ K = {norm}_{CV} (U)$
	nmlnoubi.m	$⊢ M = {norm}_{CV} (W)$
	nmlnoubi.3	$⊢ N = U {normOp}_{OLD} W$
	nmlnoubi.7	$⊢ L = U LnOp W$
	nmlnoubi.u	$⊢ U \in NrmCVec$
	nmlnoubi.w	$⊢ W \in NrmCVec$
Assertion	nmlnoubi	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A) \land \forall x \in X (x \neq Z \to M (T (x)) \leq A K (x))) \to N (T) \leq A$

Proof

Step	Hyp	Ref	Expression
1		nmlnoubi.1	$⊢ X = BaseSet (U)$
2		nmlnoubi.z	$⊢ Z = 0_{vec} (U)$
3		nmlnoubi.k	$⊢ K = {norm}_{CV} (U)$
4		nmlnoubi.m	$⊢ M = {norm}_{CV} (W)$
5		nmlnoubi.3	$⊢ N = U {normOp}_{OLD} W$
6		nmlnoubi.7	$⊢ L = U LnOp W$
7		nmlnoubi.u	$⊢ U \in NrmCVec$
8		nmlnoubi.w	$⊢ W \in NrmCVec$
9		2fveq3	$⊢ x = Z \to M (T (x)) = M (T (Z))$
10		fveq2	$⊢ x = Z \to K (x) = K (Z)$
11	10	oveq2d	$⊢ x = Z \to A K (x) = A K (Z)$
12	9 11	breq12d	$⊢ x = Z \to (M (T (x)) \leq A K (x) \leftrightarrow M (T (Z)) \leq A K (Z))$
13		id	$⊢ (x \neq Z \to M (T (x)) \leq A K (x)) \to (x \neq Z \to M (T (x)) \leq A K (x))$
14	13	imp	$⊢ ((x \neq Z \to M (T (x)) \leq A K (x)) \land x \neq Z) \to M (T (x)) \leq A K (x)$
15	14	adantll	$⊢ (((T \in L \land (A \in ℝ \land 0 \leq A)) \land (x \neq Z \to M (T (x)) \leq A K (x))) \land x \neq Z) \to M (T (x)) \leq A K (x)$
16		0le0	$⊢ 0 \leq 0$
17		eqid	$⊢ BaseSet (W) = BaseSet (W)$
18		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
19	1 17 2 18 6	lno0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T (Z) = 0_{vec} (W)$
20	7 8 19	mp3an12	$⊢ T \in L \to T (Z) = 0_{vec} (W)$
21	20	fveq2d	$⊢ T \in L \to M (T (Z)) = M (0_{vec} (W))$
22	18 4	nvz0	$⊢ W \in NrmCVec \to M (0_{vec} (W)) = 0$
23	8 22	ax-mp	$⊢ M (0_{vec} (W)) = 0$
24	21 23	eqtrdi	$⊢ T \in L \to M (T (Z)) = 0$
25	24	adantr	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to M (T (Z)) = 0$
26	2 3	nvz0	$⊢ U \in NrmCVec \to K (Z) = 0$
27	7 26	ax-mp	$⊢ K (Z) = 0$
28	27	oveq2i	$⊢ A K (Z) = A \cdot 0$
29		recn	$⊢ A \in ℝ \to A \in ℂ$
30	29	mul01d	$⊢ A \in ℝ \to A \cdot 0 = 0$
31	28 30	syl5eq	$⊢ A \in ℝ \to A K (Z) = 0$
32	31	ad2antrl	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to A K (Z) = 0$
33	25 32	breq12d	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to (M (T (Z)) \leq A K (Z) \leftrightarrow 0 \leq 0)$
34	16 33	mpbiri	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to M (T (Z)) \leq A K (Z)$
35	34	adantr	$⊢ ((T \in L \land (A \in ℝ \land 0 \leq A)) \land (x \neq Z \to M (T (x)) \leq A K (x))) \to M (T (Z)) \leq A K (Z)$
36	12 15 35	pm2.61ne	$⊢ ((T \in L \land (A \in ℝ \land 0 \leq A)) \land (x \neq Z \to M (T (x)) \leq A K (x))) \to M (T (x)) \leq A K (x)$
37	36	ex	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to ((x \neq Z \to M (T (x)) \leq A K (x)) \to M (T (x)) \leq A K (x))$
38	37	ralimdv	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A)) \to (\forall x \in X (x \neq Z \to M (T (x)) \leq A K (x)) \to \forall x \in X M (T (x)) \leq A K (x))$
39	38	3impia	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A) \land \forall x \in X (x \neq Z \to M (T (x)) \leq A K (x))) \to \forall x \in X M (T (x)) \leq A K (x)$
40	1 17 6	lnof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T : X ⟶ BaseSet (W)$
41	7 8 40	mp3an12	$⊢ T \in L \to T : X ⟶ BaseSet (W)$
42	1 17 3 4 5 7 8	nmoub2i	$⊢ (T : X ⟶ BaseSet (W) \land (A \in ℝ \land 0 \leq A) \land \forall x \in X M (T (x)) \leq A K (x)) \to N (T) \leq A$
43	41 42	syl3an1	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A) \land \forall x \in X M (T (x)) \leq A K (x)) \to N (T) \leq A$
44	39 43	syld3an3	$⊢ (T \in L \land (A \in ℝ \land 0 \leq A) \land \forall x \in X (x \neq Z \to M (T (x)) \leq A K (x))) \to N (T) \leq A$

Metamath Proof Explorer

Theorem nmlnoubi

Proof