Axiom ax-hvmulid 26708

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 26621	. . 3 class ~H
3	1, 2	wcel 1898	. 2 wff A e. ~H
4		c1 9566	. . . 4 class 1
5		csm 26623	. . . 4 class .h
6	4, 1, 5	co 6315	. . 3 class ( 1 .h A )
7	6, 1	wceq 1455	. 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  26727  hvsubid  26728  hvaddsubval  26735  hv2times  26763  hvnegdii  26764  hilvc  26864  hhssnv  26964  h1de2bi  27256  h1datomi  27283  mayete3i  27430  homulid2  27502  lnop0  27668  lnopaddi  27673  lnophmlem2  27719  lnfn0i  27744  lnfnaddi  27745  strlem1  27952