HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvmulid Structured version   Unicode version

Axiom ax-hvmulid 26337
Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvmulid  |-  ( A  e.  ~H  ->  (
1  .h  A )  =  A )

Detailed syntax breakdown of Axiom ax-hvmulid
StepHypRef Expression
1 cA . . 3  class  A
2 chil 26250 . . 3  class  ~H
31, 2wcel 1842 . 2  wff  A  e. 
~H
4 c1 9523 . . . 4  class  1
5 csm 26252 . . . 4  class  .h
64, 1, 5co 6278 . . 3  class  ( 1  .h  A )
76, 1wceq 1405 . 2  wff  ( 1  .h  A )  =  A
83, 7wi 4 1  wff  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  26356  hvsubid  26357  hvaddsubval  26364  hv2times  26392  hvnegdii  26393  hilvc  26493  hhssnv  26594  h1de2bi  26886  h1datomi  26913  mayete3i  27060  homulid2  27132  lnop0  27298  lnopaddi  27303  lnophmlem2  27349  lnfn0i  27374  lnfnaddi  27375  strlem1  27582
  Copyright terms: Public domain W3C validator