Axiom ax-hvmulid 31336

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 31249	. . 3 class ℋ
3	1, 2	wcel 2143	. 2 wff 𝐴 ∈ ℋ
4		c1 11102	. . . 4 class 1
5		csm 31251	. . . 4 class ·ℎ
6	4, 1, 5	co 7412	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1570	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31355  hvsubid  31356  hvaddsubval  31363  hv2times  31391  hvnegdii  31392  hilvc  31492  hhssnv  31594  h1de2bi  31884  h1datomi  31911  mayete3i  32058  homullid  32130  lnop0  32296  lnopaddi  32301  lnophmlem2  32347  lnfn0i  32372  lnfnaddi  32373  strlem1  32580