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 28143
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 28056 . . 3 class
31, 2wcel 2127 . 2 wff 𝐴 ∈ ℋ
4 c1 10100 . . . 4 class 1
5 csm 28058 . . . 4 class ·
64, 1, 5co 6801 . . 3 class (1 · 𝐴)
76, 1wceq 1620 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  28162  hvsubid  28163  hvaddsubval  28170  hv2times  28198  hvnegdii  28199  hilvc  28299  hhssnv  28401  h1de2bi  28693  h1datomi  28720  mayete3i  28867  homulid2  28939  lnop0  29105  lnopaddi  29110  lnophmlem2  29156  lnfn0i  29181  lnfnaddi  29182  strlem1  29389
  Copyright terms: Public domain W3C validator