Axiom ax-hvmulid 9151

Description: Scalar multiplication by one.

Assertion

Ref	Expression
ax-hvmulid	|- (A e. H~ -> (1 .h A) = A)

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 9063	. . 3 class H~
3	1, 2	wcel 994	. 2 wff A e. H~
4		c1 5389	. . . 4 class 1
5		csm 9065	. . . 4 class .h
6	4, 1, 5	co 4021	. . 3 class (1 .h A)
7	6, 1	wceq 992	. 2 wff (1 .h A) = A
8	3, 7	wi 3	1 wff (A e. H~ -> (1 .h A) = A)

This axiom is referenced by:  hvmul0or 9169  hvsubid 9170  hvaddsubval 9177  hv2times 9203  hvnegdii 9204  hilvc 9305  hhssnv 9410  projlem18 9479  h1de2bi 9753  h1datomi 9780  mayete3i 9951  mayete3OLDi 9952  homulid2 10006  lnop0 10169  lnopaddi 10174  lnophmlem2 10221  lnfn0i 10250  lnfnaddi 10251  strlem1 10458

Copyright terms: Public domain