Axiom ax-hvmulid 27863

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

Assertion

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

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 27776	. . 3 class ~H
3	1, 2	wcel 1990	. 2 wff A e. ~H
4		c1 9937	. . . 4 class 1
5		csm 27778	. . . 4 class .h
6	4, 1, 5	co 6650	. . 3 class ( 1 .h A )
7	6, 1	wceq 1483	. 2 wff ( 1 .h A ) = A
8	3, 7	wi 4	1 wff ( A e. ~H -> ( 1 .h A ) = A )

This axiom is referenced by:  hvmul0or  27882  hvsubid  27883  hvaddsubval  27890  hv2times  27918  hvnegdii  27919  hilvc  28019  hhssnv  28121  h1de2bi  28413  h1datomi  28440  mayete3i  28587  homulid2  28659  lnop0  28825  lnopaddi  28830  lnophmlem2  28876  lnfn0i  28901  lnfnaddi  28902  strlem1  29109