Axiom ax-hvmulid 30942

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 30855	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c1 11076	. . . 4 class 1
5		csm 30857	. . . 4 class ·ℎ
6	4, 1, 5	co 7390	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1540	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  30961  hvsubid  30962  hvaddsubval  30969  hv2times  30997  hvnegdii  30998  hilvc  31098  hhssnv  31200  h1de2bi  31490  h1datomi  31517  mayete3i  31664  homullid  31736  lnop0  31902  lnopaddi  31907  lnophmlem2  31953  lnfn0i  31978  lnfnaddi  31979  strlem1  32186