# 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}\in ℂ$
norm-iii.2 ${⊢}{B}\in ℋ$
Assertion norm-iii-i ${⊢}{norm}_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\left|{A}\right|{norm}_{ℎ}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 norm-iii.1 ${⊢}{A}\in ℂ$
2 norm-iii.2 ${⊢}{B}\in ℋ$
3 1 1 2 2 his35i ${⊢}\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)={A}\stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{B}\right)$
4 3 fveq2i ${⊢}\sqrt{\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)}=\sqrt{{A}\stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{B}\right)}$
5 1 cjmulrcli ${⊢}{A}\stackrel{‾}{{A}}\in ℝ$
6 hiidrcl ${⊢}{B}\in ℋ\to {B}{\cdot }_{\mathrm{ih}}{B}\in ℝ$
7 2 6 ax-mp ${⊢}{B}{\cdot }_{\mathrm{ih}}{B}\in ℝ$
8 1 cjmulge0i ${⊢}0\le {A}\stackrel{‾}{{A}}$
9 hiidge0 ${⊢}{B}\in ℋ\to 0\le {B}{\cdot }_{\mathrm{ih}}{B}$
10 2 9 ax-mp ${⊢}0\le {B}{\cdot }_{\mathrm{ih}}{B}$
11 5 7 8 10 sqrtmulii ${⊢}\sqrt{{A}\stackrel{‾}{{A}}\left({B}{\cdot }_{\mathrm{ih}}{B}\right)}=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}$
12 4 11 eqtri ${⊢}\sqrt{\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)}=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}$
13 1 2 hvmulcli ${⊢}{A}{\cdot }_{ℎ}{B}\in ℋ$
14 normval ${⊢}{A}{\cdot }_{ℎ}{B}\in ℋ\to {norm}_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\sqrt{\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)}$
15 13 14 ax-mp ${⊢}{norm}_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\sqrt{\left({A}{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)}$
16 absval ${⊢}{A}\in ℂ\to \left|{A}\right|=\sqrt{{A}\stackrel{‾}{{A}}}$
17 1 16 ax-mp ${⊢}\left|{A}\right|=\sqrt{{A}\stackrel{‾}{{A}}}$
18 normval ${⊢}{B}\in ℋ\to {norm}_{ℎ}\left({B}\right)=\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}$
19 2 18 ax-mp ${⊢}{norm}_{ℎ}\left({B}\right)=\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}$
20 17 19 oveq12i ${⊢}\left|{A}\right|{norm}_{ℎ}\left({B}\right)=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}$
21 12 15 20 3eqtr4i ${⊢}{norm}_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\left|{A}\right|{norm}_{ℎ}\left({B}\right)$