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 28474
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 28387 . . 3 class
31, 2wcel 2081 . 2 wff 𝐴 ∈ ℋ
4 c1 10384 . . . 4 class 1
5 csm 28389 . . . 4 class ·
64, 1, 5co 7016 . . 3 class (1 · 𝐴)
76, 1wceq 1522 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  28493  hvsubid  28494  hvaddsubval  28501  hv2times  28529  hvnegdii  28530  hilvc  28630  hhssnv  28732  h1de2bi  29022  h1datomi  29049  mayete3i  29196  homulid2  29268  lnop0  29434  lnopaddi  29439  lnophmlem2  29485  lnfn0i  29510  lnfnaddi  29511  strlem1  29718
  Copyright terms: Public domain W3C validator