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

Theorem tcphval 23386
Description: Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.)
Hypotheses
Ref Expression
tcphval.n 𝐺 = (toℂPreHil‘𝑊)
tcphval.v 𝑉 = (Base‘𝑊)
tcphval.h , = (·𝑖𝑊)
Assertion
Ref Expression
tcphval 𝐺 = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥))))
Distinct variable groups:   𝑥, ,   𝑥,𝐺   𝑥,𝑉   𝑥,𝑊

Proof of Theorem tcphval
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 tcphval.n . 2 𝐺 = (toℂPreHil‘𝑊)
2 id 22 . . . . 5 (𝑤 = 𝑊𝑤 = 𝑊)
3 fveq2 6433 . . . . . . 7 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4 tcphval.v . . . . . . 7 𝑉 = (Base‘𝑊)
53, 4syl6eqr 2879 . . . . . 6 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
6 fveq2 6433 . . . . . . . . 9 (𝑤 = 𝑊 → (·𝑖𝑤) = (·𝑖𝑊))
7 tcphval.h . . . . . . . . 9 , = (·𝑖𝑊)
86, 7syl6eqr 2879 . . . . . . . 8 (𝑤 = 𝑊 → (·𝑖𝑤) = , )
98oveqd 6922 . . . . . . 7 (𝑤 = 𝑊 → (𝑥(·𝑖𝑤)𝑥) = (𝑥 , 𝑥))
109fveq2d 6437 . . . . . 6 (𝑤 = 𝑊 → (√‘(𝑥(·𝑖𝑤)𝑥)) = (√‘(𝑥 , 𝑥)))
115, 10mpteq12dv 4956 . . . . 5 (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))) = (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥))))
122, 11oveq12d 6923 . . . 4 (𝑤 = 𝑊 → (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))) = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥)))))
13 df-tcph 23338 . . . 4 toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
14 ovex 6937 . . . 4 (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥)))) ∈ V
1512, 13, 14fvmpt 6529 . . 3 (𝑊 ∈ V → (toℂPreHil‘𝑊) = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥)))))
16 fvprc 6426 . . . 4 𝑊 ∈ V → (toℂPreHil‘𝑊) = ∅)
17 reldmtng 22812 . . . . 5 Rel dom toNrmGrp
1817ovprc1 6943 . . . 4 𝑊 ∈ V → (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥)))) = ∅)
1916, 18eqtr4d 2864 . . 3 𝑊 ∈ V → (toℂPreHil‘𝑊) = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥)))))
2015, 19pm2.61i 177 . 2 (toℂPreHil‘𝑊) = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥))))
211, 20eqtri 2849 1 𝐺 = (𝑊 toNrmGrp (𝑥𝑉 ↦ (√‘(𝑥 , 𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1658  wcel 2166  Vcvv 3414  c0 4144  cmpt 4952  cfv 6123  (class class class)co 6905  csqrt 14350  Basecbs 16222  ·𝑖cip 16310   toNrmGrp ctng 22753  toℂPreHilctcph 23336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-iota 6086  df-fun 6125  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-tng 22759  df-tcph 23338
This theorem is referenced by:  tcphbas  23387  tchplusg  23388  tcphmulr  23390  tcphsca  23391  tcphvsca  23392  tcphip  23393  tcphtopn  23394  tchnmfval  23396  tcphds  23399  tcphcph  23405  rrxsca  23564  rrx0  23565
  Copyright terms: Public domain W3C validator