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

Axiom ax-hvmulid 21511
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 21424 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c1 8671 . . . 4  class  1
5 csm 21426 . . . 4  class  .h
64, 1, 5co 5757 . . 3  class  ( 1  .h  A )
76, 1wceq 1619 . 2  wff  ( 1  .h  A )  =  A
83, 7wi 6 1  wff  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0or  21529  hvsubid  21530  hvaddsubval  21537  hv2times  21565  hvnegdii  21566  hilvc  21666  hhssnv  21766  h1de2bi  22058  h1datomi  22085  mayete3i  22250  mayete3iOLD  22251  homulid2  22305  lnop0  22471  lnopaddi  22476  lnophmlem2  22522  lnfn0i  22547  lnfnaddi  22548  strlem1  22755
  Copyright terms: Public domain W3C validator