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 30122
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 30035 . . 3 class
31, 2wcel 2106 . 2 wff 𝐴 ∈ ℋ
4 c1 11093 . . . 4 class 1
5 csm 30037 . . . 4 class ·
64, 1, 5co 7393 . . 3 class (1 · 𝐴)
76, 1wceq 1541 . 2 wff (1 · 𝐴) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvmul0or  30141  hvsubid  30142  hvaddsubval  30149  hv2times  30177  hvnegdii  30178  hilvc  30278  hhssnv  30380  h1de2bi  30670  h1datomi  30697  mayete3i  30844  homullid  30916  lnop0  31082  lnopaddi  31087  lnophmlem2  31133  lnfn0i  31158  lnfnaddi  31159  strlem1  31366
  Copyright terms: Public domain W3C validator