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 normOp OLD W
blometi.7 ⊢ B = U BLnOp W
blometi.u ⊢ U ∈ NrmCVec
blometi.w ⊢ W ∈ NrmCVec
Assertion blometi ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P D T ⁡ Q ≤ N ⁡ T ⁢ 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 normOp OLD W
6 blometi.7 ⊢ B = U BLnOp W
7 blometi.u ⊢ U ∈ NrmCVec
8 blometi.w ⊢ W ∈ NrmCVec
9 eqid ⊢ - v ⁡ U = - v ⁡ U
10 1 9 nvmcl ⊢ U ∈ NrmCVec ∧ P ∈ X ∧ Q ∈ X → P - v ⁡ U Q ∈ X
11 7 10 mp3an1 ⊢ P ∈ X ∧ Q ∈ X → P - v ⁡ U Q ∈ X
12 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
13 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
14 1 12 13 5 6 7 8 nmblolbi ⊢ T ∈ B ∧ P - v ⁡ U Q ∈ X → norm CV ⁡ W ⁡ T ⁡ P - v ⁡ U Q ≤ N ⁡ T ⁢ norm CV ⁡ U ⁡ P - v ⁡ U Q
15 11 14 sylan2 ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → norm CV ⁡ W ⁡ T ⁡ P - v ⁡ U Q ≤ N ⁡ T ⁢ norm CV ⁡ U ⁡ P - v ⁡ U Q
16 15 3impb ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → norm CV ⁡ W ⁡ T ⁡ P - v ⁡ U Q ≤ N ⁡ T ⁢ norm CV ⁡ U ⁡ P - v ⁡ U Q
17 1 2 6 blof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T : X ⟶ Y
18 7 8 17 mp3an12 ⊢ T ∈ B → T : X ⟶ Y
19 18 ffvelcdmda ⊢ T ∈ B ∧ P ∈ X → T ⁡ P ∈ Y
20 19 3adant3 ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P ∈ Y
21 18 ffvelcdmda ⊢ T ∈ B ∧ Q ∈ X → T ⁡ Q ∈ Y
22 21 3adant2 ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ Q ∈ Y
23 eqid ⊢ - v ⁡ W = - v ⁡ W
24 2 23 13 4 imsdval ⊢ W ∈ NrmCVec ∧ T ⁡ P ∈ Y ∧ T ⁡ Q ∈ Y → T ⁡ P D T ⁡ Q = norm CV ⁡ W ⁡ T ⁡ P - v ⁡ W T ⁡ Q
25 8 24 mp3an1 ⊢ T ⁡ P ∈ Y ∧ T ⁡ Q ∈ Y → T ⁡ P D T ⁡ Q = norm CV ⁡ W ⁡ T ⁡ P - v ⁡ W T ⁡ Q
26 20 22 25 syl2anc ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P D T ⁡ Q = norm CV ⁡ W ⁡ T ⁡ P - v ⁡ W T ⁡ Q
27 eqid ⊢ U LnOp W = U LnOp W
28 27 6 bloln ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ U LnOp W
29 7 8 28 mp3an12 ⊢ T ∈ B → T ∈ U LnOp W
30 1 9 23 27 lnosub ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ U LnOp W ∧ P ∈ X ∧ Q ∈ X → T ⁡ P - v ⁡ U Q = T ⁡ P - v ⁡ W T ⁡ Q
31 7 30 mp3anl1 ⊢ W ∈ NrmCVec ∧ T ∈ U LnOp W ∧ P ∈ X ∧ Q ∈ X → T ⁡ P - v ⁡ U Q = T ⁡ P - v ⁡ W T ⁡ Q
32 8 31 mpanl1 ⊢ T ∈ U LnOp W ∧ P ∈ X ∧ Q ∈ X → T ⁡ P - v ⁡ U Q = T ⁡ P - v ⁡ W T ⁡ Q
33 32 3impb ⊢ T ∈ U LnOp W ∧ P ∈ X ∧ Q ∈ X → T ⁡ P - v ⁡ U Q = T ⁡ P - v ⁡ W T ⁡ Q
34 29 33 syl3an1 ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P - v ⁡ U Q = T ⁡ P - v ⁡ W T ⁡ Q
35 34 fveq2d ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → norm CV ⁡ W ⁡ T ⁡ P - v ⁡ U Q = norm CV ⁡ W ⁡ T ⁡ P - v ⁡ W T ⁡ Q
36 26 35 eqtr4d ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P D T ⁡ Q = norm CV ⁡ W ⁡ T ⁡ P - v ⁡ U Q
37 1 9 12 3 imsdval ⊢ U ∈ NrmCVec ∧ P ∈ X ∧ Q ∈ X → P C Q = norm CV ⁡ U ⁡ P - v ⁡ U Q
38 7 37 mp3an1 ⊢ P ∈ X ∧ Q ∈ X → P C Q = norm CV ⁡ U ⁡ P - v ⁡ U Q
39 38 3adant1 ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → P C Q = norm CV ⁡ U ⁡ P - v ⁡ U Q
40 39 oveq2d ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → N ⁡ T ⁢ P C Q = N ⁡ T ⁢ norm CV ⁡ U ⁡ P - v ⁡ U Q
41 16 36 40 3brtr4d ⊢ T ∈ B ∧ P ∈ X ∧ Q ∈ X → T ⁡ P D T ⁡ Q ≤ N ⁡ T ⁢ P C Q