Axiom ax-hvmulid 30933

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 30846	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c1 11128	. . . 4 class 1
5		csm 30848	. . . 4 class ·ℎ
6	4, 1, 5	co 7403	. . 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  30952  hvsubid  30953  hvaddsubval  30960  hv2times  30988  hvnegdii  30989  hilvc  31089  hhssnv  31191  h1de2bi  31481  h1datomi  31508  mayete3i  31655  homullid  31727  lnop0  31893  lnopaddi  31898  lnophmlem2  31944  lnfn0i  31969  lnfnaddi  31970  strlem1  32177