Axiom ax-hvmulid 28783

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 28696	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c1 10538	. . . 4 class 1
5		csm 28698	. . . 4 class ·ℎ
6	4, 1, 5	co 7156	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1537	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  28802  hvsubid  28803  hvaddsubval  28810  hv2times  28838  hvnegdii  28839  hilvc  28939  hhssnv  29041  h1de2bi  29331  h1datomi  29358  mayete3i  29505  homulid2  29577  lnop0  29743  lnopaddi  29748  lnophmlem2  29794  lnfn0i  29819  lnfnaddi  29820  strlem1  30027