Axiom ax-hvmulid 9024

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 8968	. . 3 class H~
3	1, 2	wcel 1105	. 2 wff A e. H~
4		c1 5158	. . . 4 class 1
5		csm 8970	. . . 4 class .h
6	4, 1, 5	co 3902	. . 3 class (1 .h A)
7	6, 1	wceq 1099	. 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 9043  hvsubidt 9044  hvaddsubvalt 9051  hv2timest 9077  hvnegdi 9078  hilvc 9178  projlem18 9333  h1de2b 9606  h1de2bOLD 9607  h1datom 9635  mayete3 9804  homulid2t 9857  lnop0t 10020  lnopadd 10025  lnophmlem2 10071  lnfn0 10100  lnfnadd 10101  strlem1 10301

Copyright terms: Public domain