Metamath Proof Explorer

Theorem recextlem1

Description: Lemma for recex . (Contributed by Eric Schmidt, 23-May-2007)

Ref Expression
Assertion recextlem1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
2 ax-icn ⊢ i ∈ ℂ
3 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
4 2 3 mpan ⊢ ( 𝐵 ∈ ℂ → ( i · 𝐵 ) ∈ ℂ )
5 4 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
6 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ ℂ )
7 4 6 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − ( i · 𝐵 ) ) ∈ ℂ )
8 1 5 7 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 · ( 𝐴 − ( i · 𝐵 ) ) ) + ( ( i · 𝐵 ) · ( 𝐴 − ( i · 𝐵 ) ) ) ) )
9 1 1 5 subdid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) − ( 𝐴 · ( i · 𝐵 ) ) ) )
10 5 1 5 subdid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · 𝐵 ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( ( i · 𝐵 ) · 𝐴 ) − ( ( i · 𝐵 ) · ( i · 𝐵 ) ) ) )
11 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( i · 𝐵 ) ) = ( ( i · 𝐵 ) · 𝐴 ) )
12 4 11 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( i · 𝐵 ) ) = ( ( i · 𝐵 ) · 𝐴 ) )
13 ixi ⊢ ( i · i ) = - 1
14 13 oveq1i ⊢ ( ( i · i ) · ( 𝐵 · 𝐵 ) ) = ( - 1 · ( 𝐵 · 𝐵 ) )
15 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · 𝐵 ) ∈ ℂ )
16 15 mulm1d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 1 · ( 𝐵 · 𝐵 ) ) = - ( 𝐵 · 𝐵 ) )
17 14 16 eqtr2id ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 · 𝐵 ) = ( ( i · i ) · ( 𝐵 · 𝐵 ) ) )
18 mul4 ⊢ ( ( ( i ∈ ℂ ∧ i ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( i · i ) · ( 𝐵 · 𝐵 ) ) = ( ( i · 𝐵 ) · ( i · 𝐵 ) ) )
19 2 2 18 mpanl12 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · i ) · ( 𝐵 · 𝐵 ) ) = ( ( i · 𝐵 ) · ( i · 𝐵 ) ) )
20 17 19 eqtrd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 · 𝐵 ) = ( ( i · 𝐵 ) · ( i · 𝐵 ) ) )
21 20 anidms ⊢ ( 𝐵 ∈ ℂ → - ( 𝐵 · 𝐵 ) = ( ( i · 𝐵 ) · ( i · 𝐵 ) ) )
22 21 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 · 𝐵 ) = ( ( i · 𝐵 ) · ( i · 𝐵 ) ) )
23 12 22 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( i · 𝐵 ) ) − - ( 𝐵 · 𝐵 ) ) = ( ( ( i · 𝐵 ) · 𝐴 ) − ( ( i · 𝐵 ) · ( i · 𝐵 ) ) ) )
24 10 23 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · 𝐵 ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 · ( i · 𝐵 ) ) − - ( 𝐵 · 𝐵 ) ) )
25 9 24 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 𝐴 − ( i · 𝐵 ) ) ) + ( ( i · 𝐵 ) · ( 𝐴 − ( i · 𝐵 ) ) ) ) = ( ( ( 𝐴 · 𝐴 ) − ( 𝐴 · ( i · 𝐵 ) ) ) + ( ( 𝐴 · ( i · 𝐵 ) ) − - ( 𝐵 · 𝐵 ) ) ) )
26 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 · 𝐴 ) ∈ ℂ )
27 26 anidms ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 𝐴 ) ∈ ℂ )
28 27 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐴 ) ∈ ℂ )
29 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( i · 𝐵 ) ) ∈ ℂ )
30 4 29 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( i · 𝐵 ) ) ∈ ℂ )
31 15 negcld ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 · 𝐵 ) ∈ ℂ )
32 31 anidms ⊢ ( 𝐵 ∈ ℂ → - ( 𝐵 · 𝐵 ) ∈ ℂ )
33 32 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐵 · 𝐵 ) ∈ ℂ )
34 28 30 33 npncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 · 𝐴 ) − ( 𝐴 · ( i · 𝐵 ) ) ) + ( ( 𝐴 · ( i · 𝐵 ) ) − - ( 𝐵 · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) − - ( 𝐵 · 𝐵 ) ) )
35 15 anidms ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · 𝐵 ) ∈ ℂ )
36 subneg ⊢ ( ( ( 𝐴 · 𝐴 ) ∈ ℂ ∧ ( 𝐵 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝐴 ) − - ( 𝐵 · 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
37 27 35 36 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐴 ) − - ( 𝐵 · 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
38 34 37 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 · 𝐴 ) − ( 𝐴 · ( i · 𝐵 ) ) ) + ( ( 𝐴 · ( i · 𝐵 ) ) − - ( 𝐵 · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
39 8 25 38 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + ( i · 𝐵 ) ) · ( 𝐴 − ( i · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )