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 ffvelcdmda 
 |-  ( ( T e. B /\ P e. X ) -> ( T ` P ) e. Y )
20 19 3adant3 
 |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( T ` P ) e. Y )
21 18 ffvelcdmda 
 |-  ( ( T e. B /\ Q e. X ) -> ( T ` Q ) e. Y )
22 21 3adant2 
 |-  ( ( 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 ) ) )
39 38 3adant1 
 |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( P C Q ) = ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) )
40 39 oveq2d 
 |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( N ` T ) x. ( P C Q ) ) = ( ( N ` T ) x. ( ( normCV ` U ) ` ( P ( -v ` U ) Q ) ) ) )
41 16 36 40 3brtr4d 
 |-  ( ( T e. B /\ P e. X /\ Q e. X ) -> ( ( T ` P ) D ( T ` Q ) ) <_ ( ( N ` T ) x. ( P C Q ) ) )