This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )