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

Metamath Proof Explorer

Theorem norm-iii-i

Description: Theorem 3.3(iii) of Beran p. 97. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

Ref Expression
Hypotheses norm-iii.1 ⊢ 𝐴 ∈ ℂ
norm-iii.2 ⊢ 𝐵 ∈ ℋ
Assertion norm-iii-i ( normℎ ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 norm-iii.1 ⊢ 𝐴 ∈ ℂ
2 norm-iii.2 ⊢ 𝐵 ∈ ℋ
3 1 1 2 2 his35i ⊢ ( ( 𝐴 ·ℎ 𝐵 ) ·ih ( 𝐴 ·ℎ 𝐵 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐵 ) )
4 3 fveq2i ⊢ ( √ ‘ ( ( 𝐴 ·ℎ 𝐵 ) ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) = ( √ ‘ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐵 ) ) )
5 1 cjmulrcli ⊢ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ
6 hiidrcl ⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ·ih 𝐵 ) ∈ ℝ )
7 2 6 ax-mp ⊢ ( 𝐵 ·ih 𝐵 ) ∈ ℝ
8 1 cjmulge0i ⊢ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) )
9 hiidge0 ⊢ ( 𝐵 ∈ ℋ → 0 ≤ ( 𝐵 ·ih 𝐵 ) )
10 2 9 ax-mp ⊢ 0 ≤ ( 𝐵 ·ih 𝐵 )
11 5 7 8 10 sqrtmulii ⊢ ( √ ‘ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐵 ) ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
12 4 11 eqtri ⊢ ( √ ‘ ( ( 𝐴 ·ℎ 𝐵 ) ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
13 1 2 hvmulcli ⊢ ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ
14 normval ⊢ ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ → ( normℎ ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( √ ‘ ( ( 𝐴 ·ℎ 𝐵 ) ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) )
15 13 14 ax-mp ⊢ ( normℎ ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( √ ‘ ( ( 𝐴 ·ℎ 𝐵 ) ·ih ( 𝐴 ·ℎ 𝐵 ) ) )
16 absval ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
17 1 16 ax-mp ⊢ ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
18 normval ⊢ ( 𝐵 ∈ ℋ → ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
19 2 18 ax-mp ⊢ ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) )
20 17 19 oveq12i ⊢ ( ( abs ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
21 12 15 20 3eqtr4i ⊢ ( normℎ ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( normℎ ‘ 𝐵 ) )