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 e. CC
	norm-iii.2	|- B e. ~H
Assertion	norm-iii-i	|- ( normh ` ( A .h B ) ) = ( ( abs ` A ) x. ( normh ` B ) )

Proof

Step	Hyp	Ref	Expression
1		norm-iii.1	|- A e. CC
2		norm-iii.2	|- B e. ~H
3	1 1 2 2	his35i	|- ( ( A .h B ) .ih ( A .h B ) ) = ( ( A x. ( * ` A ) ) x. ( B .ih B ) )
4	3	fveq2i	|- ( sqrt ` ( ( A .h B ) .ih ( A .h B ) ) ) = ( sqrt ` ( ( A x. ( * ` A ) ) x. ( B .ih B ) ) )
5	1	cjmulrcli	|- ( A x. ( * ` A ) ) e. RR
6		hiidrcl	|- ( B e. ~H -> ( B .ih B ) e. RR )
7	2 6	ax-mp	|- ( B .ih B ) e. RR
8	1	cjmulge0i	|- 0 <_ ( A x. ( * ` A ) )
9		hiidge0	|- ( B e. ~H -> 0 <_ ( B .ih B ) )
10	2 9	ax-mp	|- 0 <_ ( B .ih B )
11	5 7 8 10	sqrtmulii	|- ( sqrt ` ( ( A x. ( * ` A ) ) x. ( B .ih B ) ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B .ih B ) ) )
12	4 11	eqtri	|- ( sqrt ` ( ( A .h B ) .ih ( A .h B ) ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B .ih B ) ) )
13	1 2	hvmulcli	|- ( A .h B ) e. ~H
14		normval	|- ( ( A .h B ) e. ~H -> ( normh ` ( A .h B ) ) = ( sqrt ` ( ( A .h B ) .ih ( A .h B ) ) ) )
15	13 14	ax-mp	|- ( normh ` ( A .h B ) ) = ( sqrt ` ( ( A .h B ) .ih ( A .h B ) ) )
16		absval	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
17	1 16	ax-mp	|- ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) )
18		normval	|- ( B e. ~H -> ( normh ` B ) = ( sqrt ` ( B .ih B ) ) )
19	2 18	ax-mp	|- ( normh ` B ) = ( sqrt ` ( B .ih B ) )
20	17 19	oveq12i	|- ( ( abs ` A ) x. ( normh ` B ) ) = ( ( sqrt ` ( A x. ( * ` A ) ) ) x. ( sqrt ` ( B .ih B ) ) )
21	12 15 20	3eqtr4i	|- ( normh ` ( A .h B ) ) = ( ( abs ` A ) x. ( normh ` B ) )