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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cjadd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) )
2 1 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( ∗ ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( 𝐴 + 𝐵 ) · ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) ) )
3 cjcl ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
4 cjcl ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
5 3 4 anim12i ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) )
6 muladd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
7 5 6 mpdan ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
8 2 7 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( ∗ ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
9 addcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
10 absvalsq ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) · ( ∗ ‘ ( 𝐴 + 𝐵 ) ) ) )
11 9 10 syl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) · ( ∗ ‘ ( 𝐴 + 𝐵 ) ) ) )
12 absvalsq ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
13 absvalsq ( 𝐵 ∈ ℂ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 · ( ∗ ‘ 𝐵 ) ) )
14 mulcom ( ( 𝐵 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) )
15 4 14 mpdan ( 𝐵 ∈ ℂ → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) )
16 13 15 eqtrd ( 𝐵 ∈ ℂ → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( ( ∗ ‘ 𝐵 ) · 𝐵 ) )
17 12 16 oveqan12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) )
18 mulcl ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
19 4 18 sylan2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
20 19 addcjd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) )
21 cjmul ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) )
22 4 21 sylan2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) )
23 cjcj ( 𝐵 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
24 23 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
25 24 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐵 ) )
26 22 25 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · 𝐵 ) )
27 26 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ∗ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
28 20 27 eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) )
29 17 28 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) = ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) + ( ( ∗ ‘ 𝐵 ) · 𝐵 ) ) + ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) + ( ( ∗ ‘ 𝐴 ) · 𝐵 ) ) ) )
30 8 11 29 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) )