![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imsdval | Structured version Visualization version Unicode version |
Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.) |
Ref | Expression |
---|---|
imsdval.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imsdval.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imsdval.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imsdval.8 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imsdval |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imsdval.3 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | imsdval.6 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | imsdval.8 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | imsval 26329 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | 3ad2ant1 1030 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | fveq1d 5872 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | imsdval.1 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7, 1 | nvmf 26279 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | opelxpi 4869 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | fvco3 5947 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 8, 9, 10 | syl2an 480 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | 3impb 1205 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 6, 12 | eqtrd 2487 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | df-ov 6298 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | df-ov 6298 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 15 | fveq2i 5873 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 13, 14, 16 | 3eqtr4g 2512 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-po 4758 df-so 4759 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-1st 6798 df-2nd 6799 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-pnf 9682 df-mnf 9683 df-ltxr 9685 df-sub 9867 df-neg 9868 df-grpo 25931 df-gid 25932 df-ginv 25933 df-gdiv 25934 df-ablo 26022 df-vc 26177 df-nv 26223 df-va 26226 df-ba 26227 df-sm 26228 df-0v 26229 df-vs 26230 df-nmcv 26231 df-ims 26232 |
This theorem is referenced by: imsdval2 26331 nvnd 26332 nvelbl 26337 vacn 26342 smcnlem 26345 sspimsval 26391 blometi 26456 blocnilem 26457 ubthlem2 26525 minvecolem2 26529 minvecolem4 26534 minvecolem5 26535 minvecolem6 26536 minvecolem2OLD 26539 minvecolem4OLD 26544 minvecolem5OLD 26545 minvecolem6OLD 26546 h2hmetdval 26643 hhssmetdval 26941 |
Copyright terms: Public domain | W3C validator |