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

Theorem vsfval 28419
 Description: Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
vsfval.2 𝐺 = ( +𝑣𝑈)
vsfval.3 𝑀 = ( −𝑣𝑈)
Assertion
Ref Expression
vsfval 𝑀 = ( /𝑔𝐺)

Proof of Theorem vsfval
Dummy variables 𝑥 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-vs 28385 . . . . 5 𝑣 = ( /𝑔 ∘ +𝑣 )
21fveq1i 6662 . . . 4 ( −𝑣𝑈) = (( /𝑔 ∘ +𝑣 )‘𝑈)
3 fo1st 7704 . . . . . . . 8 1st :V–onto→V
4 fof 6581 . . . . . . . 8 (1st :V–onto→V → 1st :V⟶V)
53, 4ax-mp 5 . . . . . . 7 1st :V⟶V
6 fco 6521 . . . . . . 7 ((1st :V⟶V ∧ 1st :V⟶V) → (1st ∘ 1st ):V⟶V)
75, 5, 6mp2an 691 . . . . . 6 (1st ∘ 1st ):V⟶V
8 df-va 28381 . . . . . . 7 +𝑣 = (1st ∘ 1st )
98feq1i 6494 . . . . . 6 ( +𝑣 :V⟶V ↔ (1st ∘ 1st ):V⟶V)
107, 9mpbir 234 . . . . 5 +𝑣 :V⟶V
11 fvco3 6751 . . . . 5 (( +𝑣 :V⟶V ∧ 𝑈 ∈ V) → (( /𝑔 ∘ +𝑣 )‘𝑈) = ( /𝑔 ‘( +𝑣𝑈)))
1210, 11mpan 689 . . . 4 (𝑈 ∈ V → (( /𝑔 ∘ +𝑣 )‘𝑈) = ( /𝑔 ‘( +𝑣𝑈)))
132, 12syl5eq 2871 . . 3 (𝑈 ∈ V → ( −𝑣𝑈) = ( /𝑔 ‘( +𝑣𝑈)))
14 0ngrp 28297 . . . . . 6 ¬ ∅ ∈ GrpOp
15 vex 3483 . . . . . . . . . 10 𝑔 ∈ V
1615rnex 7612 . . . . . . . . 9 ran 𝑔 ∈ V
1716, 16mpoex 7773 . . . . . . . 8 (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))) ∈ V
18 df-gdiv 28282 . . . . . . . 8 /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
1917, 18dmmpti 6481 . . . . . . 7 dom /𝑔 = GrpOp
2019eleq2i 2907 . . . . . 6 (∅ ∈ dom /𝑔 ↔ ∅ ∈ GrpOp)
2114, 20mtbir 326 . . . . 5 ¬ ∅ ∈ dom /𝑔
22 ndmfv 6691 . . . . 5 (¬ ∅ ∈ dom /𝑔 → ( /𝑔 ‘∅) = ∅)
2321, 22mp1i 13 . . . 4 𝑈 ∈ V → ( /𝑔 ‘∅) = ∅)
24 fvprc 6654 . . . . 5 𝑈 ∈ V → ( +𝑣𝑈) = ∅)
2524fveq2d 6665 . . . 4 𝑈 ∈ V → ( /𝑔 ‘( +𝑣𝑈)) = ( /𝑔 ‘∅))
26 fvprc 6654 . . . 4 𝑈 ∈ V → ( −𝑣𝑈) = ∅)
2723, 25, 263eqtr4rd 2870 . . 3 𝑈 ∈ V → ( −𝑣𝑈) = ( /𝑔 ‘( +𝑣𝑈)))
2813, 27pm2.61i 185 . 2 ( −𝑣𝑈) = ( /𝑔 ‘( +𝑣𝑈))
29 vsfval.3 . 2 𝑀 = ( −𝑣𝑈)
30 vsfval.2 . . 3 𝐺 = ( +𝑣𝑈)
3130fveq2i 6664 . 2 ( /𝑔𝐺) = ( /𝑔 ‘( +𝑣𝑈))
3228, 29, 313eqtr4i 2857 1 𝑀 = ( /𝑔𝐺)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2115  Vcvv 3480  ∅c0 4276  dom cdm 5542  ran crn 5543   ∘ ccom 5546  ⟶wf 6339  –onto→wfo 6341  ‘cfv 6343  (class class class)co 7149   ∈ cmpo 7151  1st c1st 7682  GrpOpcgr 28275  invcgn 28277   /𝑔 cgs 28278   +𝑣 cpv 28371   −𝑣 cnsb 28375 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7684  df-2nd 7685  df-grpo 28279  df-gdiv 28282  df-va 28381  df-vs 28385 This theorem is referenced by:  nvm  28427  nvmfval  28430  nvnnncan1  28433  nvaddsub  28441
 Copyright terms: Public domain W3C validator