Theorem normsqi

Description: The square of a norm. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	normcl.1	|- A e. ~H
Assertion	normsqi	|- ( ( normh ` A ) ^ 2 ) = ( A .ih A )

Proof

Step	Hyp	Ref	Expression
1		normcl.1	|- A e. ~H
2		normval	|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )
3	1 2	ax-mp	|- ( normh ` A ) = ( sqrt ` ( A .ih A ) )
4	3	oveq1i	|- ( ( normh ` A ) ^ 2 ) = ( ( sqrt ` ( A .ih A ) ) ^ 2 )
5		hiidge0	|- ( A e. ~H -> 0 <_ ( A .ih A ) )
6	1 5	ax-mp	|- 0 <_ ( A .ih A )
7		hiidrcl	|- ( A e. ~H -> ( A .ih A ) e. RR )
8	1 7	ax-mp	|- ( A .ih A ) e. RR
9	8	sqsqrti	|- ( 0 <_ ( A .ih A ) -> ( ( sqrt ` ( A .ih A ) ) ^ 2 ) = ( A .ih A ) )
10	6 9	ax-mp	|- ( ( sqrt ` ( A .ih A ) ) ^ 2 ) = ( A .ih A )
11	4 10	eqtri	|- ( ( normh ` A ) ^ 2 ) = ( A .ih A )