Axiom ax-hvmulid 8797

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 8727	. . 3 class H~
3	1, 2	wcel 955	. 2 wff A e. H~
4		c1 5207	. . . 4 class 1
5		csm 8729	. . . 4 class .h
6	4, 1, 5	co 3948	. . 3 class (1 .h A)
7	6, 1	wceq 953	. 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:  hvmul0ort 8815  hvsubidt 8816  hvaddsubvalt 8823  hv2timest 8849  hvnegdi 8850  hilvc 8950  hhssnv 9054  projlem18 9119  h1de2b 9392  h1de2bOLD 9393  h1datom 9421  mayete3 9590  homulid2t 9643  lnop0t 9806  lnopadd 9811  lnophmlem2 9857  lnfn0 9886  lnfnadd 9887  strlem1 10087

Copyright terms: Public domain