Axiom ax-hvmulid 31092

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 31005	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c1 11030	. . . 4 class 1
5		csm 31007	. . . 4 class ·ℎ
6	4, 1, 5	co 7360	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1542	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31111  hvsubid  31112  hvaddsubval  31119  hv2times  31147  hvnegdii  31148  hilvc  31248  hhssnv  31350  h1de2bi  31640  h1datomi  31667  mayete3i  31814  homullid  31886  lnop0  32052  lnopaddi  32057  lnophmlem2  32103  lnfn0i  32128  lnfnaddi  32129  strlem1  32336