Axiom ax-hvmulcl 4989

Description: Closure of scalar multiplication.

Assertion

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

Detailed syntax breakdown of Axiom ax-hvmulcl

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 4026	. . . 4 class CC
3	1, 2	wcel 1092	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 4958	. . . 4 class H~
6	4, 5	wcel 1092	. . 3 wff B e. H~
7	3, 6	wa 196	. 2 wff (A e. CC /\ B e. H~)
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) e. H~
11	7, 10	wi 2	1 wff ((A e. CC /\ B e. H~) -> (A .s B) e. H~)

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