Metamath Proof Explorer

Theorem absmul

Description: Absolute value distributes over multiplication. Proposition 10-3.7(f) of Gleason p. 133. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absmul 
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 cjmul 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) )
2 1 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) x. ( * ` ( A x. B ) ) ) = ( ( A x. B ) x. ( ( * ` A ) x. ( * ` B ) ) ) )
3 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 3 cjcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` A ) e. CC )
6 4 cjcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` B ) e. CC )
7 3 4 5 6 mul4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) x. ( ( * ` A ) x. ( * ` B ) ) ) = ( ( A x. ( * ` A ) ) x. ( B x. ( * ` B ) ) ) )
8 2 7 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) x. ( * ` ( A x. B ) ) ) = ( ( A x. ( * ` A ) ) x. ( B x. ( * ` B ) ) ) )
9 8 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sqrt ` ( ( A x. B ) x. ( * ` ( A x. B ) ) ) ) = ( sqrt ` ( ( A x. ( * ` A ) ) x. ( B x. ( * ` B ) ) ) ) )
10 cjmulrcl 
 |-  ( A e. CC -> ( A x. ( * ` A ) ) e. RR )
11 cjmulge0 
 |-  ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )
12 10 11 jca 
 |-  ( A e. CC -> ( ( A x. ( * ` A ) ) e. RR /\ 0 <_ ( A x. ( * ` A ) ) ) )
13 cjmulrcl 
 |-  ( B e. CC -> ( B x. ( * ` B ) ) e. RR )
14 cjmulge0 
 |-  ( B e. CC -> 0 <_ ( B x. ( * ` B ) ) )
15 13 14 jca 
 |-  ( B e. CC -> ( ( B x. ( * ` B ) ) e. RR /\ 0 <_ ( B x. ( * ` B ) ) ) )
16 sqrtmul 
 |-  ( ( ( ( A x. ( * ` A ) ) e. RR /\ 0 <_ ( A x. ( * ` A ) ) ) /\ ( ( B x. ( * ` B ) ) e. RR /\ 0 <_ ( B x. ( * ` B ) ) ) ) -> ( sqrt ` ( ( A x. ( * ` A ) ) x. ( B x. ( * ` B ) ) ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B x. ( * ` B ) ) ) ) )
17 12 15 16 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sqrt ` ( ( A x. ( * ` A ) ) x. ( B x. ( * ` B ) ) ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B x. ( * ` B ) ) ) ) )
18 9 17 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sqrt ` ( ( A x. B ) x. ( * ` ( A x. B ) ) ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B x. ( * ` B ) ) ) ) )
19 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
20 absval 
 |-  ( ( A x. B ) e. CC -> ( abs ` ( A x. B ) ) = ( sqrt ` ( ( A x. B ) x. ( * ` ( A x. B ) ) ) ) )
21 19 20 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. B ) ) = ( sqrt ` ( ( A x. B ) x. ( * ` ( A x. B ) ) ) ) )
22 absval 
 |-  ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
23 absval 
 |-  ( B e. CC -> ( abs ` B ) = ( sqrt ` ( B x. ( * ` B ) ) ) )
24 22 23 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) x. ( abs ` B ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B x. ( * ` B ) ) ) ) )
25 18 21 24 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )