MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  smfval Structured version   Visualization version   GIF version

Theorem smfval 30125
Description: Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
Hypothesis
Ref Expression
smfval.4 ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
Assertion
Ref Expression
smfval ๐‘† = (2nd โ€˜(1st โ€˜๐‘ˆ))

Proof of Theorem smfval
StepHypRef Expression
1 smfval.4 . 2 ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
2 df-sm 30117 . . . . 5 ยท๐‘ OLD = (2nd โˆ˜ 1st )
32fveq1i 6891 . . . 4 ( ยท๐‘ OLD โ€˜๐‘ˆ) = ((2nd โˆ˜ 1st )โ€˜๐‘ˆ)
4 fo1st 7997 . . . . . 6 1st :Vโ€“ontoโ†’V
5 fof 6804 . . . . . 6 (1st :Vโ€“ontoโ†’V โ†’ 1st :VโŸถV)
64, 5ax-mp 5 . . . . 5 1st :VโŸถV
7 fvco3 6989 . . . . 5 ((1st :VโŸถV โˆง ๐‘ˆ โˆˆ V) โ†’ ((2nd โˆ˜ 1st )โ€˜๐‘ˆ) = (2nd โ€˜(1st โ€˜๐‘ˆ)))
86, 7mpan 686 . . . 4 (๐‘ˆ โˆˆ V โ†’ ((2nd โˆ˜ 1st )โ€˜๐‘ˆ) = (2nd โ€˜(1st โ€˜๐‘ˆ)))
93, 8eqtrid 2782 . . 3 (๐‘ˆ โˆˆ V โ†’ ( ยท๐‘ OLD โ€˜๐‘ˆ) = (2nd โ€˜(1st โ€˜๐‘ˆ)))
10 fvprc 6882 . . . 4 (ยฌ ๐‘ˆ โˆˆ V โ†’ ( ยท๐‘ OLD โ€˜๐‘ˆ) = โˆ…)
11 fvprc 6882 . . . . . 6 (ยฌ ๐‘ˆ โˆˆ V โ†’ (1st โ€˜๐‘ˆ) = โˆ…)
1211fveq2d 6894 . . . . 5 (ยฌ ๐‘ˆ โˆˆ V โ†’ (2nd โ€˜(1st โ€˜๐‘ˆ)) = (2nd โ€˜โˆ…))
13 2nd0 7984 . . . . 5 (2nd โ€˜โˆ…) = โˆ…
1412, 13eqtr2di 2787 . . . 4 (ยฌ ๐‘ˆ โˆˆ V โ†’ โˆ… = (2nd โ€˜(1st โ€˜๐‘ˆ)))
1510, 14eqtrd 2770 . . 3 (ยฌ ๐‘ˆ โˆˆ V โ†’ ( ยท๐‘ OLD โ€˜๐‘ˆ) = (2nd โ€˜(1st โ€˜๐‘ˆ)))
169, 15pm2.61i 182 . 2 ( ยท๐‘ OLD โ€˜๐‘ˆ) = (2nd โ€˜(1st โ€˜๐‘ˆ))
171, 16eqtri 2758 1 ๐‘† = (2nd โ€˜(1st โ€˜๐‘ˆ))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   = wceq 1539   โˆˆ wcel 2104  Vcvv 3472  โˆ…c0 4321   โˆ˜ ccom 5679  โŸถwf 6538  โ€“ontoโ†’wfo 6540  โ€˜cfv 6542  1st c1st 7975  2nd c2nd 7976   ยท๐‘ OLD cns 30107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fo 6548  df-fv 6550  df-1st 7977  df-2nd 7978  df-sm 30117
This theorem is referenced by:  nvvop  30129  nvsf  30139  nvscl  30146  nvsid  30147  nvsass  30148  nvdi  30150  nvdir  30151  nv2  30152  nv0  30157  nvsz  30158  nvinv  30159  nvtri  30190  cnnvs  30200  phop  30338  ipdirilem  30349  h2hsm  30495  hhsssm  30778
  Copyright terms: Public domain W3C validator