Axiom ax-hvmulid 26049

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 25962	. . 3 class ~H
3	1, 2	wcel 1819	. 2 wff A e. ~H
4		c1 9510	. . . 4 class 1
5		csm 25964	. . . 4 class .h
6	4, 1, 5	co 6296	. . 3 class ( 1 .h A )
7	6, 1	wceq 1395	. 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  26068  hvsubid  26069  hvaddsubval  26076  hv2times  26104  hvnegdii  26105  hilvc  26205  hhssnv  26306  h1de2bi  26598  h1datomi  26625  mayete3i  26772  mayete3iOLD  26773  homulid2  26845  lnop0  27011  lnopaddi  27016  lnophmlem2  27062  lnfn0i  27087  lnfnaddi  27088  strlem1  27295