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

Axiom ax-hvmulid 22462
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 22375 . . 3  class  ~H
31, 2wcel 1721 . 2  wff  A  e. 
~H
4 c1 8947 . . . 4  class  1
5 csm 22377 . . . 4  class  .h
64, 1, 5co 6040 . . 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  22480  hvsubid  22481  hvaddsubval  22488  hv2times  22516  hvnegdii  22517  hilvc  22617  hhssnv  22717  h1de2bi  23009  h1datomi  23036  mayete3i  23183  mayete3iOLD  23184  homulid2  23256  lnop0  23422  lnopaddi  23427  lnophmlem2  23473  lnfn0i  23498  lnfnaddi  23499  strlem1  23706
  Copyright terms: Public domain W3C validator