Metamath Proof Explorer


Theorem normsq

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

Ref Expression
Assertion normsq AnormA2=AihA

Proof

Step Hyp Ref Expression
1 fveq2 A=ifAA0normA=normifAA0
2 1 oveq1d A=ifAA0normA2=normifAA02
3 id A=ifAA0A=ifAA0
4 3 3 oveq12d A=ifAA0AihA=ifAA0ihifAA0
5 2 4 eqeq12d A=ifAA0normA2=AihAnormifAA02=ifAA0ihifAA0
6 ifhvhv0 ifAA0
7 6 normsqi normifAA02=ifAA0ihifAA0
8 5 7 dedth AnormA2=AihA