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 \mathscr{H}$$
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 \mathscr{H}$$
3	1 1 2 2	his35i	$$⊢\left(A{\cdot }_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(A{\cdot }_{ℎ}B\right)=A\bar{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\bar{A}\left(B{\cdot }_{\mathrm{ih}}B\right)}$$
5	1	cjmulrcli	$$⊢A\bar{A}\in ℝ$$
6		hiidrcl	$$⊢B\in \mathscr{H}\to B{\cdot }_{\mathrm{ih}}B\in ℝ$$
7	2 6	ax-mp	$$⊢B{\cdot }_{\mathrm{ih}}B\in ℝ$$
8	1	cjmulge0i	$$⊢0\le A\bar{A}$$
9		hiidge0	$$⊢B\in \mathscr{H}\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\bar{A}\left(B{\cdot }_{\mathrm{ih}}B\right)}=\sqrt{A\bar{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\bar{A}}\sqrt{B{\cdot }_{\mathrm{ih}}B}$$
13	1 2	hvmulcli	$$⊢A{\cdot }_{ℎ}B\in \mathscr{H}$$
14		normval	$$⊢A{\cdot }_{ℎ}B\in \mathscr{H}\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\bar{A}}$$
17	1 16	ax-mp	$$⊢\left|A\right|=\sqrt{A\bar{A}}$$
18		normval	$$⊢B\in \mathscr{H}\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\bar{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)$$