blometi

Description: Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	blometi.1	$⊢ X = BaseSet (U)$
	blometi.2	$⊢ Y = BaseSet (W)$
	blometi.8	$⊢ C = IndMet (U)$
	blometi.d	$⊢ D = IndMet (W)$
	blometi.6	$⊢ N = U {normOp}_{OLD} W$
	blometi.7	$⊢ B = U BLnOp W$
	blometi.u	$⊢ U \in NrmCVec$
	blometi.w	$⊢ W \in NrmCVec$
Assertion	blometi	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P) D T (Q) \leq N (T) (P C Q)$

Proof

Step	Hyp	Ref	Expression
1		blometi.1	$⊢ X = BaseSet (U)$
2		blometi.2	$⊢ Y = BaseSet (W)$
3		blometi.8	$⊢ C = IndMet (U)$
4		blometi.d	$⊢ D = IndMet (W)$
5		blometi.6	$⊢ N = U {normOp}_{OLD} W$
6		blometi.7	$⊢ B = U BLnOp W$
7		blometi.u	$⊢ U \in NrmCVec$
8		blometi.w	$⊢ W \in NrmCVec$
9		eqid	$⊢ -_{v} (U) = -_{v} (U)$
10	1 9	nvmcl	$⊢ (U \in NrmCVec \land P \in X \land Q \in X) \to P -_{v} (U) Q \in X$
11	7 10	mp3an1	$⊢ (P \in X \land Q \in X) \to P -_{v} (U) Q \in X$
12		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
13		eqid	$⊢ {norm}_{CV} (W) = {norm}_{CV} (W)$
14	1 12 13 5 6 7 8	nmblolbi	$⊢ (T \in B \land P -_{v} (U) Q \in X) \to {norm}_{CV} (W) (T (P -_{v} (U) Q)) \leq N (T) {norm}_{CV} (U) (P -_{v} (U) Q)$
15	11 14	sylan2	$⊢ (T \in B \land (P \in X \land Q \in X)) \to {norm}_{CV} (W) (T (P -_{v} (U) Q)) \leq N (T) {norm}_{CV} (U) (P -_{v} (U) Q)$
16	15	3impb	$⊢ (T \in B \land P \in X \land Q \in X) \to {norm}_{CV} (W) (T (P -_{v} (U) Q)) \leq N (T) {norm}_{CV} (U) (P -_{v} (U) Q)$
17	1 2 6	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T : X ⟶ Y$
18	7 8 17	mp3an12	$⊢ T \in B \to T : X ⟶ Y$
19	18	ffvelcdmda	$⊢ (T \in B \land P \in X) \to T (P) \in Y$
20	19	3adant3	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P) \in Y$
21	18	ffvelcdmda	$⊢ (T \in B \land Q \in X) \to T (Q) \in Y$
22	21	3adant2	$⊢ (T \in B \land P \in X \land Q \in X) \to T (Q) \in Y$
23		eqid	$⊢ -_{v} (W) = -_{v} (W)$
24	2 23 13 4	imsdval	$⊢ (W \in NrmCVec \land T (P) \in Y \land T (Q) \in Y) \to T (P) D T (Q) = {norm}_{CV} (W) (T (P) -_{v} (W) T (Q))$
25	8 24	mp3an1	$⊢ (T (P) \in Y \land T (Q) \in Y) \to T (P) D T (Q) = {norm}_{CV} (W) (T (P) -_{v} (W) T (Q))$
26	20 22 25	syl2anc	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P) D T (Q) = {norm}_{CV} (W) (T (P) -_{v} (W) T (Q))$
27		eqid	$⊢ U LnOp W = U LnOp W$
28	27 6	bloln	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T \in (U LnOp W)$
29	7 8 28	mp3an12	$⊢ T \in B \to T \in (U LnOp W)$
30	1 9 23 27	lnosub	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in (U LnOp W)) \land (P \in X \land Q \in X)) \to T (P -_{v} (U) Q) = T (P) -_{v} (W) T (Q)$
31	7 30	mp3anl1	$⊢ ((W \in NrmCVec \land T \in (U LnOp W)) \land (P \in X \land Q \in X)) \to T (P -_{v} (U) Q) = T (P) -_{v} (W) T (Q)$
32	8 31	mpanl1	$⊢ (T \in (U LnOp W) \land (P \in X \land Q \in X)) \to T (P -_{v} (U) Q) = T (P) -_{v} (W) T (Q)$
33	32	3impb	$⊢ (T \in (U LnOp W) \land P \in X \land Q \in X) \to T (P -_{v} (U) Q) = T (P) -_{v} (W) T (Q)$
34	29 33	syl3an1	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P -_{v} (U) Q) = T (P) -_{v} (W) T (Q)$
35	34	fveq2d	$⊢ (T \in B \land P \in X \land Q \in X) \to {norm}_{CV} (W) (T (P -_{v} (U) Q)) = {norm}_{CV} (W) (T (P) -_{v} (W) T (Q))$
36	26 35	eqtr4d	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P) D T (Q) = {norm}_{CV} (W) (T (P -_{v} (U) Q))$
37	1 9 12 3	imsdval	$⊢ (U \in NrmCVec \land P \in X \land Q \in X) \to P C Q = {norm}_{CV} (U) (P -_{v} (U) Q)$
38	7 37	mp3an1	$⊢ (P \in X \land Q \in X) \to P C Q = {norm}_{CV} (U) (P -_{v} (U) Q)$
39	38	3adant1	$⊢ (T \in B \land P \in X \land Q \in X) \to P C Q = {norm}_{CV} (U) (P -_{v} (U) Q)$
40	39	oveq2d	$⊢ (T \in B \land P \in X \land Q \in X) \to N (T) (P C Q) = N (T) {norm}_{CV} (U) (P -_{v} (U) Q)$
41	16 36 40	3brtr4d	$⊢ (T \in B \land P \in X \land Q \in X) \to T (P) D T (Q) \leq N (T) (P C Q)$

Metamath Proof Explorer

Theorem blometi

Proof