Axiom ax-hvmulid 30968

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 30881	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c1 11029	. . . 4 class 1
5		csm 30883	. . . 4 class ·ℎ
6	4, 1, 5	co 7353	. . 3 class (1 ·ℎ 𝐴)
7	6, 1	wceq 1540	. 2 wff (1 ·ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴)

This axiom is referenced by:  hvmul0or  30987  hvsubid  30988  hvaddsubval  30995  hv2times  31023  hvnegdii  31024  hilvc  31124  hhssnv  31226  h1de2bi  31516  h1datomi  31543  mayete3i  31690  homullid  31762  lnop0  31928  lnopaddi  31933  lnophmlem2  31979  lnfn0i  32004  lnfnaddi  32005  strlem1  32212