Axiom ax-hvmulid 31093

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 31006	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c1 11039	. . . 4 class 1
5		csm 31008	. . . 4 class ·ℎ
6	4, 1, 5	co 7368	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1542	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31112  hvsubid  31113  hvaddsubval  31120  hv2times  31148  hvnegdii  31149  hilvc  31249  hhssnv  31351  h1de2bi  31641  h1datomi  31668  mayete3i  31815  homullid  31887  lnop0  32053  lnopaddi  32058  lnophmlem2  32104  lnfn0i  32129  lnfnaddi  32130  strlem1  32337