Axiom ax-hvmulid 31038

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 30951	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c1 11185	. . . 4 class 1
5		csm 30953	. . . 4 class ·ℎ
6	4, 1, 5	co 7448	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1537	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31057  hvsubid  31058  hvaddsubval  31065  hv2times  31093  hvnegdii  31094  hilvc  31194  hhssnv  31296  h1de2bi  31586  h1datomi  31613  mayete3i  31760  homullid  31832  lnop0  31998  lnopaddi  32003  lnophmlem2  32049  lnfn0i  32074  lnfnaddi  32075  strlem1  32282