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

Axiom ax-hvmulid 26049
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 25962 . . 3  class  ~H
31, 2wcel 1819 . 2  wff  A  e. 
~H
4 c1 9510 . . . 4  class  1
5 csm 25964 . . . 4  class  .h
64, 1, 5co 6296 . . 3  class  ( 1  .h  A )
76, 1wceq 1395 . 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  26068  hvsubid  26069  hvaddsubval  26076  hv2times  26104  hvnegdii  26105  hilvc  26205  hhssnv  26306  h1de2bi  26598  h1datomi  26625  mayete3i  26772  mayete3iOLD  26773  homulid2  26845  lnop0  27011  lnopaddi  27016  lnophmlem2  27062  lnfn0i  27087  lnfnaddi  27088  strlem1  27295
  Copyright terms: Public domain W3C validator