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

Axiom ax-hvmulid 22470
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 22383 . . 3  class  ~H
31, 2wcel 1721 . 2  wff  A  e. 
~H
4 c1 8955 . . . 4  class  1
5 csm 22385 . . . 4  class  .h
64, 1, 5co 6048 . . 3  class  ( 1  .h  A )
76, 1wceq 1649 . 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  22488  hvsubid  22489  hvaddsubval  22496  hv2times  22524  hvnegdii  22525  hilvc  22625  hhssnv  22725  h1de2bi  23017  h1datomi  23044  mayete3i  23191  mayete3iOLD  23192  homulid2  23264  lnop0  23430  lnopaddi  23435  lnophmlem2  23481  lnfn0i  23506  lnfnaddi  23507  strlem1  23714
  Copyright terms: Public domain W3C validator