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

Axiom ax-hvmulid 26708
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 26621 . . 3  class  ~H
31, 2wcel 1898 . 2  wff  A  e. 
~H
4 c1 9566 . . . 4  class  1
5 csm 26623 . . . 4  class  .h
64, 1, 5co 6315 . . 3  class  ( 1  .h  A )
76, 1wceq 1455 . 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  26727  hvsubid  26728  hvaddsubval  26735  hv2times  26763  hvnegdii  26764  hilvc  26864  hhssnv  26964  h1de2bi  27256  h1datomi  27283  mayete3i  27430  homulid2  27502  lnop0  27668  lnopaddi  27673  lnophmlem2  27719  lnfn0i  27744  lnfnaddi  27745  strlem1  27952
  Copyright terms: Public domain W3C validator