Axiom ax-hvmulid 4991

Description: Scalar multiplication by one.

Assertion

Ref	Expression
ax-hvmulid	⊢ (A ∈ ℋ → (1 ·s A) = A)

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 4958	. . 3 class ℋ
3	1, 2	wcel 1092	. 2 wff A ∈ ℋ
4		c1 4029	. . . 4 class 1
5		csm 4960	. . . 4 class ·s
6	4, 1, 5	co 3001	. . 3 class (1 ·s A)
7	6, 1	wceq 1091	. 2 wff (1 ·s A) = A
8	3, 7	wi 2	1 wff (A ∈ ℋ → (1 ·s A) = A)

This axiom is referenced by:  hvsubidt 5005  hv2times 5033  hvnegdi 5034  projlem18 5210  h1de2b 5459  h1datom 5483  strlem1 5691

metamath.org