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

Axiom ax-hvmulid 30523
Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvmulid (๐ด โˆˆ โ„‹ โ†’ (1 ยทโ„Ž ๐ด) = ๐ด)

Detailed syntax breakdown of Axiom ax-hvmulid
StepHypRef Expression
1 cA . . 3 class ๐ด
2 chba 30436 . . 3 class โ„‹
31, 2wcel 2105 . 2 wff ๐ด โˆˆ โ„‹
4 c1 11114 . . . 4 class 1
5 csm 30438 . . . 4 class ยทโ„Ž
64, 1, 5co 7412 . . 3 class (1 ยทโ„Ž ๐ด)
76, 1wceq 1540 . 2 wff (1 ยทโ„Ž ๐ด) = ๐ด
83, 7wi 4 1 wff (๐ด โˆˆ โ„‹ โ†’ (1 ยทโ„Ž ๐ด) = ๐ด)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  30542  hvsubid  30543  hvaddsubval  30550  hv2times  30578  hvnegdii  30579  hilvc  30679  hhssnv  30781  h1de2bi  31071  h1datomi  31098  mayete3i  31245  homullid  31317  lnop0  31483  lnopaddi  31488  lnophmlem2  31534  lnfn0i  31559  lnfnaddi  31560  strlem1  31767
  Copyright terms: Public domain W3C validator