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

Theorem smfval 27740
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 27732 . . . . 5 ·𝑠OLD = (2nd ∘ 1st )
32fveq1i 6341 . . . 4 ( ·𝑠OLD𝑈) = ((2nd ∘ 1st )‘𝑈)
4 fo1st 7341 . . . . . 6 1st :V–onto→V
5 fof 6264 . . . . . 6 (1st :V–onto→V → 1st :V⟶V)
64, 5ax-mp 5 . . . . 5 1st :V⟶V
7 fvco3 6425 . . . . 5 ((1st :V⟶V ∧ 𝑈 ∈ V) → ((2nd ∘ 1st )‘𝑈) = (2nd ‘(1st𝑈)))
86, 7mpan 708 . . . 4 (𝑈 ∈ V → ((2nd ∘ 1st )‘𝑈) = (2nd ‘(1st𝑈)))
93, 8syl5eq 2794 . . 3 (𝑈 ∈ V → ( ·𝑠OLD𝑈) = (2nd ‘(1st𝑈)))
10 fvprc 6334 . . . 4 𝑈 ∈ V → ( ·𝑠OLD𝑈) = ∅)
11 fvprc 6334 . . . . . 6 𝑈 ∈ V → (1st𝑈) = ∅)
1211fveq2d 6344 . . . . 5 𝑈 ∈ V → (2nd ‘(1st𝑈)) = (2nd ‘∅))
13 2nd0 7328 . . . . 5 (2nd ‘∅) = ∅
1412, 13syl6req 2799 . . . 4 𝑈 ∈ V → ∅ = (2nd ‘(1st𝑈)))
1510, 14eqtrd 2782 . . 3 𝑈 ∈ V → ( ·𝑠OLD𝑈) = (2nd ‘(1st𝑈)))
169, 15pm2.61i 176 . 2 ( ·𝑠OLD𝑈) = (2nd ‘(1st𝑈))
171, 16eqtri 2770 1 𝑆 = (2nd ‘(1st𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1620  wcel 2127  Vcvv 3328  c0 4046  ccom 5258  wf 6033  ontowfo 6035  cfv 6037  1st c1st 7319  2nd c2nd 7320   ·𝑠OLD cns 27722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-fo 6043  df-fv 6045  df-1st 7321  df-2nd 7322  df-sm 27732
This theorem is referenced by:  nvvop  27744  nvsf  27754  nvscl  27761  nvsid  27762  nvsass  27763  nvdi  27765  nvdir  27766  nv2  27767  nv0  27772  nvsz  27773  nvinv  27774  nvtri  27805  cnnvs  27815  phop  27953  phpar  27959  ipdirilem  27964  h2hsm  28112  hhsssm  28395
  Copyright terms: Public domain W3C validator