Theorem 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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	blometi.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	blometi.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
	blometi.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
	blometi.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	blometi.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
	blometi.u	⊢ 𝑈 ∈ NrmCVec
	blometi.w	⊢ 𝑊 ∈ NrmCVec
Assertion	blometi	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝑃 𝐶 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		blometi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		blometi.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		blometi.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
4		blometi.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
5		blometi.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6		blometi.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
7		blometi.u	⊢ 𝑈 ∈ NrmCVec
8		blometi.w	⊢ 𝑊 ∈ NrmCVec
9		eqid	⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
10	1 9	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ∈ 𝑋 )
11	7 10	mp3an1	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ∈ 𝑋 )
12		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
13		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
14	1 12 13 5 6 7 8	nmblolbi	⊢ ( ( 𝑇 ∈ 𝐵 ∧ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ∈ 𝑋 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) )
15	11 14	sylan2	⊢ ( ( 𝑇 ∈ 𝐵 ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) )
16	15	3impb	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) )
17	1 2 6	blof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ 𝑌 )
18	7 8 17	mp3an12	⊢ ( 𝑇 ∈ 𝐵 → 𝑇 : 𝑋 ⟶ 𝑌 )
19	18	ffvelcdmda	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 )
20	19	3adant3	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 )
21	18	ffvelcdmda	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 )
22	21	3adant2	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 )
23		eqid	⊢ ( −𝑣 ‘ 𝑊 ) = ( −𝑣 ‘ 𝑊 )
24	2 23 13 4	imsdval	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 ∧ ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ) )
25	8 24	mp3an1	⊢ ( ( ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 ∧ ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ) )
26	20 22 25	syl2anc	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ) )
27		eqid	⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
28	27 6	bloln	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
29	7 8 28	mp3an12	⊢ ( 𝑇 ∈ 𝐵 → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
30	1 9 23 27	lnosub	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
31	7 30	mp3anl1	⊢ ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
32	8 31	mpanl1	⊢ ( ( 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
33	32	3impb	⊢ ( ( 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
34	29 33	syl3an1	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) = ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) )
35	34	fveq2d	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( ( 𝑇 ‘ 𝑃 ) ( −𝑣 ‘ 𝑊 ) ( 𝑇 ‘ 𝑄 ) ) ) )
36	26 35	eqtr4d	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) = ( ( normCV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) )
37	1 9 12 3	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑄 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) )
38	7 37	mp3an1	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑄 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) )
39	38	3adant1	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑄 ) = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) )
40	39	oveq2d	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑇 ) · ( 𝑃 𝐶 𝑄 ) ) = ( ( 𝑁 ‘ 𝑇 ) · ( ( normCV ‘ 𝑈 ) ‘ ( 𝑃 ( −𝑣 ‘ 𝑈 ) 𝑄 ) ) ) )
41	16 36 40	3brtr4d	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝑃 𝐶 𝑄 ) ) )