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

Axiom ax-hvmulid 22358
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 22271 . . 3  class  ~H
31, 2wcel 1717 . 2  wff  A  e. 
~H
4 c1 8925 . . . 4  class  1
5 csm 22273 . . . 4  class  .h
64, 1, 5co 6021 . . 3  class  ( 1  .h  A )
76, 1wceq 1649 . 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  22376  hvsubid  22377  hvaddsubval  22384  hv2times  22412  hvnegdii  22413  hilvc  22513  hhssnv  22613  h1de2bi  22905  h1datomi  22932  mayete3i  23079  mayete3iOLD  23080  homulid2  23152  lnop0  23318  lnopaddi  23323  lnophmlem2  23369  lnfn0i  23394  lnfnaddi  23395  strlem1  23602
  Copyright terms: Public domain W3C validator