Axiom ax-hvmulid 30988

Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hvmulid	⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		chba 30901	. . 3 class ℋ
3	1, 2	wcel 2113	. 2 wff 𝐴 ∈ ℋ
4		c1 11014	. . . 4 class 1
5		csm 30903	. . . 4 class ·ℎ
6	4, 1, 5	co 7352	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1541	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31007  hvsubid  31008  hvaddsubval  31015  hv2times  31043  hvnegdii  31044  hilvc  31144  hhssnv  31246  h1de2bi  31536  h1datomi  31563  mayete3i  31710  homullid  31782  lnop0  31948  lnopaddi  31953  lnophmlem2  31999  lnfn0i  32024  lnfnaddi  32025  strlem1  32232