Axiom ax-hvmulid

Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvmulid	⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ 𝐴 ) = 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		chba	⊢ ℋ
2	0 1	wcel	⊢ 𝐴 ∈ ℋ
3		c1	⊢ 1
4		csm	⊢ ·ℎ
5	3 0 4	co	⊢ ( 1 ·ℎ 𝐴 )
6	5 0	wceq	⊢ ( 1 ·ℎ 𝐴 ) = 𝐴
7	2 6	wi	⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ 𝐴 ) = 𝐴 )