Axiom ax-hvmulid 22470

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 22383	. . 3 class ~H
3	1, 2	wcel 1721	. 2 wff A e. ~H
4		c1 8955	. . . 4 class 1
5		csm 22385	. . . 4 class .h
6	4, 1, 5	co 6048	. . 3 class ( 1 .h A )
7	6, 1	wceq 1649	. 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  22488  hvsubid  22489  hvaddsubval  22496  hv2times  22524  hvnegdii  22525  hilvc  22625  hhssnv  22725  h1de2bi  23017  h1datomi  23044  mayete3i  23191  mayete3iOLD  23192  homulid2  23264  lnop0  23430  lnopaddi  23435  lnophmlem2  23481  lnfn0i  23506  lnfnaddi  23507  strlem1  23714