Axiom ax-hvmulid 31590

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 31503	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c1 11182	. . . 4 class 1
5		csm 31505	. . . 4 class ·ℎ
6	4, 1, 5	co 7412	. . 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  31609  hvsubid  31610  hvaddsubval  31617  hv2times  31645  hvnegdii  31646  hilvc  31746  hhssnv  31848  h1de2bi  32138  h1datomi  32165  mayete3i  32312  homullid  32384  lnop0  32550  lnopaddi  32555  lnophmlem2  32601  lnfn0i  32626  lnfnaddi  32627  strlem1  32834