Axiom ax-hvmulid 31102

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 31015	. . 3 class ℋ
3	1, 2	wcel 2119	. 2 wff 𝐴 ∈ ℋ
4		c1 11037	. . . 4 class 1
5		csm 31017	. . . 4 class ·ℎ
6	4, 1, 5	co 7363	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1547	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  31121  hvsubid  31122  hvaddsubval  31129  hv2times  31157  hvnegdii  31158  hilvc  31258  hhssnv  31360  h1de2bi  31650  h1datomi  31677  mayete3i  31824  homullid  31896  lnop0  32062  lnopaddi  32067  lnophmlem2  32113  lnfn0i  32138  lnfnaddi  32139  strlem1  32346