Axiom ax-hvmulid 26337

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 26250	. . 3 class ~H
3	1, 2	wcel 1842	. 2 wff A e. ~H
4		c1 9523	. . . 4 class 1
5		csm 26252	. . . 4 class .h
6	4, 1, 5	co 6278	. . 3 class ( 1 .h A )
7	6, 1	wceq 1405	. 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  26356  hvsubid  26357  hvaddsubval  26364  hv2times  26392  hvnegdii  26393  hilvc  26493  hhssnv  26594  h1de2bi  26886  h1datomi  26913  mayete3i  27060  homulid2  27132  lnop0  27298  lnopaddi  27303  lnophmlem2  27349  lnfn0i  27374  lnfnaddi  27375  strlem1  27582