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

Axiom ax-hvmulid 22509
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 22422 . . 3  class  ~H
31, 2wcel 1725 . 2  wff  A  e. 
~H
4 c1 8991 . . . 4  class  1
5 csm 22424 . . . 4  class  .h
64, 1, 5co 6081 . . 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  22527  hvsubid  22528  hvaddsubval  22535  hv2times  22563  hvnegdii  22564  hilvc  22664  hhssnv  22764  h1de2bi  23056  h1datomi  23083  mayete3i  23230  mayete3iOLD  23231  homulid2  23303  lnop0  23469  lnopaddi  23474  lnophmlem2  23520  lnfn0i  23545  lnfnaddi  23546  strlem1  23753
  Copyright terms: Public domain W3C validator