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

Theorem tcphval 24734
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 6891 . . . . . . 7 (𝑀 = π‘Š β†’ (Baseβ€˜π‘€) = (Baseβ€˜π‘Š))
4 tcphval.v . . . . . . 7 𝑉 = (Baseβ€˜π‘Š)
53, 4eqtr4di 2790 . . . . . 6 (𝑀 = π‘Š β†’ (Baseβ€˜π‘€) = 𝑉)
6 fveq2 6891 . . . . . . . . 9 (𝑀 = π‘Š β†’ (Β·π‘–β€˜π‘€) = (Β·π‘–β€˜π‘Š))
7 tcphval.h . . . . . . . . 9 , = (Β·π‘–β€˜π‘Š)
86, 7eqtr4di 2790 . . . . . . . 8 (𝑀 = π‘Š β†’ (Β·π‘–β€˜π‘€) = , )
98oveqd 7425 . . . . . . 7 (𝑀 = π‘Š β†’ (π‘₯(Β·π‘–β€˜π‘€)π‘₯) = (π‘₯ , π‘₯))
109fveq2d 6895 . . . . . 6 (𝑀 = π‘Š β†’ (βˆšβ€˜(π‘₯(Β·π‘–β€˜π‘€)π‘₯)) = (βˆšβ€˜(π‘₯ , π‘₯)))
115, 10mpteq12dv 5239 . . . . 5 (𝑀 = π‘Š β†’ (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (βˆšβ€˜(π‘₯(Β·π‘–β€˜π‘€)π‘₯))) = (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯))))
122, 11oveq12d 7426 . . . 4 (𝑀 = π‘Š β†’ (𝑀 toNrmGrp (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (βˆšβ€˜(π‘₯(Β·π‘–β€˜π‘€)π‘₯)))) = (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯)))))
13 df-tcph 24685 . . . 4 toβ„‚PreHil = (𝑀 ∈ V ↦ (𝑀 toNrmGrp (π‘₯ ∈ (Baseβ€˜π‘€) ↦ (βˆšβ€˜(π‘₯(Β·π‘–β€˜π‘€)π‘₯)))))
14 ovex 7441 . . . 4 (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯)))) ∈ V
1512, 13, 14fvmpt 6998 . . 3 (π‘Š ∈ V β†’ (toβ„‚PreHilβ€˜π‘Š) = (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯)))))
16 fvprc 6883 . . . 4 (Β¬ π‘Š ∈ V β†’ (toβ„‚PreHilβ€˜π‘Š) = βˆ…)
17 reldmtng 24146 . . . . 5 Rel dom toNrmGrp
1817ovprc1 7447 . . . 4 (Β¬ π‘Š ∈ V β†’ (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯)))) = βˆ…)
1916, 18eqtr4d 2775 . . 3 (Β¬ π‘Š ∈ V β†’ (toβ„‚PreHilβ€˜π‘Š) = (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯)))))
2015, 19pm2.61i 182 . 2 (toβ„‚PreHilβ€˜π‘Š) = (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯))))
211, 20eqtri 2760 1 𝐺 = (π‘Š toNrmGrp (π‘₯ ∈ 𝑉 ↦ (βˆšβ€˜(π‘₯ , π‘₯))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   = wceq 1541   ∈ wcel 2106  Vcvv 3474  βˆ…c0 4322   ↦ cmpt 5231  β€˜cfv 6543  (class class class)co 7408  βˆšcsqrt 15179  Basecbs 17143  Β·π‘–cip 17201   toNrmGrp ctng 24086  toβ„‚PreHilctcph 24683
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-tng 24092  df-tcph 24685
This theorem is referenced by:  tcphbas  24735  tchplusg  24736  tcphmulr  24738  tcphsca  24739  tcphvsca  24740  tcphip  24741  tcphtopn  24742  tchnmfval  24744  tcphds  24747  tcphcph  24753  rrxsca  24912  rrx0  24913  rrxdim  32694
  Copyright terms: Public domain W3C validator