# 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
`|- X = ( BaseSet ` U )`
blometi.2
`|- Y = ( BaseSet ` W )`
blometi.8
`|- C = ( IndMet ` U )`
blometi.d
`|- D = ( IndMet ` W )`
blometi.6
`|- N = ( U normOpOLD W )`
blometi.7
`|- B = ( U BLnOp W )`
blometi.u
`|- U e. NrmCVec`
blometi.w
`|- W e. NrmCVec`
Assertion blometi
`|- ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( T ` P ) D ( T ` Q ) ) <_ ( ( N ` T ) x. ( 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 normOpOLD W )`
6 blometi.7
` |-  B = ( U BLnOp W )`
7 blometi.u
` |-  U e. NrmCVec`
8 blometi.w
` |-  W e. NrmCVec`
9 eqid
` |-  ( -v ` U ) = ( -v ` U )`
10 1 9 nvmcl
` |-  ( ( U e. NrmCVec /\ P e. X /\ Q e. X ) -> ( P ( -v ` U ) Q ) e. X )`
11 7 10 mp3an1
` |-  ( ( P e. X /\ Q e. X ) -> ( P ( -v ` U ) Q ) e. X )`
12 eqid
` |-  ( normCV ` U ) = ( normCV ` U )`
13 eqid
` |-  ( normCV ` W ) = ( normCV ` W )`
14 1 12 13 5 6 7 8 nmblolbi
` |-  ( ( T e. B /\ ( P ( -v ` U ) Q ) e. X ) -> ( ( normCV ` W ) ` ( T ` ( P ( -v ` U ) Q ) ) ) <_ ( ( N ` T ) x. ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) ) )`
15 11 14 sylan2
` |-  ( ( T e. B /\ ( P e. X /\ Q e. X ) ) -> ( ( normCV ` W ) ` ( T ` ( P ( -v ` U ) Q ) ) ) <_ ( ( N ` T ) x. ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) ) )`
16 15 3impb
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( normCV ` W ) ` ( T ` ( P ( -v ` U ) Q ) ) ) <_ ( ( N ` T ) x. ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) ) )`
17 1 2 6 blof
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T : X --> Y )`
18 7 8 17 mp3an12
` |-  ( T e. B -> T : X --> Y )`
19 18 ffvelrnda
` |-  ( ( T e. B /\ P e. X ) -> ( T ` P ) e. Y )`
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( T ` P ) e. Y )`
21 18 ffvelrnda
` |-  ( ( T e. B /\ Q e. X ) -> ( T ` Q ) e. Y )`
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( T ` Q ) e. Y )`
23 eqid
` |-  ( -v ` W ) = ( -v ` W )`
24 2 23 13 4 imsdval
` |-  ( ( W e. NrmCVec /\ ( T ` P ) e. Y /\ ( T ` Q ) e. Y ) -> ( ( T ` P ) D ( T ` Q ) ) = ( ( normCV ` W ) ` ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) ) )`
25 8 24 mp3an1
` |-  ( ( ( T ` P ) e. Y /\ ( T ` Q ) e. Y ) -> ( ( T ` P ) D ( T ` Q ) ) = ( ( normCV ` W ) ` ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) ) )`
26 20 22 25 syl2anc
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( T ` P ) D ( T ` Q ) ) = ( ( normCV ` W ) ` ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) ) )`
27 eqid
` |-  ( U LnOp W ) = ( U LnOp W )`
28 27 6 bloln
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. ( U LnOp W ) )`
29 7 8 28 mp3an12
` |-  ( T e. B -> T e. ( U LnOp W ) )`
30 1 9 23 27 lnosub
` |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. ( U LnOp W ) ) /\ ( P e. X /\ Q e. X ) ) -> ( T ` ( P ( -v ` U ) Q ) ) = ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) )`
31 7 30 mp3anl1
` |-  ( ( ( W e. NrmCVec /\ T e. ( U LnOp W ) ) /\ ( P e. X /\ Q e. X ) ) -> ( T ` ( P ( -v ` U ) Q ) ) = ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) )`
32 8 31 mpanl1
` |-  ( ( T e. ( U LnOp W ) /\ ( P e. X /\ Q e. X ) ) -> ( T ` ( P ( -v ` U ) Q ) ) = ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) )`
33 32 3impb
` |-  ( ( T e. ( U LnOp W ) /\ P e. X /\ Q e. X ) -> ( T ` ( P ( -v ` U ) Q ) ) = ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) )`
34 29 33 syl3an1
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( T ` ( P ( -v ` U ) Q ) ) = ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) )`
35 34 fveq2d
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( normCV ` W ) ` ( T ` ( P ( -v ` U ) Q ) ) ) = ( ( normCV ` W ) ` ( ( T ` P ) ( -v ` W ) ( T ` Q ) ) ) )`
36 26 35 eqtr4d
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( T ` P ) D ( T ` Q ) ) = ( ( normCV ` W ) ` ( T ` ( P ( -v ` U ) Q ) ) ) )`
37 1 9 12 3 imsdval
` |-  ( ( U e. NrmCVec /\ P e. X /\ Q e. X ) -> ( P C Q ) = ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) )`
38 7 37 mp3an1
` |-  ( ( P e. X /\ Q e. X ) -> ( P C Q ) = ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) )`
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( P C Q ) = ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) )`
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( N ` T ) x. ( P C Q ) ) = ( ( N ` T ) x. ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) ) )`
` |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( T ` P ) D ( T ` Q ) ) <_ ( ( N ` T ) x. ( P C Q ) ) )`