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

Axiom ax-hvmulid 22501
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 22414 . . 3  class  ~H
31, 2wcel 1725 . 2  wff  A  e. 
~H
4 c1 8983 . . . 4  class  1
5 csm 22416 . . . 4  class  .h
64, 1, 5co 6073 . . 3  class  ( 1  .h  A )
76, 1wceq 1652 . 2  wff  ( 1  .h  A )  =  A
83, 7wi 4 1  wff  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0or  22519  hvsubid  22520  hvaddsubval  22527  hv2times  22555  hvnegdii  22556  hilvc  22656  hhssnv  22756  h1de2bi  23048  h1datomi  23075  mayete3i  23222  mayete3iOLD  23223  homulid2  23295  lnop0  23461  lnopaddi  23466  lnophmlem2  23512  lnfn0i  23537  lnfnaddi  23538  strlem1  23745
  Copyright terms: Public domain W3C validator