Axiom ax-hvmulid 31495

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 31408	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c1 11129	. . . 4 class 1
5		csm 31410	. . . 4 class ·ℎ
6	4, 1, 5	co 7417	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1570	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is used by:  hvmul0or  31514  hvsubid  31515  hvaddsubval  31522  hv2times  31550  hvnegdii  31551  hilvc  31651  hhssnv  31753  h1de2bi  32043  h1datomi  32070  mayete3i  32217  homullid  32289  lnop0  32455  lnopaddi  32460  lnophmlem2  32506  lnfn0i  32531  lnfnaddi  32532  strlem1  32739