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

Axiom ax-hvmulid 26645
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 26558 . . 3  class  ~H
31, 2wcel 1868 . 2  wff  A  e. 
~H
4 c1 9541 . . . 4  class  1
5 csm 26560 . . . 4  class  .h
64, 1, 5co 6302 . . 3  class  ( 1  .h  A )
76, 1wceq 1437 . 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  26664  hvsubid  26665  hvaddsubval  26672  hv2times  26700  hvnegdii  26701  hilvc  26801  hhssnv  26901  h1de2bi  27193  h1datomi  27220  mayete3i  27367  homulid2  27439  lnop0  27605  lnopaddi  27610  lnophmlem2  27656  lnfn0i  27681  lnfnaddi  27682  strlem1  27889
  Copyright terms: Public domain W3C validator