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 31025
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 30938 . . 3 class
31, 2wcel 2108 . 2 wff 𝐴 ∈ ℋ
4 c1 11156 . . . 4 class 1
5 csm 30940 . . . 4 class ·
64, 1, 5co 7431 . . 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  31044  hvsubid  31045  hvaddsubval  31052  hv2times  31080  hvnegdii  31081  hilvc  31181  hhssnv  31283  h1de2bi  31573  h1datomi  31600  mayete3i  31747  homullid  31819  lnop0  31985  lnopaddi  31990  lnophmlem2  32036  lnfn0i  32061  lnfnaddi  32062  strlem1  32269
  Copyright terms: Public domain W3C validator