HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem nmo0 11851
Description: The operator norm of the zero operator.
Hypotheses
Ref Expression
nmo0.3 |- N = (UnormOpW)
nmo0.0 |- Z = (U 0op W)
Assertion
Ref Expression
nmo0 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (N` Z) = 0)

Proof of Theorem nmo0
StepHypRef Expression
1 eqid 1953 . . . . 5 |- (BaseSet` U) = (BaseSet` U)
2 eqid 1953 . . . . 5 |- (BaseSet` W) = (BaseSet` W)
3 nmo0.0 . . . . 5 |- Z = (U 0op W)
41, 2, 30oo 11849 . . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z:(BaseSet` U)-->(BaseSet` W))
5 eqid 1953 . . . . 5 |- (norm` U) = (norm` U)
6 eqid 1953 . . . . 5 |- (norm` W) = (norm` W)
7 nmo0.3 . . . . 5 |- N = (UnormOpW)
81, 2, 5, 6, 7nmoval 11823 . . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ Z:(BaseSet` U)-->(BaseSet` W)) -> (N` Z) = sup({x | E.z e. (BaseSet` U)(((norm`
U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))}, RR*, < ))
94, 8mpd3an3 1274 . . 3 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (N` Z) = sup({x | E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))}, RR*, < ))
10 df-sn 3096 . . . . 5 |- {0} = {x | x = 0}
11 eqid 1953 . . . . . . . . . . 11 |- (0vec` U) = (0vec` U)
121, 11nvzcl 11671 . . . . . . . . . 10 |- (U e. NrmCVec -> (0vec` U) e. (BaseSet` U))
1311, 5nvz0 11713 . . . . . . . . . . 11 |- (U e. NrmCVec -> ((norm` U)` (0vec` U)) = 0)
14 0re 7107 . . . . . . . . . . . 12 |- 0 e. RR
15 1re 7106 . . . . . . . . . . . 12 |- 1 e. RR
16 lt01 7443 . . . . . . . . . . . 12 |- 0 < 1
1714, 15, 16ltleii 7172 . . . . . . . . . . 11 |- 0 <_ 1
1813, 17syl6eqbr 3410 . . . . . . . . . 10 |- (U e. NrmCVec -> ((norm` U)` (0vec` U)) <_ 1)
19 fveq2 4681 . . . . . . . . . . . 12 |- (z = (0vec`
U) -> ((norm` U)` z) = ((norm` U)` (0vec` U)))
2019breq1d 3383 . . . . . . . . . . 11 |- (z = (0vec`
U) -> (((norm`
U)` z) <_ 1 <-> ((norm` U)` (0vec` U)) <_ 1))
2120rcla4ev 2444 . . . . . . . . . 10 |- (((0vec` U) e. (BaseSet` U) /\ ((norm` U)` (0vec` U)) <_ 1) -> E.z e. (BaseSet` U)((norm` U)` z) <_ 1)
2212, 18, 21syl2anc 659 . . . . . . . . 9 |- (U e. NrmCVec -> E.z e. (BaseSet` U)((norm` U)` z) <_ 1)
2322biantrurd 511 . . . . . . . 8 |- (U e. NrmCVec -> (x = 0 <-> (E.z e. (BaseSet` U)((norm` U)` z) <_ 1 /\ x = 0)))
2423adantr 468 . . . . . . 7 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (x = 0 <-> (E.z e. (BaseSet` U)((norm` U)` z) <_ 1 /\ x = 0)))
25 eqid 1953 . . . . . . . . . . . . . . 15 |- (0vec` W) = (0vec` W)
261, 25, 30oval 11848 . . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ W e. NrmCVec /\ z e. (BaseSet` U)) -> (Z` z) = (0vec` W))
27263expa 1148 . . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> (Z` z) = (0vec` W))
2827fveq2d 4685 . . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> ((norm` W)` (Z` z)) = ((norm` W)` (0vec` W)))
2925, 6nvz0 11713 . . . . . . . . . . . . 13 |- (W e. NrmCVec -> ((norm` W)` (0vec` W)) = 0)
3029ad2antlr 728 . . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> ((norm` W)` (0vec` W)) = 0)
3128, 30eqtrd 1985 . . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> ((norm` W)` (Z` z)) = 0)
3231eqeq2d 1964 . . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> (x = ((norm`
W)` (Z` z)) <-> x = 0))
3332anbi2d 702 . . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (BaseSet` U)) -> ((((norm` U)` z) <_ 1 /\ x = ((norm` W)` (Z` z))) <-> (((norm`
U)` z) <_ 1 /\ x = 0)))
3433rexbidva 2177 . . . . . . . 8 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (E.z e. (BaseSet` U)(((norm`
U)` z) <_ 1 /\ x = ((norm` W)` (Z` z))) <-> E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = 0)))
35 r19.41v 2298 . . . . . . . 8 |- (E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = 0) <-> (E.z e. (BaseSet` U)((norm` U)` z) <_ 1 /\ x = 0))
3634, 35syl6rbb 267 . . . . . . 7 |- ((U e. NrmCVec /\ W e. NrmCVec) -> ((E.z e. (BaseSet` U)((norm`
U)` z) <_ 1 /\ x = 0) <-> E.z e. (BaseSet` U)(((norm`
U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))))
3724, 36bitrd 258 . . . . . 6 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (x = 0 <-> E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))))
3837abbidv 2062 . . . . 5 |- ((U e. NrmCVec /\ W e. NrmCVec) -> {x | x = 0} = {x | E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))})
3910, 38syl5req 1998 . . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec) -> {x | E.z e. (BaseSet` U)(((norm` U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))} = {0})
4039supeq1d 5997 . . 3 |- ((U e. NrmCVec /\ W e. NrmCVec) -> sup({x | E.z e. (BaseSet` U)(((norm`
U)` z) <_ 1 /\ x = ((norm` W)` (Z` z)))}, RR*, < ) = sup({0}, RR*, < ))
419, 40eqtrd 1985 . 2 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (N` Z) = sup({0}, RR*, < ))
42 0xr 7122 . . 3 |- 0 e. RR*
43 xrltso 8176 . . . 4 |- < Or RR*
4443supsn 6019 . . 3 |- (0 e. RR* -> sup({0}, RR*, < ) = 0)
4542, 44ax-mp 8 . 2 |- sup({0}, RR*, < ) = 0
4641, 45syl6eq 2001 1 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (N` Z) = 0)
Colors of variables: wff set class
Syntax hints:   -> wi 4   <-> wb 184   /\ wa 377   = wceq 1449   e. wcel 1451  {cab 1940  E.wrex 2163  {csn 3092   class class class wbr 3373  -->wf 4012  ` cfv 4016  (class class class)co 4931  supcsup 5991  0cc0 7000  1c1 7001   <_ cle 7108  RR*cxr 7111   < clt 7112  NrmCVeccnv 11619  BaseSetcba 11621  0veccn0v 11623  normcnm 11625  normOpcnmo 11801   0op c0o 11803
This theorem is referenced by:  0blo 11852  nmlno0lem 11853
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808  ax-inf2 6071  ax-resscn 7054  ax-1cn 7055  ax-icn 7056  ax-addcl 7057  ax-addrcl 7058  ax-mulcl 7059  ax-mulrcl 7060  ax-mulcom 7061  ax-addass 7062  ax-mulass 7063  ax-distr 7064  ax-i2m1 7065  ax-1ne0 7066  ax-1rid 7067  ax-rnegex 7068  ax-rrecex 7069  ax-cnre 7070  ax-pre-lttri 7071  ax-pre-lttrn 7072  ax-pre-ltadd 7073  ax-pre-mulgt0 7074  ax-pre-sup 7075
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-tru 1345  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-nel 2074  df-ral 2166  df-rex 2167  df-reu 2168  df-rab 2169  df-v 2360  df-sbc 2525  df-csb 2600  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-if 3023  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-iun 3301  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3971  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-f1 4029  df-fo 4030  df-f1o 4031  df-fv 4032  df-ov 4933  df-oprab 4934  df-mpt 5068  df-mpt2 5069  df-1st 5166  df-2nd 5167  df-iota 5270  df-rdg 5356  df-er 5530  df-map 5618  df-en 5675  df-dom 5676  df-sdom 5677  df-riota 5818  df-sup 5992  df-pnf 7113  df-mnf 7114  df-xr 7115  df-ltxr 7116  df-le 7117  df-sub 7242  df-neg 7244  df-div 7468  df-n 7706  df-2 7752  df-3 7753  df-n0 7876  df-z 7920  df-uz 8040  df-q 8122  df-rp 8247  df-seq 8575  df-exp 8627  df-cj 8861  df-re 8862  df-im 8863  df-sqr 8955  df-abs 8956  df-grpo 10535  df-gid 10536  df-ginv 10537  df-ablo 10630  df-vc 11581  df-nv 11627  df-va 11630  df-ba 11631  df-sm 11632  df-0v 11633  df-nm 11635  df-nmo 11805  df-0o 11807
Copyright terms: Public domain