Axiom ax-hvmulid 30935

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 30848	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c1 11069	. . . 4 class 1
5		csm 30850	. . . 4 class ·ℎ
6	4, 1, 5	co 7387	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1540	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  30954  hvsubid  30955  hvaddsubval  30962  hv2times  30990  hvnegdii  30991  hilvc  31091  hhssnv  31193  h1de2bi  31483  h1datomi  31510  mayete3i  31657  homullid  31729  lnop0  31895  lnopaddi  31900  lnophmlem2  31946  lnfn0i  31971  lnfnaddi  31972  strlem1  32179