Theorem nmsq

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmsq.v	|- V = ( Base ` W )
	nmsq.h	|- ., = ( .i ` W )
	nmsq.n	|- N = ( norm ` W )
Assertion	nmsq	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( 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	cphnm	|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( A ., A ) ) )
5	4	oveq1d	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( ( sqrt ` ( A ., A ) ) ^ 2 ) )
6	1 2	cphipcl	|- ( ( W e. CPreHil /\ A e. V /\ A e. V ) -> ( A ., A ) e. CC )
7	6	3anidm23	|- ( ( W e. CPreHil /\ A e. V ) -> ( A ., A ) e. CC )
8	7	sqsqrtd	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( sqrt ` ( A ., A ) ) ^ 2 ) = ( A ., A ) )
9	5 8	eqtrd	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )