Axiom ax-hvmulid 31034

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 30947	. . 3 class ℋ
3	1, 2	wcel 2105	. 2 wff 𝐴 ∈ ℋ
4		c1 11153	. . . 4 class 1
5		csm 30949	. . . 4 class ·ℎ
6	4, 1, 5	co 7430	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1536	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31053  hvsubid  31054  hvaddsubval  31061  hv2times  31089  hvnegdii  31090  hilvc  31190  hhssnv  31292  h1de2bi  31582  h1datomi  31609  mayete3i  31756  homullid  31828  lnop0  31994  lnopaddi  31999  lnophmlem2  32045  lnfn0i  32070  lnfnaddi  32071  strlem1  32278