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

Axiom ax-hvmulid 21602
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 21515 . . 3  class  ~H
31, 2wcel 1696 . 2  wff  A  e. 
~H
4 c1 8754 . . . 4  class  1
5 csm 21517 . . . 4  class  .h
64, 1, 5co 5874 . . 3  class  ( 1  .h  A )
76, 1wceq 1632 . 2  wff  ( 1  .h  A )  =  A
83, 7wi 4 1  wff  ( A  e.  ~H  ->  (
1  .h  A )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0or  21620  hvsubid  21621  hvaddsubval  21628  hv2times  21656  hvnegdii  21657  hilvc  21757  hhssnv  21857  h1de2bi  22149  h1datomi  22176  mayete3i  22323  mayete3iOLD  22324  homulid2  22396  lnop0  22562  lnopaddi  22567  lnophmlem2  22613  lnfn0i  22638  lnfnaddi  22639  strlem1  22846
  Copyright terms: Public domain W3C validator