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

Metamath Proof Explorer

Theorem bhmafibid1cn

Description: The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023)

Ref Expression
Assertion bhmafibid1cn ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐴 ∈ ℂ )
2 1 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐶 ∈ ℂ )
4 3 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
5 2 4 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
6 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐷 ∈ ℂ )
7 6 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
8 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
9 8 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
10 7 9 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
11 2 7 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ∈ ℂ )
12 4 9 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
13 5 10 11 12 add4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) )
14 7 9 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
15 4 9 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
16 14 15 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
17 16 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
18 13 17 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
19 2 9 4 7 muladdd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) )
20 1 3 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
21 8 6 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
22 binom2sub ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐵 · 𝐷 ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( 𝐵 · 𝐷 ) ↑ 2 ) ) )
23 20 21 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( 𝐵 · 𝐷 ) ↑ 2 ) ) )
24 1 6 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
25 8 3 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
26 binom2 ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
27 24 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
28 23 27 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) = ( ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( 𝐵 · 𝐷 ) ↑ 2 ) ) + ( ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) ) )
29 20 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) ↑ 2 ) ∈ ℂ )
30 2cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → 2 ∈ ℂ )
31 20 21 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ∈ ℂ )
32 30 31 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ∈ ℂ )
33 29 32 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) ∈ ℂ )
34 21 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 · 𝐷 ) ↑ 2 ) ∈ ℂ )
35 24 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) ↑ 2 ) ∈ ℂ )
36 24 25 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
37 30 36 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
38 35 37 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ∈ ℂ )
39 25 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 · 𝐶 ) ↑ 2 ) ∈ ℂ )
40 33 34 38 39 add4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( 𝐵 · 𝐷 ) ↑ 2 ) ) + ( ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) ) = ( ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) + ( ( ( 𝐵 · 𝐷 ) ↑ 2 ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) ) )
41 mul4r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) )
42 41 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) )
43 42 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) = ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) )
44 43 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) = ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) )
45 44 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) )
46 29 37 35 nppcan3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) )
47 45 46 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) = ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) )
48 8 6 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 · 𝐷 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
49 8 3 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 · 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
50 48 49 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐵 · 𝐷 ) ↑ 2 ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
51 47 50 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) + ( ( ( 𝐵 · 𝐷 ) ↑ 2 ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
52 1 3 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
53 1 6 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
54 52 53 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) )
55 54 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
56 51 55 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( ( 𝐴 · 𝐶 ) ↑ 2 ) − ( 2 · ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) ) ) + ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) + ( 2 · ( ( 𝐴 · 𝐷 ) · ( 𝐵 · 𝐶 ) ) ) ) ) + ( ( ( 𝐵 · 𝐷 ) ↑ 2 ) + ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
57 28 40 56 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
58 18 19 57 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )