# 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 ( ( 𝑇𝐵𝑃𝑋𝑄𝑋 ) → ( ( 𝑇𝑃 ) 𝐷 ( 𝑇𝑄 ) ) ≤ ( ( 𝑁𝑇 ) · ( 𝑃 𝐶 𝑄 ) ) )