Theorem cphnm

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmsq.v	|- V = ( Base ` W )
	nmsq.h	|- ., = ( .i ` W )
	nmsq.n	|- N = ( norm ` W )
Assertion	cphnm	|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( A ., A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	|- V = ( Base ` W )
2		nmsq.h	|- ., = ( .i ` W )
3		nmsq.n	|- N = ( norm ` W )
4	1 2 3	cphnmfval	|- ( W e. CPreHil -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
5	4	fveq1d	|- ( W e. CPreHil -> ( N ` A ) = ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` A ) )
6		oveq12	|- ( ( x = A /\ x = A ) -> ( x ., x ) = ( A ., A ) )
7	6	anidms	|- ( x = A -> ( x ., x ) = ( A ., A ) )
8	7	fveq2d	|- ( x = A -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( A ., A ) ) )
9		eqid	|- ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
10		fvex	|- ( sqrt ` ( A ., A ) ) e. _V
11	8 9 10	fvmpt	|- ( A e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` A ) = ( sqrt ` ( A ., A ) ) )
12	5 11	sylan9eq	|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( A ., A ) ) )