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 27247
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 chil 27160 . . 3 class
31, 2wcel 1977 . 2 wff 𝐴 ∈ ℋ
4 c1 9816 . . . 4 class 1
5 csm 27162 . . . 4 class ·
64, 1, 5co 6549 . . 3 class (1 · 𝐴)
76, 1wceq 1475 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  27266  hvsubid  27267  hvaddsubval  27274  hv2times  27302  hvnegdii  27303  hilvc  27403  hhssnv  27505  h1de2bi  27797  h1datomi  27824  mayete3i  27971  homulid2  28043  lnop0  28209  lnopaddi  28214  lnophmlem2  28260  lnfn0i  28285  lnfnaddi  28286  strlem1  28493
  Copyright terms: Public domain W3C validator