Axiom ax-hvmulid 31638

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 31551	. . 3 class ℋ
3	1, 2	wcel 2147	. 2 wff 𝐴 ∈ ℋ
4		c1 11228	. . . 4 class 1
5		csm 31553	. . . 4 class ·ℎ
6	4, 1, 5	co 7443	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1570	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is used by:  hvmul0or  31657  hvsubid  31658  hvaddsubval  31665  hv2times  31693  hvnegdii  31694  hilvc  31794  hhssnv  31896  h1de2bi  32186  h1datomi  32213  mayete3i  32360  homullid  32432  lnop0  32598  lnopaddi  32603  lnophmlem2  32649  lnfn0i  32674  lnfnaddi  32675  strlem1  32882