Axiom ax-hvmulid 29269

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 29182	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c1 10803	. . . 4 class 1
5		csm 29184	. . . 4 class ·ℎ
6	4, 1, 5	co 7255	. . 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  29288  hvsubid  29289  hvaddsubval  29296  hv2times  29324  hvnegdii  29325  hilvc  29425  hhssnv  29527  h1de2bi  29817  h1datomi  29844  mayete3i  29991  homulid2  30063  lnop0  30229  lnopaddi  30234  lnophmlem2  30280  lnfn0i  30305  lnfnaddi  30306  strlem1  30513