![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > vafval | Structured version Unicode version |
Description: Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
vafval.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
vafval |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vafval.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-va 24094 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | fveq1i 5776 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | fo1st 6682 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | fof 5704 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | ax-mp 5 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
7 | fvco3 5853 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | mpan 670 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | syl5eq 2502 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | fvprc 5769 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | fvprc 5769 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | 11 | fveq2d 5779 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 1st0 6669 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | 12, 13 | syl6req 2507 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 10, 14 | eqtrd 2490 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 9, 15 | pm2.61i 164 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 1, 16 | eqtri 2478 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-sep 4497 ax-nul 4505 ax-pow 4554 ax-pr 4615 ax-un 6458 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-ral 2797 df-rex 2798 df-rab 2801 df-v 3056 df-sbc 3271 df-dif 3415 df-un 3417 df-in 3419 df-ss 3426 df-nul 3722 df-if 3876 df-sn 3962 df-pr 3964 df-op 3968 df-uni 4176 df-br 4377 df-opab 4435 df-mpt 4436 df-id 4720 df-xp 4930 df-rel 4931 df-cnv 4932 df-co 4933 df-dm 4934 df-rn 4935 df-res 4936 df-ima 4937 df-iota 5465 df-fun 5504 df-fn 5505 df-f 5506 df-fo 5508 df-fv 5510 df-1st 6663 df-va 24094 |
This theorem is referenced by: nvvop 24108 nvablo 24115 nvsf 24118 nvscl 24127 nvsid 24128 nvsass 24129 nvdi 24131 nvdir 24132 nv2 24133 nv0 24138 nvsz 24139 nvinv 24140 cnnvg 24189 phop 24339 phpar 24345 ip0i 24346 ipdirilem 24350 h2hva 24497 hhssva 24781 hhshsslem1 24789 |
Copyright terms: Public domain | W3C validator |