Axiom ax-hvmulid 30981

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 30894	. . 3 class ℋ
3	1, 2	wcel 2111	. 2 wff 𝐴 ∈ ℋ
4		c1 11004	. . . 4 class 1
5		csm 30896	. . . 4 class ·ℎ
6	4, 1, 5	co 7346	. . 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  31000  hvsubid  31001  hvaddsubval  31008  hv2times  31036  hvnegdii  31037  hilvc  31137  hhssnv  31239  h1de2bi  31529  h1datomi  31556  mayete3i  31703  homullid  31775  lnop0  31941  lnopaddi  31946  lnophmlem2  31992  lnfn0i  32017  lnfnaddi  32018  strlem1  32225