Axiom ax-hvmulid 31395

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 31308	. . 3 class ℋ
3	1, 2	wcel 2146	. 2 wff 𝐴 ∈ ℋ
4		c1 11119	. . . 4 class 1
5		csm 31310	. . . 4 class ·ℎ
6	4, 1, 5	co 7423	. . 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  31414  hvsubid  31415  hvaddsubval  31422  hv2times  31450  hvnegdii  31451  hilvc  31551  hhssnv  31653  h1de2bi  31943  h1datomi  31970  mayete3i  32117  homullid  32189  lnop0  32355  lnopaddi  32360  lnophmlem2  32406  lnfn0i  32431  lnfnaddi  32432  strlem1  32639