Theorem hicl 31712

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

Assertion

Ref	Expression
hicl	⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) ∈ ℂ)

Proof of Theorem hicl

Step	Hyp	Ref	Expression
1		ax-hfi 31711	. 2 ⊢ ·ih :( ℋ × ℋ)⟶ℂ
2	1	fovcl 7571	1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   ℋchba 31551   ·_ih csp 31554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-hfi 31711

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446

This theorem is used by:  hicli  31713  his5  31718  his35  31720  his7  31722  his2sub  31724  his2sub2  31725  hire  31726  hi01  31728  abshicom  31733  hi2eq  31737  hial2eq2  31739  bcs2  31814  pjhthlem1  32023  normcan  32208  pjspansn  32209  adjsym  32465  cnvadj  32524  adj2  32566  brafn  32579  kbop  32585  kbmul  32587  kbpj  32588  eigvalcl  32593  lnopeqi  32640  riesz3i  32694  cnlnadjlem2  32700  cnlnadjlem7  32705  nmopcoadji  32733  kbass2  32749  kbass5  32752  kbass6  32753  hmopidmpji  32784  pjclem4  32831  pj3si  32839