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

Axiom ax-hvmulid 21532
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 21445 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c1 8692 . . . 4  class  1
5 csm 21447 . . . 4  class  .h
64, 1, 5co 5778 . . 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  21550  hvsubid  21551  hvaddsubval  21558  hv2times  21586  hvnegdii  21587  hilvc  21687  hhssnv  21787  h1de2bi  22079  h1datomi  22106  mayete3i  22271  mayete3iOLD  22272  homulid2  22326  lnop0  22492  lnopaddi  22497  lnophmlem2  22543  lnfn0i  22568  lnfnaddi  22569  strlem1  22776
  Copyright terms: Public domain W3C validator