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ℎ ‘ 𝐵 ) )