Axiom ax-hvmulid 22462

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 22375	. . 3 class ~H
3	1, 2	wcel 1721	. 2 wff A e. ~H
4		c1 8947	. . . 4 class 1
5		csm 22377	. . . 4 class .h
6	4, 1, 5	co 6040	. . 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  22480  hvsubid  22481  hvaddsubval  22488  hv2times  22516  hvnegdii  22517  hilvc  22617  hhssnv  22717  h1de2bi  23009  h1datomi  23036  mayete3i  23183  mayete3iOLD  23184  homulid2  23256  lnop0  23422  lnopaddi  23427  lnophmlem2  23473  lnfn0i  23498  lnfnaddi  23499  strlem1  23706