Axiom ax-hvmulid 31077

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 30990	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c1 11039	. . . 4 class 1
5		csm 30992	. . . 4 class ·ℎ
6	4, 1, 5	co 7367	. . 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  31096  hvsubid  31097  hvaddsubval  31104  hv2times  31132  hvnegdii  31133  hilvc  31233  hhssnv  31335  h1de2bi  31625  h1datomi  31652  mayete3i  31799  homullid  31871  lnop0  32037  lnopaddi  32042  lnophmlem2  32088  lnfn0i  32113  lnfnaddi  32114  strlem1  32321