This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absval

Description: The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of Gleason p. 133. (Contributed by NM, 27-Jul-1999) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion absval 
|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = A -> ( * ` x ) = ( * ` A ) )
2 oveq12 
 |-  ( ( x = A /\ ( * ` x ) = ( * ` A ) ) -> ( x x. ( * ` x ) ) = ( A x. ( * ` A ) ) )
3 1 2 mpdan 
 |-  ( x = A -> ( x x. ( * ` x ) ) = ( A x. ( * ` A ) ) )
4 3 fveq2d 
 |-  ( x = A -> ( sqrt ` ( x x. ( * ` x ) ) ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
5 df-abs 
 |-  abs = ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) )
6 fvex 
 |-  ( sqrt ` ( A x. ( * ` A ) ) ) e. _V
7 4 5 6 fvmpt 
 |-  ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )