Axiom ax-hvmulid 28777

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 28690	. . 3 class ℋ
3	1, 2	wcel 2110	. 2 wff 𝐴 ∈ ℋ
4		c1 10532	. . . 4 class 1
5		csm 28692	. . . 4 class ·ℎ
6	4, 1, 5	co 7150	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1533	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  28796  hvsubid  28797  hvaddsubval  28804  hv2times  28832  hvnegdii  28833  hilvc  28933  hhssnv  29035  h1de2bi  29325  h1datomi  29352  mayete3i  29499  homulid2  29571  lnop0  29737  lnopaddi  29742  lnophmlem2  29788  lnfn0i  29813  lnfnaddi  29814  strlem1  30021