Axiom ax-hvmulid 8959

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 8871	. . 3 class H~
3	1, 2	wcel 999	. 2 wff A e. H~
4		c1 5300	. . . 4 class 1
5		csm 8873	. . . 4 class .h
6	4, 1, 5	co 4021	. . 3 class (1 .h A)
7	6, 1	wceq 997	. 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 8977  hvsubid 8978  hvaddsubval 8985  hv2times 9011  hvnegdii 9012  hilvc 9112  hhssnv 9217  projlem18 9286  h1de2bi 9560  h1datomi 9587  mayete3i 9756  homulid2 9809  lnop0 9973  lnopaddi 9978  lnophmlem2 10025  lnfn0i 10054  lnfnaddi 10055  strlem1 10261

Copyright terms: Public domain