Axiom ax-hvmulid

Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvmulid	|- ( A e. ~H -> ( 1 .h A ) = A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		chba	|- ~H
2	0 1	wcel	|- A e. ~H
3		c1	|- 1
4		csm	|- .h
5	3 0 4	co	|- ( 1 .h A )
6	5 0	wceq	|- ( 1 .h A ) = A
7	2 6	wi	|- ( A e. ~H -> ( 1 .h A ) = A )