Axiom ax-hvmulid 31267

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 31180	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c1 11089	. . . 4 class 1
5		csm 31182	. . . 4 class ·ℎ
6	4, 1, 5	co 7400	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1563	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31286  hvsubid  31287  hvaddsubval  31294  hv2times  31322  hvnegdii  31323  hilvc  31423  hhssnv  31525  h1de2bi  31815  h1datomi  31842  mayete3i  31989  homullid  32061  lnop0  32227  lnopaddi  32232  lnophmlem2  32278  lnfn0i  32303  lnfnaddi  32304  strlem1  32511