Axiom ax-hvmulid 8900

Description: Scalar multiplication by one.

Assertion

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

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 8812	. . 3 class ℋ
3	1, 2	wcel 962	. 2 wff A ∈ ℋ
4		c1 5255	. . . 4 class 1
5		csm 8814	. . . 4 class ·h
6	4, 1, 5	co 3979	. . 3 class (1 ·h A)
7	6, 1	wceq 960	. 2 wff (1 ·h A) = A
8	3, 7	wi 3	1 wff (A ∈ ℋ → (1 ·h A) = A)

This axiom is referenced by:  hvmul0or 8918  hvsubid 8919  hvaddsubval 8926  hv2times 8952  hvnegdii 8953  hilvc 9053  hhssnv 9158  projlem18 9227  h1de2bi 9501  h1datomi 9528  mayete3i 9697  homulid2 9750  lnop0 9914  lnopaddi 9919  lnophmlem2 9966  lnfn0i 9995  lnfnaddi 9996  strlem1 10202

Copyright terms: Public domain