Axiom ax-hicl 5043

Description: Closure of inner product.

Assertion

Ref	Expression
ax-hicl	⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (A ·i B) ∈ ℂ)

Detailed syntax breakdown of Axiom ax-hicl

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class ℋ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B ∈ ℋ
6	3, 5	wa 196	. 2 wff (A ∈ ℋ ∧ B ∈ ℋ )
7		csp 4963	. . . 4 class ·i
8	1, 4, 7	co 3001	. . 3 class (A ·i B)
9		cc 4026	. . 3 class ℂ
10	8, 9	wcel 1092	. 2 wff (A ·i B) ∈ ℂ
11	6, 10	wi 2	1 wff ((A ∈ ℋ ∧ B ∈ ℋ ) → (A ·i B) ∈ ℂ)

This axiom is referenced by:  hicl 5044  his5 5050  his7 5051  his2subt 5052  hiidrclt 5053  hizer1t 5054  hi2eqt 5059  occllem4 5183  pjclem4 5653  pj3s 5659

metamath.org