Axiom ax-hvmulid 31155

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 31068	. . 3 class ℋ
3	1, 2	wcel 2141	. 2 wff 𝐴 ∈ ℋ
4		c1 11071	. . . 4 class 1
5		csm 31070	. . . 4 class ·ℎ
6	4, 1, 5	co 7392	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1559	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31174  hvsubid  31175  hvaddsubval  31182  hv2times  31210  hvnegdii  31211  hilvc  31311  hhssnv  31413  h1de2bi  31703  h1datomi  31730  mayete3i  31877  homullid  31949  lnop0  32115  lnopaddi  32120  lnophmlem2  32166  lnfn0i  32191  lnfnaddi  32192  strlem1  32399