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

Axiom ax-hvmulid 21586
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 21499 . . 3  class  ~H
31, 2wcel 1684 . 2  wff  A  e. 
~H
4 c1 8738 . . . 4  class  1
5 csm 21501 . . . 4  class  .h
64, 1, 5co 5858 . . 3  class  ( 1  .h  A )
76, 1wceq 1623 . 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  21604  hvsubid  21605  hvaddsubval  21612  hv2times  21640  hvnegdii  21641  hilvc  21741  hhssnv  21841  h1de2bi  22133  h1datomi  22160  mayete3i  22307  mayete3iOLD  22308  homulid2  22380  lnop0  22546  lnopaddi  22551  lnophmlem2  22597  lnfn0i  22622  lnfnaddi  22623  strlem1  22830
  Copyright terms: Public domain W3C validator