Axiom ax-hvmulid 8831

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 8743	. . 3 class H~
3	1, 2	wcel 958	. 2 wff A e. H~
4		c1 5223	. . . 4 class 1
5		csm 8745	. . . 4 class .h
6	4, 1, 5	co 3961	. . 3 class (1 .h A)
7	6, 1	wceq 956	. 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 8849  hvsubidt 8850  hvaddsubvalt 8857  hv2timest 8883  hvnegdi 8884  hilvc 8984  hhssnv 9089  projlem18 9158  h1de2b 9432  h1datom 9459  mayete3 9628  homulid2t 9681  lnop0t 9845  lnopadd 9850  lnophmlem2 9897  lnfn0 9926  lnfnadd 9927  strlem1 10132

Copyright terms: Public domain