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 28203
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 28116 . . 3 class
31, 2wcel 2145 . 2 wff 𝐴 ∈ ℋ
4 c1 10139 . . . 4 class 1
5 csm 28118 . . . 4 class ·
64, 1, 5co 6793 . . 3 class (1 · 𝐴)
76, 1wceq 1631 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  28222  hvsubid  28223  hvaddsubval  28230  hv2times  28258  hvnegdii  28259  hilvc  28359  hhssnv  28461  h1de2bi  28753  h1datomi  28780  mayete3i  28927  homulid2  28999  lnop0  29165  lnopaddi  29170  lnophmlem2  29216  lnfn0i  29241  lnfnaddi  29242  strlem1  29449
  Copyright terms: Public domain W3C validator