Axiom ax-hvmulid 29087

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 29000	. . 3 class ℋ
3	1, 2	wcel 2110	. 2 wff 𝐴 ∈ ℋ
4		c1 10730	. . . 4 class 1
5		csm 29002	. . . 4 class ·ℎ
6	4, 1, 5	co 7213	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1543	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  29106  hvsubid  29107  hvaddsubval  29114  hv2times  29142  hvnegdii  29143  hilvc  29243  hhssnv  29345  h1de2bi  29635  h1datomi  29662  mayete3i  29809  homulid2  29881  lnop0  30047  lnopaddi  30052  lnophmlem2  30098  lnfn0i  30123  lnfnaddi  30124  strlem1  30331