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

Axiom ax-hvmulid 25754
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 25667 . . 3  class  ~H
31, 2wcel 1767 . 2  wff  A  e. 
~H
4 c1 9505 . . . 4  class  1
5 csm 25669 . . . 4  class  .h
64, 1, 5co 6295 . . 3  class  ( 1  .h  A )
76, 1wceq 1379 . 2  wff  ( 1  .h  A )  =  A
83, 7wi 4 1  wff  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  25773  hvsubid  25774  hvaddsubval  25781  hv2times  25809  hvnegdii  25810  hilvc  25910  hhssnv  26011  h1de2bi  26303  h1datomi  26330  mayete3i  26477  mayete3iOLD  26478  homulid2  26550  lnop0  26716  lnopaddi  26721  lnophmlem2  26767  lnfn0i  26792  lnfnaddi  26793  strlem1  27000
  Copyright terms: Public domain W3C validator