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 30297
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 30210 . . 3 class โ„‹
31, 2wcel 2106 . 2 wff ๐ด โˆˆ โ„‹
4 c1 11113 . . . 4 class 1
5 csm 30212 . . . 4 class ยทโ„Ž
64, 1, 5co 7411 . . 3 class (1 ยทโ„Ž ๐ด)
76, 1wceq 1541 . 2 wff (1 ยทโ„Ž ๐ด) = ๐ด
83, 7wi 4 1 wff (๐ด โˆˆ โ„‹ โ†’ (1 ยทโ„Ž ๐ด) = ๐ด)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  30316  hvsubid  30317  hvaddsubval  30324  hv2times  30352  hvnegdii  30353  hilvc  30453  hhssnv  30555  h1de2bi  30845  h1datomi  30872  mayete3i  31019  homullid  31091  lnop0  31257  lnopaddi  31262  lnophmlem2  31308  lnfn0i  31333  lnfnaddi  31334  strlem1  31541
  Copyright terms: Public domain W3C validator