Theorem hicl 5044

Description: Closure inference for inner product.

Hypotheses

Ref	Expression
hicl.1	⊢ A ∈ ℋ
hicl.2	⊢ B ∈ ℋ

Assertion

Ref	Expression
hicl	⊢ (A ·i B) ∈ ℂ

Proof of Theorem hicl

Step	Hyp	Ref	Expression
1		hicl.1	. 2 ⊢ A ∈ ℋ
2		hicl.2	. 2 ⊢ B ∈ ℋ
3		ax-hicl 5043	. 2 ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (A ·i B) ∈ ℂ)
4	1, 2, 3	mp2an 520	1 ⊢ (A ·i B) ∈ ℂ

Syntax hints:   ∈ wcel 1092  (class class class)co 3001  ℂcc 4026   ℋ chil 4958   ·_i csp 4963

This theorem is referenced by:  normlem0 5062  normlem2 5064  normlem3 5065  normlem7 5069  normlem9 5070  normlem8 5071  bcseq 5073  norm-ii 5086  norm-iii 5087  normpyth 5090  normpar 5099  bcs 5101  occllem1 5180  occllem6 5185  pjthlem4 5228  pjthlem5 5229  pjthlem6 5230  pjthlem7 5231  pjthlem8 5232  pjthlem10 5234  pjthlem11 5235  h1de2 5458  h1de2b 5459  h1de2ctlem 5460

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-hicl 5043

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org