Theorem normsq

Description: The square of a norm. (Contributed by NM, 12-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	normsq	|- ( A e. ~H -> ( ( normh ` A ) ^ 2 ) = ( A .ih A ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( A = if ( A e. ~H , A , 0h ) -> ( normh ` A ) = ( normh ` if ( A e. ~H , A , 0h ) ) )
2	1	oveq1d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` A ) ^ 2 ) = ( ( normh ` if ( A e. ~H , A , 0h ) ) ^ 2 ) )
3		id	|- ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )
4	3 3	oveq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( A .ih A ) = ( if ( A e. ~H , A , 0h ) .ih if ( A e. ~H , A , 0h ) ) )
5	2 4	eqeq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( normh ` A ) ^ 2 ) = ( A .ih A ) <-> ( ( normh ` if ( A e. ~H , A , 0h ) ) ^ 2 ) = ( if ( A e. ~H , A , 0h ) .ih if ( A e. ~H , A , 0h ) ) ) )
6		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
7	6	normsqi	|- ( ( normh ` if ( A e. ~H , A , 0h ) ) ^ 2 ) = ( if ( A e. ~H , A , 0h ) .ih if ( A e. ~H , A , 0h ) )
8	5 7	dedth	|- ( A e. ~H -> ( ( normh ` A ) ^ 2 ) = ( A .ih A ) )