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

Metamath Proof Explorer

Theorem sqabsadd

Description: Square of absolute value of sum. Proposition 10-3.7(g) of Gleason p. 133. (Contributed by NM, 21-Jan-2007)

Ref Expression
Assertion sqabsadd 
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cjadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )
2 1 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( * ` ( A + B ) ) ) = ( ( A + B ) x. ( ( * ` A ) + ( * ` B ) ) ) )
3 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
4 cjcl 
 |-  ( B e. CC -> ( * ` B ) e. CC )
5 3 4 anim12i 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) e. CC /\ ( * ` B ) e. CC ) )
6 muladd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( * ` A ) e. CC /\ ( * ` B ) e. CC ) ) -> ( ( A + B ) x. ( ( * ` A ) + ( * ` B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) + ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
7 5 6 mpdan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( ( * ` A ) + ( * ` B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) + ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
8 2 7 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( * ` ( A + B ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) + ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
9 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
10 absvalsq 
 |-  ( ( A + B ) e. CC -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( A + B ) x. ( * ` ( A + B ) ) ) )
11 9 10 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( A + B ) x. ( * ` ( A + B ) ) ) )
12 absvalsq 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
13 absvalsq 
 |-  ( B e. CC -> ( ( abs ` B ) ^ 2 ) = ( B x. ( * ` B ) ) )
14 mulcom 
 |-  ( ( B e. CC /\ ( * ` B ) e. CC ) -> ( B x. ( * ` B ) ) = ( ( * ` B ) x. B ) )
15 4 14 mpdan 
 |-  ( B e. CC -> ( B x. ( * ` B ) ) = ( ( * ` B ) x. B ) )
16 13 15 eqtrd 
 |-  ( B e. CC -> ( ( abs ` B ) ^ 2 ) = ( ( * ` B ) x. B ) )
17 12 16 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) = ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) )
18 mulcl 
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( A x. ( * ` B ) ) e. CC )
19 4 18 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( * ` B ) ) e. CC )
20 19 addcjd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( * ` B ) ) + ( * ` ( A x. ( * ` B ) ) ) ) = ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) )
21 cjmul 
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. ( * ` ( * ` B ) ) ) )
22 4 21 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. ( * ` ( * ` B ) ) ) )
23 cjcj 
 |-  ( B e. CC -> ( * ` ( * ` B ) ) = B )
24 23 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( * ` B ) ) = B )
25 24 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) x. ( * ` ( * ` B ) ) ) = ( ( * ` A ) x. B ) )
26 22 25 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. ( * ` B ) ) ) = ( ( * ` A ) x. B ) )
27 26 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( * ` B ) ) + ( * ` ( A x. ( * ` B ) ) ) ) = ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) )
28 20 27 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) = ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) )
29 17 28 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) = ( ( ( A x. ( * ` A ) ) + ( ( * ` B ) x. B ) ) + ( ( A x. ( * ` B ) ) + ( ( * ` A ) x. B ) ) ) )
30 8 11 29 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )