Axiom ax-hvmulid 31613

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 31526	. . 3 class ℋ
3	1, 2	wcel 2144	. 2 wff 𝐴 ∈ ℋ
4		c1 11204	. . . 4 class 1
5		csm 31528	. . . 4 class ·ℎ
6	4, 1, 5	co 7420	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1569	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is used by:  hvmul0or  31632  hvsubid  31633  hvaddsubval  31640  hv2times  31668  hvnegdii  31669  hilvc  31769  hhssnv  31871  h1de2bi  32161  h1datomi  32188  mayete3i  32335  homullid  32407  lnop0  32573  lnopaddi  32578  lnophmlem2  32624  lnfn0i  32649  lnfnaddi  32650  strlem1  32857