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

Axiom ax-hvmulid 21416
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 21329 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c1 8618 . . . 4  class  1
5 csm 21331 . . . 4  class  .h
64, 1, 5co 5710 . . 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  21434  hvsubid  21435  hvaddsubval  21442  hv2times  21470  hvnegdii  21471  hilvc  21571  hhssnv  21671  h1de2bi  21963  h1datomi  21990  mayete3i  22155  mayete3iOLD  22156  homulid2  22210  lnop0  22376  lnopaddi  22381  lnophmlem2  22427  lnfn0i  22452  lnfnaddi  22453  strlem1  22660
  Copyright terms: Public domain W3C validator