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

Axiom ax-hvmulid 21580
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 21493 . . 3  class  ~H
31, 2wcel 1687 . 2  wff  A  e. 
~H
4 c1 8735 . . . 4  class  1
5 csm 21495 . . . 4  class  .h
64, 1, 5co 5821 . . 3  class  ( 1  .h  A )
76, 1wceq 1625 . 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  21598  hvsubid  21599  hvaddsubval  21606  hv2times  21634  hvnegdii  21635  hilvc  21735  hhssnv  21835  h1de2bi  22127  h1datomi  22154  mayete3i  22301  mayete3iOLD  22302  homulid2  22374  lnop0  22540  lnopaddi  22545  lnophmlem2  22591  lnfn0i  22616  lnfnaddi  22617  strlem1  22824
  Copyright terms: Public domain W3C validator