Axiom ax-hvmulid 31025

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 30938	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c1 11156	. . . 4 class 1
5		csm 30940	. . . 4 class ·ℎ
6	4, 1, 5	co 7431	. . 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  31044  hvsubid  31045  hvaddsubval  31052  hv2times  31080  hvnegdii  31081  hilvc  31181  hhssnv  31283  h1de2bi  31573  h1datomi  31600  mayete3i  31747  homullid  31819  lnop0  31985  lnopaddi  31990  lnophmlem2  32036  lnfn0i  32061  lnfnaddi  32062  strlem1  32269