Metamath Proof Explorer

Theorem absmul

Description: Absolute value distributes over multiplication. Proposition 10-3.7(f) of Gleason p. 133. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absmul ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cjmul ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) )
2 1 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 · 𝐵 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) )
3 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
4 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 3 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
6 4 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
7 3 4 5 6 mul4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ 𝐵 ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
8 2 7 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
9 8 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( √ ‘ ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) ) = ( √ ‘ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) )
10 cjmulrcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
11 cjmulge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
12 10 11 jca ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
13 cjmulrcl ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ∈ ℝ )
14 cjmulge0 ⊢ ( 𝐵 ∈ ℂ → 0 ≤ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) )
15 13 14 jca ⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
16 sqrtmul ⊢ ( ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∧ ( ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) → ( √ ‘ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) )
17 12 15 16 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( √ ‘ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) )
18 9 17 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( √ ‘ ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) )
19 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
20 absval ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( √ ‘ ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( √ ‘ ( ( 𝐴 · 𝐵 ) · ( ∗ ‘ ( 𝐴 · 𝐵 ) ) ) ) )
22 absval ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
23 absval ⊢ ( 𝐵 ∈ ℂ → ( abs ‘ 𝐵 ) = ( √ ‘ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) )
24 22 23 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 · ( ∗ ‘ 𝐵 ) ) ) ) )
25 18 21 24 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )