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 27833
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 27746 . . 3 class
31, 2wcel 1988 . 2 wff 𝐴 ∈ ℋ
4 c1 9922 . . . 4 class 1
5 csm 27748 . . . 4 class ·
64, 1, 5co 6635 . . 3 class (1 · 𝐴)
76, 1wceq 1481 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  27852  hvsubid  27853  hvaddsubval  27860  hv2times  27888  hvnegdii  27889  hilvc  27989  hhssnv  28091  h1de2bi  28383  h1datomi  28410  mayete3i  28557  homulid2  28629  lnop0  28795  lnopaddi  28800  lnophmlem2  28846  lnfn0i  28871  lnfnaddi  28872  strlem1  29079
  Copyright terms: Public domain W3C validator