Axiom ax-hfvmul 9150

Description: Scalar multiplication is an operation on CC and H~.

Assertion

Ref	Expression
ax-hfvmul	|- .h :(CC X. H~)-->H~

Detailed syntax breakdown of Axiom ax-hfvmul

Step	Hyp	Ref	Expression
1		cc 5386	. . 3 class CC
2		chil 9063	. . 3 class H~
3	1, 2	cxp 3249	. 2 class (CC X. H~)
4		csm 9065	. 2 class .h
5	3, 2, 4	wf 3259	1 wff .h :(CC X. H~)-->H~

This axiom is referenced by:  hvmulex 9156  hvmulcl 9158  hilvc 9305  hhssabli 9408  hhssnv 9410  hhsssh 9415

Copyright terms: Public domain