![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nmlno0i | Structured version Visualization version GIF version |
Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nmlno0.3 | ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
nmlno0.0 | ⊢ 𝑍 = (𝑈 0op 𝑊) |
nmlno0.7 | ⊢ 𝐿 = (𝑈 LnOp 𝑊) |
nmlno0i.u | ⊢ 𝑈 ∈ NrmCVec |
nmlno0i.w | ⊢ 𝑊 ∈ NrmCVec |
Ref | Expression |
---|---|
nmlno0i | ⊢ (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveqeq2 6849 | . . 3 ⊢ (𝑇 = if(𝑇 ∈ 𝐿, 𝑇, 𝑍) → ((𝑁‘𝑇) = 0 ↔ (𝑁‘if(𝑇 ∈ 𝐿, 𝑇, 𝑍)) = 0)) | |
2 | eqeq1 2742 | . . 3 ⊢ (𝑇 = if(𝑇 ∈ 𝐿, 𝑇, 𝑍) → (𝑇 = 𝑍 ↔ if(𝑇 ∈ 𝐿, 𝑇, 𝑍) = 𝑍)) | |
3 | 1, 2 | bibi12d 346 | . 2 ⊢ (𝑇 = if(𝑇 ∈ 𝐿, 𝑇, 𝑍) → (((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) ↔ ((𝑁‘if(𝑇 ∈ 𝐿, 𝑇, 𝑍)) = 0 ↔ if(𝑇 ∈ 𝐿, 𝑇, 𝑍) = 𝑍))) |
4 | nmlno0.3 | . . 3 ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) | |
5 | nmlno0.0 | . . 3 ⊢ 𝑍 = (𝑈 0op 𝑊) | |
6 | nmlno0.7 | . . 3 ⊢ 𝐿 = (𝑈 LnOp 𝑊) | |
7 | nmlno0i.u | . . 3 ⊢ 𝑈 ∈ NrmCVec | |
8 | nmlno0i.w | . . 3 ⊢ 𝑊 ∈ NrmCVec | |
9 | 5, 6 | 0lno 29561 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐿) |
10 | 7, 8, 9 | mp2an 691 | . . . 4 ⊢ 𝑍 ∈ 𝐿 |
11 | 10 | elimel 4554 | . . 3 ⊢ if(𝑇 ∈ 𝐿, 𝑇, 𝑍) ∈ 𝐿 |
12 | eqid 2738 | . . 3 ⊢ (BaseSet‘𝑈) = (BaseSet‘𝑈) | |
13 | eqid 2738 | . . 3 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊) | |
14 | eqid 2738 | . . 3 ⊢ ( ·𝑠OLD ‘𝑈) = ( ·𝑠OLD ‘𝑈) | |
15 | eqid 2738 | . . 3 ⊢ ( ·𝑠OLD ‘𝑊) = ( ·𝑠OLD ‘𝑊) | |
16 | eqid 2738 | . . 3 ⊢ (0vec‘𝑈) = (0vec‘𝑈) | |
17 | eqid 2738 | . . 3 ⊢ (0vec‘𝑊) = (0vec‘𝑊) | |
18 | eqid 2738 | . . 3 ⊢ (normCV‘𝑈) = (normCV‘𝑈) | |
19 | eqid 2738 | . . 3 ⊢ (normCV‘𝑊) = (normCV‘𝑊) | |
20 | 4, 5, 6, 7, 8, 11, 12, 13, 14, 15, 16, 17, 18, 19 | nmlno0lem 29564 | . 2 ⊢ ((𝑁‘if(𝑇 ∈ 𝐿, 𝑇, 𝑍)) = 0 ↔ if(𝑇 ∈ 𝐿, 𝑇, 𝑍) = 𝑍) |
21 | 3, 20 | dedth 4543 | 1 ⊢ (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ifcif 4485 ‘cfv 6494 (class class class)co 7352 0cc0 11010 NrmCVeccnv 29355 BaseSetcba 29357 ·𝑠OLD cns 29358 0veccn0v 29359 normCVcnmcv 29361 LnOp clno 29511 normOpOLD cnmoo 29512 0op c0o 29514 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7665 ax-cnex 11066 ax-resscn 11067 ax-1cn 11068 ax-icn 11069 ax-addcl 11070 ax-addrcl 11071 ax-mulcl 11072 ax-mulrcl 11073 ax-mulcom 11074 ax-addass 11075 ax-mulass 11076 ax-distr 11077 ax-i2m1 11078 ax-1ne0 11079 ax-1rid 11080 ax-rnegex 11081 ax-rrecex 11082 ax-cnre 11083 ax-pre-lttri 11084 ax-pre-lttrn 11085 ax-pre-ltadd 11086 ax-pre-mulgt0 11087 ax-pre-sup 11088 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5530 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5587 df-we 5589 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6252 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7308 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7796 df-1st 7914 df-2nd 7915 df-frecs 8205 df-wrecs 8236 df-recs 8310 df-rdg 8349 df-er 8607 df-map 8726 df-en 8843 df-dom 8844 df-sdom 8845 df-sup 9337 df-pnf 11150 df-mnf 11151 df-xr 11152 df-ltxr 11153 df-le 11154 df-sub 11346 df-neg 11347 df-div 11772 df-nn 12113 df-2 12175 df-3 12176 df-n0 12373 df-z 12459 df-uz 12723 df-rp 12871 df-seq 13862 df-exp 13923 df-cj 14944 df-re 14945 df-im 14946 df-sqrt 15080 df-abs 15081 df-grpo 29264 df-gid 29265 df-ginv 29266 df-ablo 29316 df-vc 29330 df-nv 29363 df-va 29366 df-ba 29367 df-sm 29368 df-0v 29369 df-nmcv 29371 df-lno 29515 df-nmoo 29516 df-0o 29518 |
This theorem is referenced by: nmlno0 29566 nmlnop0iHIL 30767 |
Copyright terms: Public domain | W3C validator |