Axiom ax-hvmulid 25754

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 25667	. . 3 class ~H
3	1, 2	wcel 1767	. 2 wff A e. ~H
4		c1 9505	. . . 4 class 1
5		csm 25669	. . . 4 class .h
6	4, 1, 5	co 6295	. . 3 class ( 1 .h A )
7	6, 1	wceq 1379	. 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  25773  hvsubid  25774  hvaddsubval  25781  hv2times  25809  hvnegdii  25810  hilvc  25910  hhssnv  26011  h1de2bi  26303  h1datomi  26330  mayete3i  26477  mayete3iOLD  26478  homulid2  26550  lnop0  26716  lnopaddi  26721  lnophmlem2  26767  lnfn0i  26792  lnfnaddi  26793  strlem1  27000