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 27029
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 26942 . . 3 class
31, 2wcel 1938 . 2 wff 𝐴 ∈ ℋ
4 c1 9696 . . . 4 class 1
5 csm 26944 . . . 4 class ·
64, 1, 5co 6431 . . 3 class (1 · 𝐴)
76, 1wceq 1474 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  27048  hvsubid  27049  hvaddsubval  27056  hv2times  27084  hvnegdii  27085  hilvc  27185  hhssnv  27287  h1de2bi  27579  h1datomi  27606  mayete3i  27753  homulid2  27825  lnop0  27991  lnopaddi  27996  lnophmlem2  28042  lnfn0i  28067  lnfnaddi  28068  strlem1  28275
  Copyright terms: Public domain W3C validator