Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 )
20 19 3adant3 ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑌 )
21 18 ffvelrnda ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑄 ) ∈ 𝑌 )
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 ⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑃 ) 𝐷 ( 𝑇 ‘ 𝑄 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝑃 𝐶 𝑄 ) ) )