Axiom ax-hvmulcl 4989

Description: Closure of scalar multiplication.

Assertion

Ref	Expression
ax-hvmulcl	⊢ ((A ∈ ℂ ∧ B ∈ ℋ ) → (A ·s B) ∈ ℋ )

Detailed syntax breakdown of Axiom ax-hvmulcl

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

This axiom is referenced by:  hvmulcl 4990  hvsubclt 4998  hvsub4t 5014  hvaddsub12t 5015  hvsubcan1t 5016  hvaddsubasst 5018  his5 5050  his2subt 5052  helch 5151  ocsh 5164  h1de2ct 5461  spansncol 5473  spanunsn 5482

metamath.org