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 ⊢ A ∈ ℂ
norm-iii.2 ⊢ B ∈ ℋ
Assertion norm-iii-i ⊢ norm ℎ ⁡ A ⋅ ℎ B = A ⁢ norm ℎ ⁡ B

Proof

Step Hyp Ref Expression
1 norm-iii.1 ⊢ A ∈ ℂ
2 norm-iii.2 ⊢ B ∈ ℋ
3 1 1 2 2 his35i ⊢ A ⋅ ℎ B ⋅ ih A ⋅ ℎ B = A ⁢ A ‾ ⁢ B ⋅ ih B
4 3 fveq2i ⊢ A ⋅ ℎ B ⋅ ih A ⋅ ℎ B = A ⁢ A ‾ ⁢ B ⋅ ih B
5 1 cjmulrcli ⊢ A ⁢ A ‾ ∈ ℝ
6 hiidrcl ⊢ B ∈ ℋ → B ⋅ ih B ∈ ℝ
7 2 6 ax-mp ⊢ B ⋅ ih B ∈ ℝ
8 1 cjmulge0i ⊢ 0 ≤ A ⁢ A ‾
9 hiidge0 ⊢ B ∈ ℋ → 0 ≤ B ⋅ ih B
10 2 9 ax-mp ⊢ 0 ≤ B ⋅ ih B
11 5 7 8 10 sqrtmulii ⊢ A ⁢ A ‾ ⁢ B ⋅ ih B = A ⁢ A ‾ ⁢ B ⋅ ih B
12 4 11 eqtri ⊢ A ⋅ ℎ B ⋅ ih A ⋅ ℎ B = A ⁢ A ‾ ⁢ B ⋅ ih B
13 1 2 hvmulcli ⊢ A ⋅ ℎ B ∈ ℋ
14 normval ⊢ A ⋅ ℎ B ∈ ℋ → norm ℎ ⁡ A ⋅ ℎ B = A ⋅ ℎ B ⋅ ih A ⋅ ℎ B
15 13 14 ax-mp ⊢ norm ℎ ⁡ A ⋅ ℎ B = A ⋅ ℎ B ⋅ ih A ⋅ ℎ B
16 absval ⊢ A ∈ ℂ → A = A ⁢ A ‾
17 1 16 ax-mp ⊢ A = A ⁢ A ‾
18 normval ⊢ B ∈ ℋ → norm ℎ ⁡ B = B ⋅ ih B
19 2 18 ax-mp ⊢ norm ℎ ⁡ B = B ⋅ ih B
20 17 19 oveq12i ⊢ A ⁢ norm ℎ ⁡ B = A ⁢ A ‾ ⁢ B ⋅ ih B
21 12 15 20 3eqtr4i ⊢ norm ℎ ⁡ A ⋅ ℎ B = A ⁢ norm ℎ ⁡ B