Axiom ax-hicl 5043

Description: Closure of inner product.

Assertion

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

Detailed syntax breakdown of Axiom ax-hicl

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class H~
3	1, 2	wcel 1092	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B e. H~
6	3, 5	wa 196	. 2 wff (A e. H~ /\ B e. H~)
7		csp 4963	. . . 4 class .i
8	1, 4, 7	co 3001	. . 3 class (A .i B)
9		cc 4026	. . 3 class CC
10	8, 9	wcel 1092	. 2 wff (A .i B) e. CC
11	6, 10	wi 2	1 wff ((A e. H~ /\ B e. H~) -> (A .i B) e. CC)

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