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 )