Metamath Proof Explorer

Theorem hicl

Description: Closure of inner product. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Assertion hicl 
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )

Proof

Step Hyp Ref Expression
1 ax-hfi 
 |-  .ih : ( ~H X. ~H ) --> CC
2 1 fovcl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )