# 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}=\mathrm{BaseSet}\left({U}\right)$
blometi.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
blometi.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
blometi.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
blometi.6 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
blometi.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
blometi.u ${⊢}{U}\in \mathrm{NrmCVec}$
blometi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion blometi ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)\le {N}\left({T}\right)\left({P}{C}{Q}\right)$

### Proof

Step Hyp Ref Expression
1 blometi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 blometi.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 blometi.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
4 blometi.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
5 blometi.6 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
6 blometi.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
7 blometi.u ${⊢}{U}\in \mathrm{NrmCVec}$
8 blometi.w ${⊢}{W}\in \mathrm{NrmCVec}$
9 eqid ${⊢}{-}_{v}\left({U}\right)={-}_{v}\left({U}\right)$
10 1 9 nvmcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {P}{-}_{v}\left({U}\right){Q}\in {X}$
11 7 10 mp3an1 ${⊢}\left({P}\in {X}\wedge {Q}\in {X}\right)\to {P}{-}_{v}\left({U}\right){Q}\in {X}$
12 eqid ${⊢}{norm}_{CV}\left({U}\right)={norm}_{CV}\left({U}\right)$
13 eqid ${⊢}{norm}_{CV}\left({W}\right)={norm}_{CV}\left({W}\right)$
14 1 12 13 5 6 7 8 nmblolbi ${⊢}\left({T}\in {B}\wedge {P}{-}_{v}\left({U}\right){Q}\in {X}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({P}{-}_{v}\left({U}\right){Q}\right)\right)\le {N}\left({T}\right){norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
15 11 14 sylan2 ${⊢}\left({T}\in {B}\wedge \left({P}\in {X}\wedge {Q}\in {X}\right)\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({P}{-}_{v}\left({U}\right){Q}\right)\right)\le {N}\left({T}\right){norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
16 15 3impb ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({P}{-}_{v}\left({U}\right){Q}\right)\right)\le {N}\left({T}\right){norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
17 1 2 6 blof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}:{X}⟶{Y}$
18 7 8 17 mp3an12 ${⊢}{T}\in {B}\to {T}:{X}⟶{Y}$
19 18 ffvelrnda ${⊢}\left({T}\in {B}\wedge {P}\in {X}\right)\to {T}\left({P}\right)\in {Y}$
20 19 3adant3 ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}\right)\in {Y}$
21 18 ffvelrnda ${⊢}\left({T}\in {B}\wedge {Q}\in {X}\right)\to {T}\left({Q}\right)\in {Y}$
22 21 3adant2 ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({Q}\right)\in {Y}$
23 eqid ${⊢}{-}_{v}\left({W}\right)={-}_{v}\left({W}\right)$
24 2 23 13 4 imsdval ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({P}\right)\in {Y}\wedge {T}\left({Q}\right)\in {Y}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)={norm}_{CV}\left({W}\right)\left({T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)\right)$
25 8 24 mp3an1 ${⊢}\left({T}\left({P}\right)\in {Y}\wedge {T}\left({Q}\right)\in {Y}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)={norm}_{CV}\left({W}\right)\left({T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)\right)$
26 20 22 25 syl2anc ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)={norm}_{CV}\left({W}\right)\left({T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)\right)$
27 eqid ${⊢}{U}\mathrm{LnOp}{W}={U}\mathrm{LnOp}{W}$
28 27 6 bloln ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in \left({U}\mathrm{LnOp}{W}\right)$
29 7 8 28 mp3an12 ${⊢}{T}\in {B}\to {T}\in \left({U}\mathrm{LnOp}{W}\right)$
30 1 9 23 27 lnosub ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in \left({U}\mathrm{LnOp}{W}\right)\right)\wedge \left({P}\in {X}\wedge {Q}\in {X}\right)\right)\to {T}\left({P}{-}_{v}\left({U}\right){Q}\right)={T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)$
31 7 30 mp3anl1 ${⊢}\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}\in \left({U}\mathrm{LnOp}{W}\right)\right)\wedge \left({P}\in {X}\wedge {Q}\in {X}\right)\right)\to {T}\left({P}{-}_{v}\left({U}\right){Q}\right)={T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)$
32 8 31 mpanl1 ${⊢}\left({T}\in \left({U}\mathrm{LnOp}{W}\right)\wedge \left({P}\in {X}\wedge {Q}\in {X}\right)\right)\to {T}\left({P}{-}_{v}\left({U}\right){Q}\right)={T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)$
33 32 3impb ${⊢}\left({T}\in \left({U}\mathrm{LnOp}{W}\right)\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}{-}_{v}\left({U}\right){Q}\right)={T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)$
34 29 33 syl3an1 ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}{-}_{v}\left({U}\right){Q}\right)={T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)$
35 34 fveq2d ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({P}{-}_{v}\left({U}\right){Q}\right)\right)={norm}_{CV}\left({W}\right)\left({T}\left({P}\right){-}_{v}\left({W}\right){T}\left({Q}\right)\right)$
36 26 35 eqtr4d ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)={norm}_{CV}\left({W}\right)\left({T}\left({P}{-}_{v}\left({U}\right){Q}\right)\right)$
37 1 9 12 3 imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {P}{C}{Q}={norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
38 7 37 mp3an1 ${⊢}\left({P}\in {X}\wedge {Q}\in {X}\right)\to {P}{C}{Q}={norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
39 38 3adant1 ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {P}{C}{Q}={norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
40 39 oveq2d ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {N}\left({T}\right)\left({P}{C}{Q}\right)={N}\left({T}\right){norm}_{CV}\left({U}\right)\left({P}{-}_{v}\left({U}\right){Q}\right)$
41 16 36 40 3brtr4d ${⊢}\left({T}\in {B}\wedge {P}\in {X}\wedge {Q}\in {X}\right)\to {T}\left({P}\right){D}{T}\left({Q}\right)\le {N}\left({T}\right)\left({P}{C}{Q}\right)$