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 ) ) ) ) ) )