Metamath Proof Explorer


Theorem hilnormi

Description: Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hilnorm.5 =BaseSetU
hilnorm.2 ih=𝑖OLDU
hilnorm.9 UNrmCVec
Assertion hilnormi norm=normCVU

Proof

Step Hyp Ref Expression
1 hilnorm.5 =BaseSetU
2 hilnorm.2 ih=𝑖OLDU
3 hilnorm.9 UNrmCVec
4 eqid normCVU=normCVU
5 1 4 2 ipnm UNrmCVecxnormCVUx=xihx
6 3 5 mpan xnormCVUx=xihx
7 6 mpteq2ia xnormCVUx=xxihx
8 1 4 nvf UNrmCVecnormCVU:
9 8 feqmptd UNrmCVecnormCVU=xnormCVUx
10 3 9 ax-mp normCVU=xnormCVUx
11 dfhnorm2 norm=xxihx
12 7 10 11 3eqtr4ri norm=normCVU