This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-hvmulid

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

		Ref	Expression
	Assertion	ax-hvmulid	$⊢ A \in ℋ \to 1 \cdot_{ℎ} A = A$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		chba	$class ℋ$
2	0 1	wcel	$wff A \in ℋ$
3		c1	$class 1$
4		csm	$class \cdot_{ℎ}$
5	3 0 4	co	$class (1 \cdot_{ℎ} A)$
6	5 0	wceq	$wff 1 \cdot_{ℎ} A = A$
7	2 6	wi	$wff (A \in ℋ \to 1 \cdot_{ℎ} A = A)$