Axiom ax-hvmulid 30122

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 30035	. . 3 class ℋ
3	1, 2	wcel 2106	. 2 wff 𝐴 ∈ ℋ
4		c1 11093	. . . 4 class 1
5		csm 30037	. . . 4 class ·ℎ
6	4, 1, 5	co 7393	. . 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  30141  hvsubid  30142  hvaddsubval  30149  hv2times  30177  hvnegdii  30178  hilvc  30278  hhssnv  30380  h1de2bi  30670  h1datomi  30697  mayete3i  30844  homullid  30916  lnop0  31082  lnopaddi  31087  lnophmlem2  31133  lnfn0i  31158  lnfnaddi  31159  strlem1  31366