This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ~H = ( BaseSet ` U )
hilnorm.2 
|- .ih = ( .iOLD ` U )
hilnorm.9 
|- U e. NrmCVec
Assertion hilnormi 
|- normh = ( normCV ` U )

Proof

Step Hyp Ref Expression
1 hilnorm.5 
 |-  ~H = ( BaseSet ` U )
2 hilnorm.2 
 |-  .ih = ( .iOLD ` U )
3 hilnorm.9 
 |-  U e. NrmCVec
4 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
5 1 4 2 ipnm 
 |-  ( ( U e. NrmCVec /\ x e. ~H ) -> ( ( normCV ` U ) ` x ) = ( sqrt ` ( x .ih x ) ) )
6 3 5 mpan 
 |-  ( x e. ~H -> ( ( normCV ` U ) ` x ) = ( sqrt ` ( x .ih x ) ) )
7 6 mpteq2ia 
 |-  ( x e. ~H |-> ( ( normCV ` U ) ` x ) ) = ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) )
8 1 4 nvf 
 |-  ( U e. NrmCVec -> ( normCV ` U ) : ~H --> RR )
9 8 feqmptd 
 |-  ( U e. NrmCVec -> ( normCV ` U ) = ( x e. ~H |-> ( ( normCV ` U ) ` x ) ) )
10 3 9 ax-mp 
 |-  ( normCV ` U ) = ( x e. ~H |-> ( ( normCV ` U ) ` x ) )
11 dfhnorm2 
 |-  normh = ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) )
12 7 10 11 3eqtr4ri 
 |-  normh = ( normCV ` U )