Axiom ax-hvmulid 26645

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 26558	. . 3 class ~H
3	1, 2	wcel 1868	. 2 wff A e. ~H
4		c1 9541	. . . 4 class 1
5		csm 26560	. . . 4 class .h
6	4, 1, 5	co 6302	. . 3 class ( 1 .h A )
7	6, 1	wceq 1437	. 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  26664  hvsubid  26665  hvaddsubval  26672  hv2times  26700  hvnegdii  26701  hilvc  26801  hhssnv  26901  h1de2bi  27193  h1datomi  27220  mayete3i  27367  homulid2  27439  lnop0  27605  lnopaddi  27610  lnophmlem2  27656  lnfn0i  27681  lnfnaddi  27682  strlem1  27889