Axiom ax-hvmulid 31081

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 30994	. . 3 class ℋ
3	1, 2	wcel 2113	. 2 wff 𝐴 ∈ ℋ
4		c1 11027	. . . 4 class 1
5		csm 30996	. . . 4 class ·ℎ
6	4, 1, 5	co 7358	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1541	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31100  hvsubid  31101  hvaddsubval  31108  hv2times  31136  hvnegdii  31137  hilvc  31237  hhssnv  31339  h1de2bi  31629  h1datomi  31656  mayete3i  31803  homullid  31875  lnop0  32041  lnopaddi  32046  lnophmlem2  32092  lnfn0i  32117  lnfnaddi  32118  strlem1  32325