Axiom ax-hvmulid 29377

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 29290	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c1 10881	. . . 4 class 1
5		csm 29292	. . . 4 class ·ℎ
6	4, 1, 5	co 7284	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1539	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  29396  hvsubid  29397  hvaddsubval  29404  hv2times  29432  hvnegdii  29433  hilvc  29533  hhssnv  29635  h1de2bi  29925  h1datomi  29952  mayete3i  30099  homulid2  30171  lnop0  30337  lnopaddi  30342  lnophmlem2  30388  lnfn0i  30413  lnfnaddi  30414  strlem1  30621